####
Stanford Encyclopedia of Philosophy

Supplement to Frege's Logic, Theorem, and Foundations for Arithmetic

## Proof that Q is Hereditary on the Natural Numbers

We want to prove the following claim:
*HerOn*(*Q*,)

The proof of this claim appeals to the following Lemma
(cf. **Gg** I, Theorem 149):
**Lemma on ***Predecessor*^{+}:

*x* & *Precedes*(*y*,*x*)

#[*z* *Precedes*^{+}(*z*,*y*)] =
#[*z* *Precedes*^{+}(*z*,*x*) & *z* *x*]
(Proof of the Lemma on *Predecessor*^{+})

Intuitively, the Lemma on Predecessor^{+} tells us that if
*y* precedes a number *x*, then
#[*z* *z**y*] is
identical to
#[*z*
*z**x* &
*z**x*].
Now to show *HerOn*(*Q*,), we have to
show:

*n**m*[*Precedes*(*n*,*m*) (*Qn* *Qm*)]

If we replace ‘*Q*’ with its definition and simplify the result
by -Conversion, then what we have to show is:
*n**m*(*Precedes*(*n*,*m*)

*Precedes*(*n*,#[*z* *Precedes*^{+}(*z*,*n*)])
*Precedes*(*m*,#[*z* *Precedes*^{+}(*z*,*m*)])

(Intuitively, we have to show that if *n* precedes *m*,
then if *n* precedes the number of numbers less than or equal to
*n*, then *m* precedes the number of numbers less than or
equal to *m*.) So, letting *n* and *m* be arbitrary, we
assume both:
(A) *Precedes*(*n*,*m*)

(B) *Precedes*(*n*,#[*z* *Precedes*^{+}(*z*,*n*)])

to show:
*Precedes*(*m*,#[*z* *Precedes*^{+}(*z*,*m*)])

By the definition of Predecessor, we have to show that there is a concept *F* and object *x* such that:
(1) *Fx*

(2) #[*z* *Precedes*^{+}(*z*,*m*)] = #*F*

(3) *m* = #[*u*
*Fu* & *u*
*x*]

We can demonstrate that there is an *F* and *x* for which
(1), (2) and (3) hold if we pick *F* to be
[*z*
*Precedes*^{+}(*z*,*m*)] and pick *x* to be
*m*. We now establish (1), (2), and (3) for these choices.
To show that (1) holds, we have to show:

[*z*
*Precedes*^{+}(*z*,*m*)]*m*

But we know, from the definition of *Precedes*^{+},
that *Precedes*^{+}(*m*,*m*). So by abstraction using
-Conversion, we are done.
To show that (2) holds, we need do no work, since our choice of *F* requires us to show:

#[*z* *Precedes*^{+}(*z*,*m*)] =
#[*z* *Precedes*^{+}(*z*,*m*)],

which we know by the logic of identity.
To show (3) holds, we need to show:

(C) *m* = #[*u*
*Precedes*^{+}(*u*,*m*) & *u*
*m*]

[Note that the -expression in the above has been
simplified by applying
-Conversion to the following (which, strictly
speaking, is what results when you substitute our choice for *F*
in (3)):
[*u* [*z*
*Precedes*^{+}(*z*,*m*)]*u*
& *u* *m*]

In what follows, we use the simplified version of this
-expression.]
Now in virtue of (A), (B) and the functionality of Predecessor (the
proof of which was left as an exercise in the subsection No Two
Numbers Have the Same Successor in §5), we know *m* =
#[*z*
*Precedes*^{+}(*z*,*n*)]. So, substituting
for *m* in (C), we have to show:

#[*z*
*Precedes*^{+}(*z*,*n*)] =
#[*u*
*Precedes*^{+}(*u*,*m*) & *u*
*m*]

But we can demonstrate this by appealing to the Lemma on
Predecessor^{+} mentioned at the outset. We may instantiate the
variables *x* and *y* in this Lemma to *m* and
*n*, respectively, yielding:
*m* & *Precedes*(*n*,*m*)

#[*z*
*Precedes*^{+}(*z*,*n*)] =
#[*z*
*Precedes*^{+}(*z*,*m*) & *z*
*m*]

Since the consequence is what we had to show, we are done, for the
conjuncts of the antecedent are things we assumed to be true at the
beginning of our conditional proof.
Return to Frege's Logic, Theorem, and Foundations for Arithmetic

Copyright © 1998, 1999 by

Edward N. Zalta

*zalta@stanford.edu*
*First published: June 10, 1998*

*Content last modified: November 22, 1999*