A finitist Gödel second incompleteness theorem

Question

Can we prove by finitist means (such as with $\text{Con}(\text{ZFC}) \to \text{Con}(\text{ZFC + CH})$; see Kunen's Set Theory, p.8) that $\text{ZFC} \vdash \text{Con}(\text{ZFC}) \Rightarrow \text{ZFC} \vdash \perp$? That is, can we show that if we had any formal ZFC-proof of the sentence $\text{Con}(\text{ZFC})$, that we could transform it by purely finitist ("mechanical") means into a proof of $\text{ZFC} \vdash \perp$? Or do we need a stronger metatheory to get Gödel's second incompleteness theorem? Does this question make sense?

Answer 1

Looking back, I think my original answer wasn't very satisfactory. I believe the following is better.

Yes, GSIT is already as "finitary" as one could reasonably hope.

Throughout, $T$ is the "appropriate" theory we're analyzing and we work in an "appropriate" metatheory $S$. Note that stronger $T$ and $S$ only make things easier. I'll say a bit about what we need from $T$ and $S$ more precisely below, but for now let me just note that $I\Sigma_1$ - a tiny fragment of first-order Peano arithmetic $\mathsf{PA}$, and almost unspeakably weaker than $\mathsf{ZFC}$ - is overkill for both $T$ and $S$.

---

First, we have some crucial set-up. Here $\mathfrak{G}_T$ is the Godel-Rosser sentence for $T$ ("For every proof of me there is a shorter disproof of me"). There are two specific $T$-proofs which we construct ahead of time (in particular, none of this depends on having a putative $T$-proof of $Con(T)$):

• There is a $T$-proof $\pi$ of "If $\mathfrak{G}_T$ is $T$-undecidable then $\mathfrak{G}_T$ is true."

• There is an explicit procedure $\Theta$ for producing from a putative $T$-proof of $\mathfrak{G}_T$ a $T$-proof of $\perp$.

Now suppose we had a $T$-proof $\theta$ of $Con(T)$. Consider the following construction $\hat{\Theta}$ (which uses $\Theta$ as a "subroutine"):

• Combining $\theta$ with $\pi$ we get a proof $\eta_1$ that $\mathfrak{G}_T$ is $T$-undecidable.

• This in turn yields a $T$-proof $\eta_2$ of $\mathfrak{G}_T$ ($T$ argues "if $\mathfrak{G}_T$ is $T$-undecidable then vacuously for every $T$-proof of $\mathfrak{G}_T$ there is a shorter $T$-disproof of $\mathfrak{G}_T$ - which is to say $\mathfrak{G}_T$ is true").

• But now consider $\Theta(\eta_2)$.

---

Now let's dig into the above in a bit more detail.

First, the trivial stuff. Both $\Theta$ and $\hat{\Theta}$ are just explicit algorithms we write down; writing something down isn't problematic for us, we just explicitly do it.

Next, the nontrivial stuff. Obviously we've carried along the assumptions that logic can be satisfactorily "arithmetized" (or "set-ized," or whatever) in $T$ and $S$. Briefly, we need both $S$ and $T$ to satisfy an extremely weak completeness property - essentially, the ability to verify specific computations.

Beyond this, there are really two nontrivial things that happened, and I'll treat them in order:

We asserted the existence of $\pi$.

This relied on a possibly-surprising assumption about $T$ - a very weak one to be sure, but a nontrivial one nonetheless: that $T$ be strong enough to prove that some basic arithmetic operations (like multiplication) are always defined.

The idea behind $\pi$ is this:

"Go by contrapositive. If $\mathfrak{G}_T$ were false, we could prove the falsity of $\mathfrak{G}_T$ inside $T$ by finding and verifying a $T$-proof of $\mathfrak{G}_T$ and then checking each putative shorter $T$-proof of $\neg\mathfrak{G}_T$; combining all these calculations would give a single $T$-proof of $\neg\mathfrak{G}_T$."

Note the "combining all these calculations" bit. There's a significant "length-blowup" here: the length of the $T$-proof of $\neg\mathfrak{G}_T$ we get is naively exponential in the length of the putative $T$-prof of $\mathfrak{G}_T$ we get directly from the assumption that $\mathfrak{G}_T$ is false. This can be brought down significantly, but there's still something nontrivial here. In order for that argument to go through in $T$, we need $T$ to be able to prove the totality of the appropriate arithmetic operations.

And this is unavoidable: we can find very weak theories of arithmetic which can prove their own consistency¹, escaping contradiction by being unable to prove that multiplication is always defined (or worse).

We claimed properties of algorithms

Writing down the specific $\Theta$ and $\hat{\Theta}$ isn't fundamentally hard (and hey, suffering builds character). But when we claim that the things we've written down have certain properties, we are implicitly working in some metatheory and may be invoking nontrivial assumptions.

We're going to see exactly the same issue here that we did above. $\hat{\Theta}$ is boring, but $\Theta$ is basically just "$\pi$ in the metatheory." So we also need $S$ to prove the totality of basic arithmetic operations.

And again this is important: working in a weak metatheory can have some very odd results.

¹Dan Willard: Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles, Journal of Symbolic Logic 66 (2):536-596 (2001). DOI: 10.2307/2695030, JSTOR, author's website