#### Supplement to Frege's Theorem and Foundations for Arithmetic

## Proof that Q is Hereditary on the Natural Numbers

We want to prove the following claim:

HerOn(Q,N)

The proof of this claim appeals to the following Lemma (cf.
**Gg** I, Theorem 149):

Lemma on:Predecessor^{+}

Nx&Precedes(y,x) →

#[λzPrecedes^{+}(z,y)] = #[λzPrecedes^{+}(z,x) &z≠x]

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*,*N*), 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,#[λzPrecedes^{+}(z,n)]) →

Precedes(m,#[λzPrecedes^{+}(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,#[λzPrecedes^{+}(z,n)])

to show:

Precedes(m,#[λzPrecedes^{+}(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) #[λzPrecedes^{+}(z,m)] = #F

(3)m= #[λuFu&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:

[λzPrecedes^{+}(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:

#[λzPrecedes^{+}(z,m)] = #[λzPrecedes^{+}(z,m)],

which we know by the logic of identity.

To show (3) holds, we need to show:

(C)m= #[λuPrecedes^{+}(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[λzPrecedes^{+}(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:

#[λzPrecedes^{+}(z,n)] = #[λuPrecedes^{+}(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:

Nm&Precedes(n,m) →

#[λzPrecedes^{+}(z,n)] = #[λzPrecedes^{+}(z,m) &z≠m]

Since the consequent 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.