This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Proof of the Lemma on Predecessor+

The Lemma on Predecessor+ can be proved with the help of the following Lemma:

Lemma: No Number Ancestrally Precedes Itself
x[x Precedes*(x,x)]

(Proof) [Exercise for the Reader]

Now the Lemma on Predecessor+ asserts:
x & Precedes(y,x)
   #[z Precedes+(z,y)] = #[z Precedes+(z,x) & z x]
To prove this, assume that n 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 2), 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 and our assumption that Precedes(m,n), it follows from a fact about R+ (see §4, Weak Ancestral, Facts About R+, Fact 7), that Precedes+(a,m), which is what we had to show.