2. Indirect Proof (IP) in Predicate Logic Indirect proof (IP) can be used in predicate logic proofs in much the same way as in propositional logic proofs. As usual, you will begin an indented indirect proof sequence by assuming the negation of the statement to be obtained. If you are then able to derive a contradiction from this assumption, the indirect proof sequence is discharged and you can assert the denial of the original assumption. The following example shows how to use indirect proof in predicate logic. 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. (3x)(Ax v Bx) (3x)CX (3x)CX (x)~AX ~(X)~AX (3X)AX Aa ~(3x) (Ax v Bx) (x)~ (Ax v Bx) ~(Aa v Ba) ~Aa ~Ba ~Aa Aa Aa / (x)~AX AIP 3 QN 4 EI 1,2 MT 6 QN 7 UI 8 DM 9 Simp 5,10 Conj 3-11 IP 1. 2. 3. 4. 5. 6. 7. 8. 9. (y)Ry> (y)My Me ~Re 10. ~Re Re (3y)Ry (y)My ~~Re ~Me Me Me. ~Me / ~Re (Use the following tabs if you need help remembering any of the natural deduction rules you have learned so far.) NATURAL DEDUCTION RULES AND PROOF METHODS Modus Ponens (MP) Simplification (Simp) Distribution (Dist) Modus Tollens (MT) Conjunction (Conj) Double Negation (DN) Pure Hypothetical Syllogism (HS) Disjunctive Syllogism (DS) Addition (Add) De Morgan's Rule (DM) Commutativity (Com) Transposition (Trans) Material Implication (Impl) Material Equivalence (Equiv) Exportation (Exp) Constructive Dilemma (CD) Associativity (Assoc) Tautology (Taut) Conditional Proof (ACP + CP) Indirect Proof (AIP + IP) Universal Instantiation (UI) Universal Generalization (UG) Existential Instantiation (El) Existential Generalization (EG) Quantifier Negation (QN) 7