MATH3066 ALGEBRA AND LOGIC
Deduction Rules for the Propositional and Predicate Calculi
The Ten Rules of Deduction for the Propositional Calculus:
(1) Rule of Assumptions (A): Any wff may be written down as an assump- tion, depending only on itself.
(2) Modus Ponens (MP): Given V and V ⇒ W , we may deduce W , depending on the pooled assumptions for V and V ⇒ W .
(3) Modus Tollens (MT): Given ∼ W and V ⇒ W , we may deduce ∼ V , depending on the pooled assumptions for ∼ W and V ⇒ W .
(4) Double Negation (DN): Given ∼∼ W , we may deduce W , and given W we may deduce ∼∼ W , in each case depending on the same underlying assumptions.
(5) Conditional Proof (CP): Given V , introduced at some earlier step by Rule of Assumptions, and given W , relying on V as an underlying assump- tion, we may deduce V ⇒ W , discharging the assumption V , but relying on any remaining assumptions used to deduce W from V .
(6) ∧-Introduction (∧ I): Given V and W , we may deduce V ∧W , relying on the pooled assumptions for V and W .
(7) ∧-Elimination (∧ E): Given V ∧ W , we may deduce V or deduce W , relying on assumptions for V ∧ W .
(8) ∨-Introduction (∨ I): Given V , we may deduce V ∨ W or deduce W ∨ V for any W , relying on the assumptions for V .
(9) ∨-Elimination (∨ E): Given V ∨ W and two deductions of C , firstly from V , introduced by Rule of Assumptions, and secondly from W , intro- duced by Rule of Assumptions, we may deduce C again, but from V ∨ W , discharging the assumptions V and W , but pooling any assumptions for V ∨ W and any assumptions used to deduce C from V and C from W .
(10) Reductio ad Absurdum (RAA): Given V , introduced at some earlier step by Rule of Assumptions, and given the contradiction W ∧ ∼ W , relying on V as an underlying assumption, we may deduce ∼ V , discharging the assumption V , but relying on any remaining assumptions used to deduce W ∧ ∼ W from V .
The Four Extra Rules of Deduction for the Predicate Calculus:
(11) ∀-Introduction (∀ I): Given a wff W(b) , where b is a constant symbol that occurs at least once, we may deduce (∀x) W(x) , where x is a new variable that does not appear in W(b) and replaces b uniformly throughout W(b) , relying on the assumptions for W(b) , provided the symbol b does not appear in any wff in this list of underlying assumptions.
(12) ∀-Elimination (∀ E): Given a wff (∀x) W(x) , we may deduce W(b) , where b is a constant symbol replacing x uniformly throughout W(x) , re- lying on assumptions for (∀x) W(x) .
(13) ∃-Introduction (∃ I): Given a wff W(b) , where b is a constant symbol that occurs at least once, we may deduce (∃x) W(x) , where W(x) results from W(b) by replacing at least one occurrence of b by x, relying on the assumptions for W(b) .
(14) ∃-Elimination (∃ E): Given a wff (∃x) W(x) and a deduction of C from W(b), introduced by Rule of Assumptions, where b is a new constant symbol that replaces x uniformly throughout W(x) , we may deduce C again, but from (∃x) W(x) , discharging the assumption W(b) , but pooling any assumptions for (∃x) W(x) and any assumptions used to deduce C from W(b), provided b does not appear in C or in any of these underlying assumptions.