Supplement to Frege’s Theorem and Foundations for Arithmetic
Proof of the Lemma on Predecessor\(^{+}\)
We wish to prove the Lemma on Predecessor\(^{+}\), which asserts:
\[\begin{align*} &Nx\amp \mathit{Precedes}(y,x) \rightarrow \\ &\quad \#[\lambda z \,\mathit{Precedes}^{+}(z,y)] = \#[\lambda z \,\mathit{Precedes}^{+}(z,x)\amp z \neq x] \end{align*}\]
Now this Lemma can be proved with the help of the following Lemma:
Lemma: No Number Ancestrally Precedes Itself
\(\forall x[Nx\rightarrow\neg\mathit{Precedes}^{*}(x,x)]\)
(Proof of the Lemma that No Number Ancestrally Precedes Itself)
Now to prove the Lemma on Predecessor\(^{+}\!\), assume that \(Nn\) and \(\mathit{Precedes}(m,n)\). We want to show:
\(\#[\lambda z \, \mathit{Precedes}^{+}(z,m)] = \#[\lambda z \, \mathit{Precedes}^{+}(z,n)\amp z \neq n]\)
By Hume's Principle, it suffices to show:
\([\lambda z \, \mathit{Precedes}^{+}(z,m)]\approx [\lambda z \, \mathit{Precedes}^{+}(z,n)\amp z \neq n]\)
Now it is a fact about equinumerosity (Fact 1, Facts About Equinumerosity, §3) that if two concepts are materially equivalent, then they are equinumerous. It therefore suffices to show that
\(\forall x([\lambda z \, \mathit{Precedes}^{+}(z,m)]x\equivwide [\lambda z \, \mathit{Precedes}^{+}(z,n)\amp z \neq n]x)\)
And by \(\lambda\)-Conversion, it suffices to show:
\(\forall x[\mathit{Precedes}^{+}(x,m) \equivwide \mathit{Precedes}^{+}(x,n)\amp x \neq n]\)
So let us pick an arbitrary object, say \(a\), and show:
\(\mathit{Precedes}^{+}(a,m) \equivwide (\mathit{Precedes}^{+}(a,n)\amp a \neq n)\)
\((\rightarrow)\) Assume \(\mathit{Precedes}^{+}(a,m)\). Then from our assumption that \(\mathit{Precedes}(m,n)\) and a Fact about \(R^{+}\) (Fact 3, Facts About \(R^{+}\!\), §4, Weak Ancestral), it follows that \(\mathit{Precedes}^{*}(a,n)\). A fortiori, then, \(\mathit{Precedes}^{+}(a,n)\). Now by the Lemma mentioned at the outset of this proof, namely, No Natural Number Ancestrally Precedes Itself, we know that \(\neg \mathit{Precedes}^{*}(n,n)\). Since \(a\) ancestrally precedes \(n\) and \(n\) does not, it follows that \(a\neq n\). We have therefore proved what we were after, namely:
\(\mathit{Precedes}^{+}(a,n)\amp a\neq n\)
\((\leftarrow)\) Assume \(\mathit{Precedes}^{+}(a,n)\) and \(a\neq n\). By definition, the first conjunct tells us that either \(\mathit{Precedes}^{*}(a,n)\) or \(a = n\). Since we know by assumption that the latter disjunct is not true, we know \(\mathit{Precedes}^{*}(a,n)\). But from this fact, the fact that Predecessor is 1-1, and our assumption that \(\mathit{Precedes}(m,n)\), it follows from a fact about \(R^{+}\) (Fact 8, Facts About \(R^{+}\), §4, Weak Ancestral), that \(\mathit{Precedes}^{+}(a,m)\), which is what we had to show.