PROPOSITIONAL RULES


******* INTRO RULES *******                    *** TRANSFORMATION RULES ***

      | A                                            ~A -> B
      |---                                     DFA  ---------
      | B                                             A v B
CP   -------
      A -> B                                         (A -> B) & (B -> A)
                                               LB   ---------------------
        A                                                  A <-> B
DNN  -------
       ~~A                                           A <-> B
                                               CQ   ---------
        A                                            B <-> A
        B
FC   -------                                         A & B
      A & B                                    CC   -------
                                                     B & A

        A         B                                  A v B
FD   -------   -------                         CD   -------
      A v B     A v B                                B v A

                                                     ~A & ~B      ~A v ~B
******* ELIM RULES *******                     DM   ----------   ----------
                                                     ~(A v B)     ~(A & B)
      A -> B
        A                                              A & B
AA   -------                                   DNA  ------------
        B                                            ~(A -> ~B)

       ~~A                                            A -> B
DNP  -------                                   COP  ----------
        A                                            ~B -> ~A

      A & B     A & B
CJ   -------   -------                         ******* OTHER RULES *******
        A         B
                                                     ...A...     ...B...
      A -> B                                         A <-> B     A <-> B
       ~B                                      RQ   ---------   ---------
DC   -------                                         ...B...     ...A...
       ~A
                                                     | A    | A
      A v B     A v B                                |---   |---
       ~B        ~A                                  | ~B   | B
DD   -------   -------                         IP   -------------
        A         B                                      ~A

      A v B     A v B                                A -> B
      A -> C    A -> C                               B -> C
      B -> C    B -> D                         HS   --------
DS   -------   -------                               A -> C
        C       C v D


Rules with multiple versions may be referred to by their simple names
(use "DM" instead of "DM &" or "DM~v", etc.).  All transformation
rules may be reversed (i.e., there are really two versions of LB, four
versions of DM, etc.).  Double-negations may be automatically
simplified in all rules.  For example, DC could be used with ~A -> ~B
and B to infer A.



PREDICATIVE RULES


(1) Existential Generalization--EG

         Suppose that t  is a term and  j,k,...,m are any  occurrences of
 this term in F(t).

         (i)   F(t)                	Dependencies {e,...,f}
  iEG     (j)   (E X) F(X)          Dependencies {e,...,f}


 (2) Existential Specification--ES

         (i)   (E X) F(X,Y)        	Dependencies {e,...,f}
 VARIABLES* X
 AMBIGUOUS TERM* #Y (an ambiguous name with the postscript Y)
 iES     (j)   F(#Y, Y)         	Dependencies {e,...,f}

 (3)  Universal Generalization--UG

         (i) F(X,Y,Z)            	 Dependencies {e,...,f; W ... U}
 GENERALIZE* X
 iUG     (j) (A X) F(X,Y,Z)     	 Dependencies {e,...,f}

(4)  Universal Specification--US

         (i) (A X) F(X,...)   		 Dependencies {e,...,f}
 iUS     (j)  F(Y,1...)     		 Dependencies {e,...,f}

 
	(1)  Flagging restriction on UG: UG may not be applied  to a
     line using  a variable that  is flagged in  that line,  that is,
     using a  variable that is  free in  that line AND  is free  in a
     premise upon which that line depends.

         (2)  Introduction of ambiguous  names (ES): In  applying ES,
     the  ambiguous  name  entered  must  not  have  been  introduced
     previously by any rule.

         (3)  Postscripting of ambiguous names (ES):  Ambiguous names
     have a natural dependency relation on any free variables  AND on
     postscripts occurring in the  line to which ES is  applied. This
     dependency  is  made  explicit  by  postscripting  all  the free
     variables  and  postscripts  in a  line  to  the  ambiguous name
     introduced by application of ES to that line.

         (4)  Further restriction on variables of  generalization (EG
     and UG): The variable of generalization must not occur both free
     and as a postscript in the formula to which UG or EG is applied.

         Rules 5 and  6 below can be  summarized as follows:   Do not
     substitute a term that gets captured by a quantifier.

         (5)  Further restriction on terms  of US: When using  US, do
     not substitute a term one of whose variables becomes captured by
     a quantifier of the original formula.

         (6)  Analogous  restriction on  ES:  When using  ES,  do not
     substitute a variable that  becomes captured by a  quantifier of
     the original line.



 (5)  Quantifier Negation--QN, QNA, and QNE

         (i) NOT (E X) <denial of (...)> Dependencies {e,...,f}
iQNA    (j) (A X) (...)                 Dependencies {e,...,f}

 ----
         (i)  (A X) <denial of (...)>    Dependencies {e,...,f}

 iQNA    (j)  NOT (E X) (...)

 ----
         (i) NOT (A X)<denial of (...)>  Dependencies {e,...,f}

 iQNE    (j) (E X) (...)                 Dependencies {e,...,f}

 ----
         (i) (E X) <denial of (...)>     Dependencies {e,...,f}

 iQNE    (j) NOT (A X) (...)             Dependencies {e,...,f}