Edward Nelson has started writing out the details of a proof of the inconsistency of a version of arithmetic. I'm an undergraduate trying to read through this slowly and carefully.
I've run into a problem, however, with one of his arguments on page 11. It's a proof that "there is a specific number that is not a finite number", which he attributes to Simon Kochen. I did a little digging, and found he had written up a better version of the argument on page 74 of his 1986 book "Predicative Arithmetic" (available on his website). For your convenience, here are just the relevant pages:
$\textbf{Chapter 18}$
$\textbf{An impassable barrier}$
$\quad$ Let us pause to examine from an impredicative point of view what we are doing. Take a strong theory $\rm T$ containing $\rm 0$ and $\rm S$, say an extension by definitions of Peano Arithmetic $I$ or even of $\sf ZFC$ (Zermelo-Fraenkel set theory with the axiom of choice). Let $\rm\hat T$ be the theory obtained by adjoining a unary predicate symbol $\phi$ and the axiom $\text{Fin. }\ \phi(0)\ \& \ (\phi(x)\to\phi({\rm S}x))\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$ This adjunction does not increase the power of the theory in any way; we can for example interpret $\phi(x)$ by $x=x$. If $\rm T$ is an axiomatization of arithmetic, say an extension by definitions of $I$, then by a specific number we mean a variable-free term $\rm b$ of $\rm T$; if $\rm T$ is an extension by definitions of $\sf ZFC$ containing the constant $\omega$ denoting the set of all natural numbers, then by a specific number we mean a variable-free term $\rm b$ of $\rm T$ such that $\vdash_{\rm T}{\rm b}\in\omega$. We say that a specific number $\rm b$ is a finite number in case $\vdash_{\rm\hat T}\phi(\rm b)$.
$\quad$ Now consider a specific number $\rm b$, such as $10000$ or $10\uparrow10\uparrow10$, and try to prove $\phi(\rm b)$. The initial reaction of some mathematicians to such a problem is a failure to see the difficulty: they suggest proving $\phi(\rm b)$ by induction. But even if the induction principle is an axiom scheme of $\rm T$, we do not have induction available for $\phi(x)$, because the axioms of $\rm T$ say nothing about formulas containing $\phi$. A second reaction is that the problem is trivial because there is an obvious proof in $\rm b$ steps. This observation manages to be both meaningless and incorrect; meaningless because of the ubiquitous pun confusing the formal and genetic concepts of number, and incorrect because there are specific numbers $\rm b$ for which one can show that there is no proof in $\rm\hat T$ of $\phi(b)$. That is, there is a specific number that is not a finite number.
$\quad$ To see this, we will let $\rm T$ be an extension by definitions of $I$. We assume that $I$ is consistent; otherwise there is indeed a proof in $\rm\hat T$ of $\phi(b)$. Consider Gödel's construction of a closed formula $\forall n\mathrm{C}[n]$ that is unprovable even though $\mathrm{C}[0],\mathrm{C}[1],\mathrm{C}[2],...$ are all provable. Let $\rm D$ be the unary formula $\mathrm{C}[n]\to\forall n C[n]$. Then $\exists n{\rm D}[n]$ is provable, since it is equivalent to the tautology $\forall n\mathrm{C}[n]\to\forall n\mathrm{C}[n]$, but ${\rm D}[0],{\rm D}[1],{\rm D}[2],...$ are all unprovable, since from a proof of one of them and the proof of the corresponding theorem among $\mathrm{C}[0],\mathrm{C}[1],\mathrm{C}[2],...$ we would immediately obtain a proof of $\forall n {\rm C}[n]$. Now consider the constant $N$ with the defining axiom $1.\ \ \ \ N=n\ \leftrightarrow\ \mathrm{D}[n]\ \&\ \forall m(m
The existence condition holds by the least number principle and the uniqueness condition is obvious. We assume that $(1)$ is an axiom of $\rm T$. We claim that $\phi(N)$ is not a theorem of $\rm\hat T$. To see this, take a model of the consistent theory obtained by adjoining $\neg{\rm D}[0],\neg{\rm D}[1],\neg{\rm D}[2],...$ to $\rm T$ and represent $\phi$ by membership in the smallest subset of the universe of the model containing the individual representing $0$ and closed under the function representing $\rm S$. Then $\phi(N)$ is not valid in the model, so $\phi(N)$ is not a theorem of $\rm\hat T$. I am grateful to Simon Kochen for this example.
My problem is specifically these two sentences:
Let $D$ be the unary formula $C[n] \rightarrow \forall n C[n]$. Then $\exists n D[n]$ is provable, since it is equivalent to the tautology $\forall n C[n] \rightarrow \forall n C[n]$.
How in God's name is $\exists n D[n]$ equivalent to $\forall n C[n] \rightarrow \forall n C[n]$?