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

## Proof That No Number Ancestrally Precedes Itself

We wish to prove:

Lemma: No Number Ancestrally Precedes Itself

∀x[Nx→ ¬Precedes*(x,x)]

*Proof*. Assume *Nb*, to show:
¬*Precedes**(*b*,*b*).
Now Fact 7 concerning *R*^{+} is:

[Fx&R^{+}(x,y) &Her(F,R)] →Fy

So we know the following instance of Fact 7 is true, where *x* = 0,
*y* is *b*, *F* is [λ*z*
¬*Precedes*^{*}(*z*,*z*)], and
*R* is *Precedes*:

([λz¬Precedes^{*}(z,z)]0 &Precedes^{+}(0,b) &

Her([λz¬Precedes^{*}(z,z)],Precedes)) → [λz¬Precedes^{*}(z,z)]b

By λ-Conversion on various terms in the above, this reduces to:

[¬Precedes^{*}(0,0) &Precedes^{+}(0,b) &

Her([λz¬Precedes^{*}(z,z)],Precedes)] → ¬Precedes^{*}(b,b)

So to establish ¬*Precedes*^{*}(*b*,*b*), we need to show each of the
following conjuncts of the antecedent:

- ¬
*Precedes*^{*}(0,0) *Precedes*^{+}(0,*b*)*Her*([λ*z*¬*Precedes*^{*}(*z*,*z*)],*Precedes*)

To prove (a), note that in the Proof of Theorem 2
(i.e., ¬∃*x*(*N**x* &
*Precedes*(*x*,0))), we established that
¬∃*x*(*Precedes*(*x*,0)).
But it is an instance of Fact 4 concerning *R*^{*},
that

∃xPrecedes^{*}(x,0) → ∃xPrecedes(x,0).

It therefore follows that
¬∃*x*(*Precedes*^{*}(*x*,0)).
So ¬*Precedes*^{*}(0,0).

We know (b) by our assumption that *Nb* and the definition
of *N*.

To establish (c), we have to show:

∀x,y(Precedes(x,y) →

([λz¬Precedes^{*}(z,z)]x→ [λz¬Precedes^{*}(z,z)]y))

That is, by λ-Conversion, we have to show:

∀x,y(Precedes(x,y) → (¬Precedes^{*}(x,x) → ¬Precedes^{*}(y,y)))

And by contraposition, we have to show:

∀x,y(Precedes(x,y) → (Precedes^{*}(y,y) →Precedes^{*}(x,x)))

So assume *Precedes*(*a*,*b*) and
*Precedes*^{*}(*b*,*b*). If we
show *Precedes*^{*}(*a*,*a*), we are
done. We know the following instance of Fact 8
concerning *R*^{+}, where *a* is substituted
for *z*, *b* for *y*, *b* for *x*,
and *Precedes* for *R*:

Precedes^{*}(b,b) &Precedes(a,b) &Precedesis 1–1 →

Precedes^{+}(b,a)

Since we have assumed *Precedes*^{*}(*b*,*b*) and
*Precedes*(*a*,*b*), and we have proven in the
main text that *Predecessor* is 1–1, we can use the
instance of Fact 8 to
conclude *Precedes*^{+}(*b*,*a*).
But the following is an instance of Fact 2 concerning *R*^{+},
when *a* is substituted for *x*, *b* for *y*,
*a* for *z*, and *R* is *Precedes*:

Precedes(a,b) &Precedes^{+}(b,a) →Precedes^{*}(a,a)

But we know *Precedes*(*a*,*b*) by assumption
and we have just shown *Precedes*^{+}(*b*,*a*).
So *Precedes*^{*}(*a*,*a*), and we are done.