Notes for Friday, January 28 Re Homework 3: the tables + | 0 1 * | 0 1 ------- ------- 0 | 0 1 0 | 0 0 1 | 1 0 1 | 0 1 given in the assignment admit three interpretations relevant to the assignment: uninterpreted sets of integers logic interpretation dual logic interpretation 0 odd integers true false 1 even integers false true + addition <+> (xor) <-> (biconditional) * multiplication & (conjunction) | (disjunction) Because of the interpretation in the integers, we should be able to see that + and * are commutative and associative, 0 is the identity of +, 1 is the identity of *. The additional rules x+x=0 and xx = x can be verified by inspection. We claim that the constant 1 and operators + and * are enough to define all propositional connectives in the logic interpretation: translate ~x by 1+x, x&y by xy and x|y by x+y+xy We claim that the logical rules for this system described above are enough to verify translations of all the axioms of Boolean algebra, and we ask you to do the verification as exercise 1. Here's an example: Verify ~(x|y) == ~x & ~y First translate into the notation of this system: ~(x|y) translates to 1+(x+y+xy) ~x & ~y translates to (1+x)(1+y) then verify the equation 1+(x+y+xy) = (1+x)(1+y) between the translated expressions. (1+x)(1+y) = 1+x+y+xy by standard algebra manipulations (and it's enough to say that in this case; when the special rules x+x=0 and xx = x come into play one should be more explicit). Most of the laws of Boolean algebra listed in the notes should have short verifications; ones involving disjunction will be the most complicated. Exercise 2 requires you to think about the logical meaning of formulas like P<+>Q<+>R<+>S or P<->Q<->R<->S using this interpretation (actually, use the dual interpretation in the second case). In both cases, what you are thinking about is how to evaluate the sum of a list of 0's and 1's in this little algebra; a brief description of how to evaluate sums, filtered through the logical interpretations, gives a brief description (already known to some of you) of the truth values of propositional formulas of the two kinds indicated. Natural Deduction Now we will start to develop a style of formal reasoning in propositional calculus which is more closely related to the way we ``naturally'' reason (that's why I'll call it ``natural deduction''). Any formal reasoning involves drawing a conclusion from a set of premises. Where G is a set of formulas and C is a formula, we write G |- C if the truth of all the elements of the set G (premises) allows us to conclude that the formula C (the conclusion) is true. The meaning of this notation is related to but not identical to the meaning of the notation A |= B (A entails B). We call expressions of this kind ``derivations''. It is important to note that verification of assertions of the form G|-C will generally be on syntactical grounds; we consider manipulations of expressions (formal rules operating on syntax) rather than our knowledge of what the expressions are supposed to mean (semantics). Truth tables are an example of a semantically motivated method (though we have seen in our motivation of Boolean algebra that a syntax-driven approach can simulate truth table based reasoning). Some rules about valid derivations: G |- C when C is an element of G If G is a subset of H and G |- C then H |- C If G |- C1 and G u {C1} |- C2 then G |- C2 We can always take a premise as a valid conclusion, and adding more premises does not affect the validity of our conclusion. If we can draw a conclusion from a set of premises, we can add that conclusion to our set of premises and draw further conclusions (which will follow from our original set of premises). Now that we've introduced formal notation for these ideas, we'll speak a little more informally about rules related to our connectives. In any proof, we will have a theorem in mind to prove, which we will call our ``goal'', and some premises which we are allowed to use (which I may also call ``hypotheses''). For each propositional connective, we will have two different kinds of rules. ``Introduction rules'' for a connective allow us to prove a goal with that connective; ``elimination rules'' for a connective allow us to use premises with that connective. (The reasons for these names may not be entirely obvious). Let's start with the example of conjunction: To prove a conclusion of the form A & B it seems natural to prove A and then prove B, and the introduction rule for conjunction takes the form A B ------------- (conjunction introduction) A & B In terms of derivations, we can write this ``{A,B} |- A&B is a valid derivation for any formulas A,B'' If we have a premise of the form A & B, how can we use it? It seems that one can draw the simpler conclusion A or the simpler conclusion B (this seems to be all that one can do!) so we have two elimination rules A & B ------------- (conjunction elimination 1) A and A & B ------------- (conjunction elimination 2) B In terms of derivations, {A&B}|-A and {A&B}|-B are valid derivations where A and B are any formulas. Even with this simple set of rules, we can actually prove things: 1. A & B (premise) 2. A (conjunction elimination 1 on line 1) 3. B (conjunction elimination 2 on line 1) 4. B & A (conjunction introduction on lines 3,2) [a good question was raised at this point as to whether the order 3,2 is important here; I want to see if I can come up with an example of a rule where it is important to indicate the order of the arguments] from which we see that we can write {A & B} |- B & A The format of proof with lines used here can be justified using the properties of derivations given above. We leave as an instructive exercise for the reader the restatement of this proof in the language of derivations. We briefly introduce an elimination rule P P->Q ------- implication elimination 1 Q doubtless familiar to most of you as Modus Ponens. Another implication elimination rule is ~Q P -> Q ---------- implication elimination 2 ~P (not covered in lecture). We briefly introduce the implication introduction rule, which has new features. In derivation form, the rule is this: if G u {P} |- Q, then G |- P->Q In English, to prove an expression of the form P->Q, introduce P as a new premise, and prove Q. The new premise P cannot be used outside the context of this special proof. This rule has the curious feature of allowing proofs with no premises at all (no axioms): 1. P (premise for subproof ending at line 2) 2. P (copied from line 1) 3. P -> P (implication introduction, lines 1-2) Of course, there is a premise in this proof in line 1, but it is a premise of a subproof, not of the entire proof. In derivation form, this proof can be presented thus: {P} |- P (because P is an element of {P}) emptyset u {P} |- P (set theory -- emptyset is the identity of union) emptyset |- P->P (implication introduction) in which form it is clearer that P is not a true premise of the proof.