========================================================================= WARNING: THIS IS A VERY LONG DOCUMENT! ========================================================================= Homework #4 had the following problem, with the following solution: ------------------------------------------------------------------------- PROBLEM: -------- Given the following, can you prove that the unicorn is mythical? How about magical? Horned? If the unicorn is mythical, then it is immortal, but if it is not mythical, then it is a mortal mammal. If the unicorn is either immortal or a mammal, then it is horned. The unicorn is magical if it is horned. In doing this problem, you might find the following additional rules of inference for the natural-deduction system that I am introducing in lecture to be useful: vIntro: From P From Q ----------- ----------- Infer (PvQ) Infer (PvQ) vElim: From (PvQ) From (PvQ) and ~P and ~Q ---------- ---------- Infer Q Infer P <->Intro: From (P -> Q) From (P -> Q) and (Q -> P) and (Q -> P) --------------- --------------- Infer (P <-> Q) Infer (Q <-> P) <->Elim: From (P <-> Q) From (P <-> Q) -------------- -------------- Infer (P -> Q) Infer (Q -> P) ------------------------------------------------------------------------ SOLUTION: --------- Using the following syntax and semantics: [[MYTH]] = the unicorn is mythical [[MORT]] = the unicorn is mortal [[MAMM]] = the unicorn is a mammal [[HORN]] = the unicorn is horned [[MAGIC]] = the unicorn is magical represent the argument as follows: 1. MYTH -> ~MORT 2. ~MYTH -> (MORT ^ MAMM) 3. (~MORT v MAMM) -> HORN 4. HORN -> MAGIC Then argue as follows (I will leave it to you to fill in the missing steps): 5. ~MYTH -> MAMM ; from 2 6. (MYTH v ~MYTH) -> (~MORT v MAMM) ; from 1, 5 7. HORN ; from 3, 6 8. MAGIC ; from 4, 7 So HORN and MAGIC can be inferred. But MYTH cannot: If MYTH is F and MORT, MAMM, HORN, and MAGIC are all T, then the premises are all T, but MYTH is F. So the truth-value of MYTH need not be T even if all the premises are T. ------------------------------------------------------------------------ The syntactic proof above is really just a sketch of a formal proof. The gaps need to be filled in. In particular, I need to show you how it can be done in *our* system of propositional logic, which is a bit more "austere" (or "sparse") than the one used in the solution, since our system only has 2 inference rules per connective: one for introducing it and one for eliminating it. But there are many other valid patterns of reasoning that allow you to introduce or eliminate connectives, and these can be used *as if* they were rules of inference. I will give the proof in our system below. Some of the steps are justified by additional rules of inference of the sort just mentioned. So I'll also have to state and justify those rules. I'll do that *after* I show you the proof. Given lines 1-4 above as the premises of our argument, we want to: Show (HORN ^ MAGIC): To do that, let's first show HORN (and then show MAGIC). To do *that*, let's first show: ~MORT v MAMM. And to do *that*, let's first show: (MYTH v ~MYTH) -> (~MORT v MAMM). AND... to do *that*, let's first show: ~MYTH -> MAMM: That's a conditional statement, so we need to enter a subproof for ->Intro: *5. ~MYTH // temporary premise for ->Intro *6. ~MYTH -> (MORT ^ MAMM) // send 2 *7. MORT ^ MAMM // 6,5, ->Elim *8. MAMM // 7, ^Elim *9. ~MYTH -> MAMM // 5,8, ->Intro 10. ~MYTH -> MAMM // return 9 (= line 5 of answer above); // note that this *did* depend on line 2 // just as answer-line 5 says 11. (MYTH v ~MYTH) -> (~MORT v MAMM) // 1,10, Constructive Dilemma; // what's "Constructive Dilemma"? // see below; // note that this line 11 = line 6 // of the answer above; // note also that it does depend // on lines 1 & 10 (= answer line 5) 12. MYTH v ~MYTH // Theorem (what's that? see below) 13. ~MORT v MAMM // 11, 12, ->Elim 14. HORN // 3, 13, ->Elim (= line 7 of answer); // note that it does depend on line 3 Show MAGIC: 15. MAGIC // 4, 14, ->Elim QED. Now, what are "Constructive Dilemma" & "Theorem"? They are "derivable rules of inference", i.e., rules of inference that can be proved using the other rules of inference, so that we really don't need them--they are eliminable. But they can be added to our stock of inference rules as "shortcuts". They are, in fact, "macros": Every occurrence of them in a proof can be replaced by "expanding the macro", i.e., by replacing them by their proofs as instantiated for the specific case in which they're used. Here are those 2 rules, and their proofs (each of which involves yet other "macro" derivable rules of inference!): Constructive Dilemma: From (P -> Q) & (R -> S) ------------------------ Infer (P v R) -> (Q v S) [Note that this is another ->Intro rule, since it shows you how to produce a (particularly complex) conditional wff] Proof: 1. P->Q // premise 2. R->S // premise Strategy: Assume PvR & show QvS by ->Intro: *3. PvR // temporary premise for ->Intro Show QvS; strategy: Use ~Elim **4. ~(QvS) // temporary premise for ~Elim **5. ~Q ^ ~S // 4, DeMorgan's Law-1; that's another macro!; see below **6. ~Q // 5, ^Elim **7. P->Q // send 1 **8. ~P // 7, 6, Modus Tollens; yet another macro!; see below **9. ~S // 5, ^Elim **10. R->S // send 2 **11. ~R // 10, 9, Modus Tollens **12. ~P ^ ~R // 8, 11, ^Intro **13. ~(PvR) // 12, DeMorgan's Law-2; still yet another macro; see below **14. PvR // send 3 **15. QvS // 4, 13, 14, ~Elim *16. QvS // return 15 *17. (PvR) -> (QvS) // 3, 16, ->Intro 18. (PvR) -> (QvS) // return 17 QED. "Theorem": You may infer (P v ~P) at any time. (This rule is often called "Tautology", but that's a semantic term, and we're in the realm of syntax right now, so I prefer to call this "Theorem", which is a syntactic term). [Note that this is another "vIntro" rule, of a very special kind] Proof: Show: (P v ~P) Strategy: Use ~Elim *1. ~(P v ~P) // temporary premise for ~Elim *2. ~P ^ ~~P // 1, DeMorgan's Law-1 (there it is again; see below) *3. ~P // 2, ^Elim *4. ~~P // 2, ^Elim *5. (P v ~P) // 1, 3, 4, ~Elim 6. (P v ~P) // return 5 QED. Now for the derivable rules that we used to derive the above derivable rules: DeMorgan's Law-1: From ~(PvQ) --------------- Infer (~P ^ ~Q) [Note that this is another "^Intro" rule] Proof: 1. ~(PvQ) // premise Strategy: Show ~P; then show ~Q. Strategy to show ~P: Use ~Intro: *2. P // temporary premise for ~Intro *3. ~(PvQ) // send 1 *4. PvQ // 2, vIntro *5. ~P // 2,3,4, ~Intro 6. ~P // return 5 Show ~Q; strategy: Use ~Intro: *7. Q // temporary premise for ~Intro *8. ~(PvQ) // send 1; note that we have to do this again; // we can't re-use line 3, // since it's in a different subproof *9. PvQ // 7, vIntro; note that we can't re-use line 4, either *10. ~Q // 7,8,9, ~Intro 11. ~Q // return 10 12. (~P ^ ~Q) // 6,11, ^Intro QED. While we're at it, let's also show that DeMorgan's Law works in the other "direction" (and there are other DeMorgan Laws: for distributing ~ over v): DeMorgan's Law-2: From (~P ^ ~Q) -------------- Infer ~(PvQ) [Note that this is another "~Intro" rule] Proof: 1. (~P ^ ~Q) // premise Show ~(PvQ); strategy: use ~Intro *2. PvQ // temporary premise for ~Intro *3. (~P ^ ~Q) // send 1 *4. ~P // 3, ^Elim *5. Q // 2,4, vElim // (this is one of our "primitive" rules; see above) *6. ~Q // 3, ^Elim *7. ~(PvQ) // 2,5,6, ~Intro 8. ~(PvQ) // return 7 QED. Modus Tollens: From (P->Q) & ~Q ----------- Infer ~P [Note that this is yet another "~Intro" rule] Proof: 1. (P->Q) // premise 2. ~Q // premise Show ~P; strategy: Use ~Intro *3. P // temporary premise for ~Intro *4. (P->Q) // send 1 *5. Q // 4,3 ->Intro (also known as "Modus Ponens") *6. ~Q // send 2 *7. ~P // 3,5,6, ~Intro 8. ~P // return 7 QED. That "discharges" all of our derived rules. So, if you *really* want to see the proof of HORN ^ MAGIC, simply insert appropriate instantiations of the proofs of these rules into the proof of HORN ^ MAGIC (and, in some cases, you will need to insert appropriate instantiations of the proofs of some of these rules into the proofs of others of these rules!). That's why it's nice to have macros! (And why it's nice to have derived rules of inference.) Whew!