Proof That No Number Ancestrally Precedes Itself

We wish to prove:

Lemma: No Number Ancestrally Precedes Itself
$\forall x[Nx\rightarrow \neg\mathit{Precedes}^{*}(x,x)]$

Proof. Assume $Nb$, to show: $\neg \mathit{Precedes}^{*}(b,b)$. Now Fact 7 concerning $R^{+}$ is:

$[Fx\amp R^{+}(x,y) \amp \mathit{Her}(F,R)]\rightarrow Fy$

So we know the following instance of Fact 7 is true, where $x = 0$, $y$ is $b$, $F$ is $[\lambda z \, \neg\mathit{Precedes}^{*}(z,z)]$, and $R$ is Precedes:

By $\lambda$-Conversion on various terms in the above, this reduces to:

So to establish $\neg\mathit{Precedes}^{*}(b,b)$, we need to show each of the following conjuncts of the antecedent:

1. $\neg\mathit{Precedes}^{*}(0,0)$
2. $\mathit{Precedes}^{+}(0,b)$
3. $\mathit{Her}([\lambda z\, \neg\mathit{Precedes}^{*}(z,z)], \mathit{Precedes})$

To prove (a), note that in the Proof of Theorem 2 (i.e., $\neg\exists x(Nx\amp \mathit{Precedes}(x,0)))$, we established that $\neg\exists x(\mathit{Precedes}(x,0)$). But it is an instance of Fact 4 concerning $R^{*}$, that

$\exists x\mathit{Precedes}^{*}(x,0) \rightarrow \exists x\mathit{Precedes}(x,0)$.

It therefore follows that $\neg\exists x(\mathit{Precedes}^{*}(x,0))$. So $\neg\mathit{Precedes}^{*}(0,0)$.

We know (b) by our assumption that $Nb$ and the definition of $N$.

To establish (c), we have to show:

That is, by $\lambda$-Conversion, we have to show:

$\forall x,y(\mathit{Precedes}(x,y)\rightarrow (\neg\mathit{Precedes}^{*}(x,x)\rightarrow \neg\mathit{Precedes}^{*}(y,y)))$

And by contraposition, we have to show:

$\forall x,y(\mathit{Precedes}(x,y)\rightarrow (\mathit{Precedes}^{*}(y,y)\rightarrow \mathit{Precedes}^{*}(x,x)))$

So assume Precedes $(a,b)$ and $\mathit{Precedes}^{*}(b,b)$. If we show $\mathit{Precedes}^{*}(a,a)$, we are done. We know the following instance of Fact 8 concerning $R^{+}$, where $a$ is substituted for $z$, $b$ for $y$, $b$ for $x$, and Precedes for $R$:

Since we have assumed $\mathit{Precedes}^{*}(b,b)$ and $\mathit{Precedes}(a,b)$, and we have proven in the main text that Predecessor is 1-1, we can use the instance of Fact 8 to conclude $\mathit{Precedes}^{+}(b,a)$. But the following is an instance of Fact 2 concerning $R^{+}$, when $a$ is substituted for $x$, $b$ for $y$, $a$ for $z$, and $R$ is Precedes:

$\mathit{Precedes}(a,b)\amp \mathit{Precedes}^{+}(b,a)\rightarrow\mathit{Precedes}^{*}(a,a)$

But we know $\mathit{Precedes}(a,b)$ by assumption and we have just shown $\mathit{Precedes}^{+}(b,a)$. So $\mathit{Precedes}^{*}(a,a)$, and we are done.

Proof of the Lemma on Predecessor