Hints for Homework 8: Don't use multiplication; put everything into terms of addition and successor. Introducing New Predicates by Definition: I give permission to define predicates. If P is any formula in which only x occurs free, we can introduce a new predicate symbol New_Predicate with the defining axiom: (Ax.New_Predicate(x) <-> P) Notice that New_Predicate is a predicate symbol standing for the set {x | P} already introduced: New_Predicate(a) is equivalent to a E {x|P}, because either is equivalent to P[a/x]. For example, we could define a predicate of ``being zero'' as follows: Definition: Is_Null(x) <-> x = 0 The same principles apply to defining multi-place predicates: Definition of Order: x <= y <-> (Ez.x+z=y) This definition of the symbol <= is valid because the only free variables in the formula (Ez.x+z=y) are x and y and <= is a new symbol (in the Watson environment I have to use =< for this relation because <= is reserved for reverse theorem application :-( ) Similar rules apply to introducing new constants and function symbols by definition. Mr. Guha asked about recursive definitions; we will see later that we can justify recursive definitions, but they take a little extra work. Proofs in Class The rest of our time on Wednesday was spent doing proofs on the board. I wrote up the following facts that we know: Axioms: 1. (Ax. x' =/= 0) 2. (Axy. x'=y' -> x=y) 3. (Ax. x+0=x) 4. (Axy. x+y' = (x+y)') 5. (Ax. x*0 = 0) 6. (Axy. x*y' = x*y + x) Definitions: 1. 0'=1 (and so forth) 2. x=/=y is defined as ~(x=y) (notice that this is allowed by our rules of definition above) Theorems: 1. (Ax.x' = x+1) (On the basis of this theorem, I allow you to use the notations x' and x+1 interchangeably without comment) 2. (Ax.x+y=y+x) I exhibit the proofs given in class. These give examples of the kinds of abbreviated justifications (and reductions of numbers of lines) that are being allowed. Theorem 3: (Ax.x' =/= x) Prove this by induction on x. Goal (basis step): 0' =/= 0 1. 0' =/= 0 axiom 1, univ elim | 2. a' =/= a ind hyp | Goal: a'' =/= a' | | 3. a'' = a' subpremise for neg intro | | 4. a' = a axiom 2, univ elim twice, m.p. | | 5. a'=a & a'=/=a c.i. lines 2,4 | 6. a'' =/= a' neg intro lines 3-5 7. (Ax.x' =/= x) math induction, 1, 2-6 This is the first proof where we have brought Theorem 2 into play. Notice that we treat x=/=y logically exactly as if it were ~(x=y); we omit formal appeals to the definition of =/=. Theorem 4: (Axyz.x+z=y+z -> x=y) Notice that the converse implication is true by properties of equality, so we could prove the biconditional instead with very little more work. We prove this by induction on z. | 1. a=a, b=b arbitrary object intro | Goal: (Az.a+z=b+z->a=b) Prove this by induction on z. Notice that we do the induction proof inside the outermost box (a univ intro box); there was some confusion about this in class. | Goal (basis): a+0=b+0 -> a=b | 2. a+0=b+0 -> a=b axiom 3 with univ elim, twice; prop =; | obvious propositional tautology | | 3. a+c=b+c -> a=b ind hyp | | Goal: a+c'=b+c' -> a=b | | | 4. a+c'=b+c' subpremise for imp. intro. | | | 5. (a+c)' = (b+c)' axiom 4, univ. elim., prop. = | | | 6. a+c=b+c axiom 2, univ. elim. | | | 7. a=b ind. hyp (line 3), line 6, m.p. | | 8. a+c'=b+c' -> a=b imp. intro. lines 4-7 | 9. (Az.a+z=b+z->a=b) math. induction lines 2,3-8 10. (Axyz.x+z=y+z -> x=y) multiple univ. intro., lines 1-9 Comments: in line 2, we allow a line to be justified by the fact that it is an obvious propositional tautology; this is an allowed move henceforth. The proof by ``multiple univ. intro'' can easily be unpacked into two proofs by univ intro -- we need to open two nested boxes with separate arbitrary object intro lines, then put the quantifiers back on one at a time. | a=a, b=b arbitrary object intro | . | . | . | Pab who knows how? (Axy.Pxy) multiple univ. intro. is an abbreviation for | a=a a.o.i. | | b = b a.o.i. | | . | | . | | . | | Pab who knows how? | (Ay.Pab) univ. intro. (Ax.(Ay.Pxy)) (equivalently, (Axy.Pab)) univ. intro. We allow ourselves henceforth to introduce many arbitrary objects in a single box for a proof of a statement with many leading universal quantifiers. A comment on the box in the math induction derived rule: We know if we look at how the rule was derived that the box | Pa |. |. |. | Pa' in a math induction proof comes from the proof of the sentence (Ax.Px->Px') which our abbreviated format allows us to avoid writing down. In fact, this is a valid derived rule we might want to use on other occasions: | Pa | . | . | . | Qa (Ax.Px->Qx) where a occurs only in the box, is valid reasoning, as we see if we pretty up the packaging a bit: Goal:(Ax.Px->Qx) | a=a arbitrary object intro | Goal: Pa -> Qa | | Pa | | . | | . | | . | | Qa | Pa -> Qa imp. intro. previous box (Ax.Px->Qx) previous box On this basis, we allow reasoning like this: | Pa | . | . | . | Qa (Ax.Px->Qx) universal implication introduction (uii) prev. box. where a is a new variable (it does not occur outside the box). Just as in the math induction rule, we will use Greek letters for the new object, because it was an arbitrary object in the original reasoning.