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

## Proof of the Lemma on Predecessor^{+}

We wish to prove the Lemma on Predecessor^{+}, which asserts:

Lemma on:Predecessor^{+}

Nx&Precedes(y,x) →

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

Now this Lemma can be proved with the help of the following Lemma:

Lemma: No Number Ancestrally Precedes Itself

∀x[Nx→ ¬Precedes*(x,x)](Proof of the Lemma that No Number Ancestrally Precedes Itself)

Now to prove the Lemma on Predecessor^{+}, assume that
*N**n* and *Precedes*(*m*,*n*). We
want to show:

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

By Hume's Principle, it suffices to show:

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

Now it is a fact about equinumerosity (see the Facts About Equinumerosity, in §3, Equinumerosity, Fact 1) that if two concepts are materially equivalent, then they are equinumerous. It therefore suffices to show that

∀x([λzPrecedes^{+}(z,m)]x≡ [λzPrecedes^{+}(z,n) &z≠n]x)

And by λ-Conversion, it suffices to show:

∀x[Precedes^{+}(x,m) ≡Precedes^{+}(x,n) &x≠n]

So let us pick an arbitrary object, say *a*, and show:

Precedes^{+}(a,m) ≡ (Precedes^{+}(a,n) &a≠n)

(→) Assume
*Precedes*^{+}(*a*,*m*). Then from our
assumption that *Precedes*(*m*,*n*) and a Fact
about *R*^{+} (see §4, Weak Ancestral, Facts About
*R*^{+}, Fact 3), it follows that
*Precedes**(*a*,*n*). *A fortiori*, then,
*Precedes*^{+}(*a*,*n*). Now by the Lemma
mentioned at the outset of this proof, namely, No Natural Number
Ancestrally Precedes Itself, we know that
¬*Precedes**(*n*,*n*). Since *a*
ancestrally precedes *n* and *n* does not, it follows
that *a* ≠ *n*. We have therefore proved what we were
after, namely:

Precedes^{+}(a,n) &a≠n

(←) Assume *Precedes*^{+}(*a*,*n*)
and *a* ≠ *n*. By definition, the first conjunct tells
us that either *Precedes**(*a*,*n*) or *a*
= *n*. Since we know by assumption that the latter disjunct is
not true, we know *Precedes**(*a*,*n*). But from
this fact, the fact that Predecessor is 1-1, and our assumption that
*Precedes*(*m*,*n*), it follows from a fact about
*R*^{+} (see §4, Weak Ancestral, Facts About
*R*^{+}, Fact 8), that
*Precedes*^{+}(*a*,*m*), which is what we
had to show.