Proof of the Lemma on Predecessor⁺

We wish to prove the Lemma on Predecessor⁺, which asserts:

Lemma on Predecessor⁺:
Nx & Precedes(y,x) →
   #[λz Precedes⁺(z,y)] = #[λz Precedes⁺(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 Nn and Precedes(m,n). We want to show:

#[λz Precedes⁺(z,m)] = #[λz Precedes⁺(z,n) & z ≠ n]

By Hume's Principle, it suffices to show:

[λz Precedes⁺(z,m)] ≈ [λz Precedes⁺(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([λz Precedes⁺(z,m)]x ≡ [λz Precedes⁺(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.

Return to Proof that Q is Hereditary on the Natural Numbers