next up previous
Next: Monday, March 6, 2000 Up: Lecture Notes Previous: Notes for March 1,

March 3, 2000

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''?



Randall Holmes
2000-05-05