Supplement to Frege's Logic, Theorem, and Foundations for Arithmetic
Proof of the Lemma on Predecessor+
We wish to prove the Lemma on Predecessor+, which asserts:Lemma on Predecessor+:Now this Lemma can be proved with the help of the following Lemma:
Nx & Precedes(y,x) →
#[λz Precedes+(z,y)] = #[λz Precedes+(z,x) & z ≠ x]
Lemma: No Number Ancestrally Precedes Itself
∀x[Nx → ¬Precedes*(x,x)](Proof) [Exercise for the Reader]
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 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, 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 7), that Precedes+(a,m), which is what we had to show.