THERE ARE SOME TYPOS IN HOMEWORK 4, ASSIGNMENT 1 they are corrected in the posted version; I miswrote the right sides of distributive laws several times...
We continue the development of rules we didn't include in our basic list. 1. P -> Q premise 2. ~Q premise | 3. P premise of subproof | 4. Q modus ponens, lines 3,1 | 5. Q & ~Q conjunction introduction, lines 2,4 6. ~P negation introduction, lines 3-5. So (as promised above) we have the rule P -> Q ~Q -------- implication elimination 2 (modus tollens) ~P Now I develop Grantham's disjunction elimination rule: 1. P|Q premise 2. P->R premise 3. Q->R premise 4. | ~R premise of subproof 5. | ~P modus tollens, lines 2,4 6. | Q disjunction elimination 2, lines 1,5 7. | ~Q modus tollens, lines 3,4 8. | Q & ~Q conjunction introduction, lines 6,7 9. ~ ~R negation introduction, lines 4-8 10. R double negation elimination, line 9 which justifies the rule P | Q P -> R Q -> R ------- proof by cases R Note that I do not call this rule ``disjunction elimination''. In combination with implication introduction, this justifies the rule G |- P|Q G,P |- R G,Q |- R --------- proof by cases with subproofs G |- R which really captures the structure of a proof by cases. Development of New Rules from Proofs (reuse and modularity) Notice that every proof can be reinterpreted as a new rule! Rules for Biconditional and Xor Biconditional Xor P <-> Q P <-> Q P <+> Q P <+> Q P Q ~P ~Q -------- --------- ------- --------- Q P Q P G, P |- Q G, P |- ~Q or G, Q |- ~P G, Q |- P G, ~Q |- P or G, ~P |- Q --------- ------------------------ G |- P <-> Q G |- P <+> Q The rules have the names one expects; I won't care about numbering of these rules as we won't use them often. Rules for NAND and NOR are left to your imagination. A Rule We Do Not Have We do not have the ability to use biconditional theorems (equivalences) to ``substitute equals for equals'' as we did in our Boolean algebra formalization of propositional logic. (Such a rule is valid but it takes work to show this). Proof Strategy We number the lines in our proofs from the beginning forward to the end and we may try to prove theorems by writing down the premises and applying the rules in a forward direction with some success. But the best strategy for natural deduction is to work backwards from the goal to the theorem. The idea is to look at the topmost connective of the theorem we are trying to prove and think about what the previous step of the proof (which presumably uses the introduction rule for that connective) would look like. Of course, another possible way to prove a theorem is to assume its negation and try to prove a contradiction from it. Notice that our basic rules allow us three ways to prove a statement with a given propositional connective at the top: we can prove it using the introduction rule for that connective, we can find it as a component of a premise, or we can deduce it from a contradiction (anything can be deduced from a contradiction!). The last case is rather special, since we don't actually _believe_ any contradictions :-) An Example of Proof Development (Grantham proves the same formula in the book; our different treatment of disjunction makes our proof somewhat shorter). Goal: ~(A & B) -> (~A | ~B) The last step of the proof should be an implication introduction, appealing to a subproof in which ~(A&B) is the first line and ~A | ~B is the last. So we have the following proof sketch: | 1. ~(A&B) premise of subproof . . . | n. (~A | ~B) ??? n+1. ~(A & B) -> (~A | ~B) implication introduction, lines 1-n. Now we try the same goal-directed approach on the disjunction ~A | ~B: it should be proved by disjunction introduction in a subproof with hypothesis ~~A and conclusion ~B (or hypothesis ~~B and conclusion ~A, but this is symmetrical). | 1. ~(A & B) premise of subproof || 2. ~~A premise of subsubproof . . . || n-1. ~B ??? | n. (~A | ~B) disjunction introduction 2, lines 2-(n-1) n+1. ~(A & B) -> (~A | ~B) implication introduction, lines 1-n. Continuing, we think that the natural way to prove ~B is by negation introduction, using a proof with premise B and conclusion a contradiction. | 1. ~(A & B) premise of subproof || 2. ~~A premise of subsubproof ||| 3. B premise of subsubsubproof (!) . . . ||| n-2. Q & ~Q (we don't know what Q will be). ??? || n-1. ~B negation introduction, lines 3-(n-2) | n. (~A | ~B) disjunction introduction 2, lines 2-(n-1) n+1. ~(A & B) -> (~A | ~B) implication introduction, lines 1-n. The proof is now best completed by ``forward'' reasoning. | 1. ~(A & B) premise of subproof || 2. ~~A premise of subsubproof ||| 3. B premise of subsubsubproof (!) ||| 4. A double negation elimination, line 2 ||| 5. A&B conjunction introduction, lines 4,3 ||| 6. (A&B) & ~(A&B) conjunction introduction, lines 1,5 || 7. ~B negation introduction lines 3-6. | 8. (~A | ~B) disjunction introduction 2, lines 2-7 9. ~(A & B) -> (~A | ~B) implication introduction, lines 1-8. If we chose Q = A&B, the whole proof could be developed in the goal directed style, and it does seem that of the available formulas this might have been the best choice. Readers may like to see a completely ``boxed'' version: ---------------------------------------------------------------- | 1. ~(A & B) premise of subproof | |------------------------------------------------------------- | || 2. ~~A premise of subsubproof | | ||---------------------------------------------------------- | | ||| 3. B premise of subsubsubproof (!) | | | ||| 4. A double negation elimination, line 2 | | | ||| 5. A&B conjunction introduction, lines 4,3 | | | ||| 6. (A&B) & ~(A&B) conjunction introduction, lines 1,5 | | | ||---------------------------------------------------------- | | || 7. ~B negation introduction, lines 3-6 | | |------------------------------------------------------------- | | 8. (~A | ~B) disjunction introduction 2, lines 2-7 | ---------------------------------------------------------------- 9. ~(A & B) -> (~A | ~B) implication introduction, lines 1-8.