We discussed problem 1 in Homework 4; I'm not going to reproduce the discussion here, but we are going to do a fully worked out example in class on Wednesday, so that it is clear what is wanted. Reasoning justified in minute detail, as in Homework 4 or in the natural deduction proofs we are getting into, is not being presented as a style of proof we should normally do all the time; the reason for studying this is to see what principles underlie our usual reasoning. We discussed Exercise 2 in Homework 3, which I am going to ignore, since no one seemed to understand what I wanted: the idea is that a sentence P <+> Q <+> R <+>... linked by xor translates in the ``mod 2 arithmetic'' system to the sum P+Q+R... Such a sum is equal to 1 just in case an odd number of the summands are equal to 1. Thus the propositional formula is true (the interpretation of 1) just in case an odd number of the formulas linked by xor are true. Then we look at chained biconditionals: P <-> Q <-> R <->... will be interpreted by P+Q+R... in the dual interpretation of the ``mod 2 arithmetic'' system, in which 0 stands for true and 1 for false. A sum will equal 0 if an even number of the summands are equal to 1; using this dual interpretation, we see that the propositional formula will be true (have value 0) just in case an even number of the formulas in the chain of biconditionals are false (have value 1). So the mod 2 arithmetic interpretation can be used to clarify the meanings of chains of propositions linked by the associative operations <-> and <+>. Homework 3 is an example of the interpretation of one mathematical system inside another; this phenomenon occurs regularly in math and probably in CS, and it's useful to have practice reasoning about it. I put some additional rules on the board, but none were actually used in example proofs that did not appear in the notes for the first lecture, so I'll save new rules for the ``official'' list to appear in a future set of notes (one hopes the notes for tomorrow!) The example proofs we did in class: Prove |- (P & Q) -> P (this is a tautology; this proof will have no top-level premises). Proof: | 1. P&Q premise of subproof | 2. P by line 1, conjunction elimination 1 3. (P&Q)->P by lines 1-2, implication introduction Prove {P->Q,Q->R} |- P->R We first write down the two premises: 1. P-> Q premise 2. Q -> R premise Someone suggested using an elimination rule here, but we don't have one that applies (modus ponens and modus tollens don't help us). Suppose that we temporarily assume P 3. P Then we can add more lines 4. Q by modus ponens, lines 3,1 5. R by modus ponens, lines 4,2 But the structure consisting of lines 1-5 as we have written them is not a proof. Here's how it really works: 1. P-> Q premise 2. Q -> R premise | 3. P premise of subproof | 4. Q by modus ponens, lines 3,1 | 5. R by modus ponens, lines 4,2 6. P->R by implication introduction, lines 3-5. in which it is clear that the assumption in line 3 is doing something quite different from the assumptions in lines 1 and 2. The | characters in the margin are used to indent the subproof. I could be more fulsome and put them in a box: 1. P-> Q premise 2. Q -> R premise ---------------------------------- | 3. P premise of subproof | | 4. Q by modus ponens, lines 3,1| | 5. R by modus ponens, lines 4,2| ---------------------------------- 6. P->R by implication introduction, lines 3-5. But I hope that the more economical convention will be clear enough. Another numbering convention would make it clearer that the block is a unit: 1. P-> Q premise 2. Q -> R premise -------------------------------------- | 3.1 P premise of subproof | | 3.2 Q by modus ponens, lines 1, 3.1| | 3.3 R by modus ponens, lines 2, 3.2| -------------------------------------- 4. P->R by implication introduction, ``line 3'' In any event, one cannot use any line inside a block outside that block, but note that lines 1 and 2 are available inside the block. Scoping conventions like this should be familiar from programming languages.