Stanford Encyclopedia of Philosophy

Supplement to Frege's Logic, 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

∃x Precedes*(x,0) → ∃x Precedes(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