Predicates and Relations in the Language of Sets and Ordered Pairs We are now going to move into the realm of mathematical content, but we are first going to strengthen our logic. We will introduce the ability to talk about sets and ordered pairs, but we will do this in a restricted way which really only allows us to describe the predicates and relations we already have, but using different language. For any unary predicate symbol R, we allow x E R to be used to mean the same thing as Rx. For any binary predicate symbol Rxy, we allow (x,y) E R to be used to mean the same thing as Rxy, and similarly we allow n-ary predicate symbols to be expressed using n-tuples and membership E. For any formula T and term a, we allow a E {x | T[a/x]} to mean the same thing as T[a/x]. Formally speaking, we regard {x | T[a/x]} as a unary predicate symbol, but we only use it with the membership notation. Similarly, we allow the definition of binary predicates with notation like {(x,y) | T}. We comment that function notation (x |-> T) or ((x,y) |-> T) where T is a term can be used similarly to introduce new function symbols. If these notations are used, they can be used in the same contexts as function symbols. Note carefully what we do NOT allow. E is not a predicate symbol in the usual sense. x E y where x and y are variables is not a well-formed formula; only a predicate symbol or a set symbol can appear to the left of E. (It seems to me that confusion between E as the membership symbol and E as the universal quantifier in typewriter notation is unlikely; of course, these symbols both have quite different shapes on the blackboard or in a hypothetical future nicely type-set version of these notes.) Only a term or a pair or n-tuple can appear to the right of an E. Moreover, an n-tuple may appear only in the context to the right of a membership symbol with an n-ary predicate or set of n-tuples to the left. So far we have not strengthened our logic at all; we have just added some notation. Now we will strengthen it a lot! Quantification over Sets and Relations We allow n-ary predicate letters to be used as variables ranging over sets of n-tuples, and we allow quantification over set variables. The crucial point here is that the name spaces of regular variables and variables over sets of n-tuples (which are really n-place predicates in disguise) do not overlap. One might also allow quantification over n-place functions; the name spaces are again disjoint. The rules for reasoning with quantifiers over sets and n-place relations are the same as those for regular quantifiers; one may introduce arbitrary n-place relations or witnesses to existential hypotheses about relations, and one may instantiate set or relation variables with set symbols where appropriate. What I'm really doing here is introducing what is called ``second-order logic'' rather than set theory; I'm allowing quantifiers over predicates, but I'm doing it in a way that is likely to be notationally more familiar. The Paradox We Don't Meet The Russell paradox of set theory does not occur here. This paradox involves the set {x | ~x E x} of all sets that are not members of themselves, and this is not a legal expression for us (so far) because only a regular variable can appear in the context ``{x | ...}'' and only a unary predicate symbol or a set symbol or variable can appear in the context ``...E x''; the same letter x cannot play both of these roles! The Point of All This: We Introduce Some Mathematical Content Now we are going to introduce some mathematical content! We will study the theory of ``Peano arithmetic''. This is the theory of the natural numbers 0,1,2,3... stripped down to its most basic elements. (scholarly footnote: It should be observed that the system we introduce is really ``second-order Peano arithmetic'' because of our use of quantification over sets, but this is actually the system originally introduced by Peano, anyway.) We introduce primitive function symbols x' (for the successor x+1 of x) x+y and x*y (for which we assume familiar operator precedence conventions; also, we may abbreviate x*y as just xy as usual) and the following basic axioms: 1. (Ax. ~x'=0) 2. (Ax.(Ay.x = y <-> x' = y')) 3. (Ax.x+0 = x) 4. (Ax.(Ay.x+(y') = (x+y)')) 5. (Ax.(Ay.x*0 = 0)) 6. (Ax.(Ay.x*(y') = (x*y)+x)) These axioms look remarkably minimal! We look in vain for such familiar things as the commutativity of addition, for example! The real power lies in the following familiar principle: Axiom of Mathematical Induction: (AS.(0 E S & (Ax.x E S -> x' E S)) -> (Ay.y E S)) This says that any set S which contains 0 and is closed under the successor operation contains all elements of our universe (that is, all the natural numbers). We are mostly going to confine our use of sets to applications of induction, at least for a while, though I _may_ take a detour in which I show that the existence of the operations + and * can be proved using just axioms 1-2 and the axiom of induction, which will involve a more sophisticated use of our logic. This allows us to continue our exploration of ``foundational'' aspects of mathematics by examining the development of some familiar mathematics from the ground up, and begin the ``discrete'' component of our course by working with mathematical induction. A basic caution here: in what follows, we may only use mathematical principles that we have actually proved! There is a danger in working with what _looks_ like familiar material that we may smuggle in things that we ``know'' but have not proved... Definition: We define 1 as 0'. Similarly, we define 2 as 1', 3 as 2' and so forth. Exercise (optional): submit a formal definition of our usual notation for natural numbers in terms of the primitive notation. Theorem 1: (Ax.x+1 = x') Proof: Let a be arbitrary. a+1 = a+0' (by definition of 1) = (a+0)' (by axiom 4) = a' (by axiom 3); since a was arbitrary we have proved (Ax.x+1 = x'). We examine a completely formal proof. Our axioms are available as premises in any proof; we introduce them by name rather than supplying them with line numbers. Goal: (Ax.x+1 = x') | 1. a=a arbitrary object intro | 2. a+1 = a+1 equality intro | 3. a+1 = a+0' equality elim, line 2 and definition of 1 | 4. a+0'=(a+0)' univ. elim., axiom 4 | 5. a+1 = (a+0)' equality elim, lines 3,4 | 6. a+0 = a univ. elim., axiom 3 | 7. a+1 = a' equality elim, lines 5,6 8. (Ax.x+1 = x') univ. intro, lines 1-7 You should observe that the formal proof is essentially the same proof, except that we are being careful to the point of being paranoid. In particular, the maneuver of proving a universal statement by introducing an arbitrary object (the univ. intro. rule) is present in the English just as in the formal proof. Our First Induction Proof Theorem 2: Every nonzero number has a predecessor. First we put this into mathematical notation: a predecessor for x is a number y such that y+1 = x, or y' = x. To say that every number has a predecessor is to say that for each x, there is a y such that y' = x. Theorem 2 (in logical notation): (Ax.(~x=0)-> (Ey.y'=x)) We want to prove this by induction. A proof by induction has the following form: Goal: (Ax.x E P) Goal: 0 E P (basis step) . . . n. 0 E P ??? Goal: (Ax.x E P -> x' E P) (induction step) . . . n+i (Ax.x E P -> x' E P) ??? n+i+1. 0 E P & (Ax.x E P -> x' E P) c.i. lines n-(n+i) n+i+2. (0 E P & (Ax.x E P -> x' E P)) -> (Ay.y E P) univ. elim., axiom of induction n+i+3. (Ay.y E P) Of course, since this is an important form of proof, we introduce a derived rule: 0 E P (Ax.x E P -> x' E P) --------------------- mathematical induction, set form (Ay.y E P) which will allow the omission of the tedious (and often rather long!) lines n+i+1 and n+i+2 or the following form without set notation: P[0/z] (Ax.P[x/z] -> P[x'/z]) ----------------------- mathematical induction, property form (Ay.P[y/z]) This is proved by replacing the set P in the set form with the set notation {x | P[x/z]} and appealing to the definition of set notation. Although we stated the math induction axiom in terms of sets, we will initially work with the property-based derived rule. We will come back to what induction has to say about sets when we talk about such things as the Least Number Principle. Now back to our specific theorem: Goal: (Ax.~x=0->(Ey.y' = x)) If we do this in set form, we will talk about the set {x | ~x=0->(Ey.y' = x)} a lot, and I would rather not do that. Let P be the formula ~z=0->(Ey.y'=z) Goal (basis step): ~0=0->(Ey.y'=0) (this is P[0/z]) | 1. ~0=0 subpremise | 2. 0=0 equality intro | 3. (Ey.y'=0) neg. intro. lines 1,2 an absurd conclusion is drawn from an absurd premise! 4. ~0=0->(Ey.y'=0) imp. intro. lines 1-3 (basis step complete) Goal (induction step): (Ax.(~x=0->(Ey.y' = x))->(~x'=0->(Ey.y' = x'))) This is (Ax.P[x/z]->P[x'/z]). | 5. a=a arbitrary object intro | Goal: (~a=0->(Ey.y' = a))->(~a'=0->(Ey.y' = a')) | | 6. ~a=0->(Ey.y' = a) subpremise This subpremise in an induction proof has a name: it is called the ``inductive hypothesis''. | | Goal: ~a'=0->(Ey.y' = a') We observe that ~a'=0 is true (it is an instantiation of axiom 1), which suggests that our goal is not really this but this: | | Goal: (Ey.y' = a') which is easy to prove: | | 7. a' = a' eq. intro. | | 8. (Ey.y'=a') exist. intro. | | 9. ~a'=0->(Ey.y' = a') true conclusion, line 8 (this is why we don't need an imp. intro. box) | 10. (~a=0->(Ey.y' = a))->(~a'=0->(Ey.y' = a')) imp. intro. lines 6-9 11. (Ax.(~x=0->(Ey.y' = x))->(~x'=0->(Ey.y' = x'))) univ. intro. lines 5-10 (induction step complete) 12. (Ax.~x=0->(Ey.y' = x)) math induction, property form, 4,11 Note that the conclusion is (Ax.P[x/z]), as we expect. The form of the proof suggests an evem more streamlined derived rule of mathematical induction: G |- P[0/z] G, P[a/z] |- P[a'/z] where a does not appear in G _________________________________________________ G |- (Ax.P[x/z]) In terms of boxes, this looks like this: n. P[0/z] ??? (basis step proved) | n+1. P[a/z] subpremise (inductive hypothesis) | . | . | . | n+i. P[a'/z] ??? n+i+1. (Ax.P[x/z]) math induction, n, (n+i)-(n+i) This is stripped to the essentials; but you should be able to see that the box is the essential core of a proof by imp. intro. and univ. intro. of (Ax.P[x/z] -> P[x'/z]). This proof in English is in my opinion one of those proofs that is so easy that it is hard (this is my reason for giving the formal proof first!) Theorem 2 (English version): Every nonzero number has a predecessor. We prove this by induction. The assertion says of every number that if it is not zero, it has a predecessor. This assertion is trivially true of 0, which completes the basis step. Now we assume for some n that if n is nonzero, n has a predecessor, and we show that the same is true for n'. If n' is nonzero (which is obviously true by axiom 1!), then n' has a predecessor (namely, n!) so the result follows by mathematical induction. The reason that I believe this proof can be so hard to follow for some readers is that no use at all is made of the inductive hypothesis; this feature is reflected in the formal proof (in fact, the formal proof is the same proof, in all essential features!). In fact, it is even worse: the conclusion to be drawn from the unused inductive hypothesis is an implication (if n' is nonzero then n' has a predecessor) in whose proof the antecedent is ignored! Question: what have we NOT proved that we might suppose is implied by the English assertion ``Every nonzero number has a predecessor''?