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