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:
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]$?