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:

  1. ¬Precedes*(0,0)
  2. Precedes+(0,b)
  3. Her([λz ¬Precedes*(z,z)], Precedes)

To prove (a), note that in the Proof of Theorem 2 (i.e., ¬∃x(Nx & 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) & Precedes is 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.

Proof of the Lemma on Predecessor

Copyright © 2013 by
Edward N. Zalta <zalta@stanford.edu>

Open access to the SEP is made possible by a world-wide funding initiative.
Please Read How You Can Help Keep the Encyclopedia Free


The SEP would like to congratulate the National Endowment for the Humanities on its 50th anniversary and express our indebtedness for the five generous grants it awarded our project from 1997 to 2007.