Proof of the Lemma on Predecessor$^{+}$

We wish to prove the Lemma on Predecessor$^{+}$, which asserts:

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.

Return to Proof that Q is Hereditary on the Natural Numbers