#### 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:The proof of this claim appeals to the following Lemma (cf.HerOn(Q,N)

**Gg**I, Theorem 149):

Intuitively, the Lemma on PredecessorLemma on:Predecessor^{+}

Nx&Precedes(y,x) →

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

^{+}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:

∀If we replace ‘n∀m[Precedes(n,m) → (Qn→Qm)]

*Q*’ with its definition and simplify the result by λ-Conversion, then what we have to show is:

∀(Intuitively, we have to show that ifn∀m(Precedes(n,m) →

Precedes(n,#[λzPrecedes^{+}(z,n)]) →Precedes(m,#[λzPrecedes^{+}(z,m)])

*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)to show:Precedes(n,m)

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

By the definition of Predecessor, we have to show that there is a conceptPrecedes(m,#[λzPrecedes^{+}(z,m)])

*F*and object

*x*such that:

(1)We can demonstrate that there is anFx

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

(3)m= #[λuFu&u≠x]

*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:

[λBut we know, from the definition ofzPrecedes^{+}(z,m)]m

*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:

#[λwhich we know by the logic of identity.zPrecedes^{+}(z,m)] = #[λzPrecedes^{+}(z,m)],

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

(C)[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 form= #[λuPrecedes^{+}(u,m) &u≠m]

*F*in (3)):

[λIn what follows, we use the simplified version of this λ-expression.]u[λzPrecedes^{+}(z,m)]u&u≠m]

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:

#[λBut we can demonstrate this by appealing to the Lemma on PredecessorzPrecedes^{+}(z,n)] = #[λuPrecedes^{+}(u,m) &u≠m]

^{+}mentioned at the outset. We may instantiate the variables

*x*and

*y*in this Lemma to

*m*and

*n*, respectively, yielding:

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.Nm&Precedes(n,m) →

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

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