Relating GIT2 and Tarski’s undefinability

logicproof-explanationset-theorysolution-verification

I am trying to read on set theory / logic. Informally, I read that Godel's second incompleteness theorem (GIT2) states that given a (sufficiently strong) logic, if the logic proves its own consistency, then the logic is inconsistent.

In most proofs of GIT2 that I read (i.e. Kunen's book), GIT2 is proven using a diagonalization argmuent by constructing a formula $\gamma$ which says "I am not provable".

But suppose that we already have Tarski's undefinability theorem at hand, am curious if we can use Tarski's theorem to prove GIT2 this way (informally in a finitistic metatheory). Suppose we are working in $ZFC$.

  1. Suppose that $ZFC \vdash Con(ZFC)$.
  2. Using (1) and the result that If $Con(ZFC)$, then $M\models ZFC$ for some $M$, we get $ZFC \vdash (M \models ZFC)$ for some set-like $M$, as proper classes "don't exist" in $ZFC$.
  3. But from Tarsk's undefinability theorem, we have that $M \models ZFC$ as undefined for any class or set-like $M$, so that we can say $ZFC \vdash \neg (M \models ZFC)$.
  4. Given that $ZFC \vdash (M \models ZFC)$ and $ZFC \vdash \neg(M \models ZFC)$, it follows that $ZFC$ is inconsistent, and GIT2 is proven when the logic is $ZFC$

Any comments / help are welcome and much appreciated.

EDIT: As per comments there's a bug in 3 above, but am retaining my post as it is, as a souvenir. But I saw a post which says that TUT does not imply GIT2. Is that the case ?

Best Answer

It's very difficult to prove that one true theorem cannot be used to prove another true theorem. However, there are a couple observations we can make here which indicate that there is no "easy" road from Tarski's undefinability theorem to the second incompleteness theorem (by contrast, there is such a road from TUT to GIT1). On the other hand, if we use a stronger form of TUT and allow ourselves a more involved argument, then we can do this.

Probably no "easy" route

There are a couple of reasons we (in my opinion) should not expect an easy proof of GIT2 from TUT.

Most immediately, there are some "reasonably-expressive" theories for which the second incompleteness theorem actually fails. When the theory in question is presented as a computable set of axioms, these are called "self-verifying theories" and were first studied by Willard; see e.g. the wiki page. However, TUT (and GIT1 for that matter) have no such edge-cases.

Now the theories above are rather weird - e.g. multiplication won't be total in them - but there is yet another way that an appropriate theory can prove its own consistency: be described in a more complicated way. This is probably folklore:

Fix some "reasonable" enumeration of $\mathsf{ZFC}$ as $\{\psi_i:i\in\omega\}$. Then there is a formula $\varphi(x)$ which says "$x$ is (the code for) some $\psi_i$ such that $\{\psi_j: j\le i\}$ is consistent."

Assuming $\mathsf{ZFC}$ is consistent this $\varphi$ classically picks out the $\mathsf{ZFC}$ axioms themselves, and by the reflection principle we will have $\varphi^M$ contains (true, external) $\mathsf{ZFC}$ for any model $M\models\mathsf{ZFC}$. And, trivially, the theory picked out by $\varphi$ is consistent! The issue of course is that $\varphi$ is not a "nice" definition of a theory. But Tarski's undefinability theorem is extremely coarse, and applies to all definable theories in an appropriate sense, so we shouldn't expect it to (easily) imply such a fine-grained result.

Finally, and very similarly to the second point above, consider the following two sorts of "dangerous formulas:"

$\theta(x)$ is 1-dangerous if whenever $M\models\mathsf{ZFC}$ we have that (the standard part of) $\theta^M$ is a consistent complete theory containing $\mathsf{ZFC}$.

$\theta(x)$ is 2-dangerous if whenever $M\models\mathsf{ZFC}$ we have that $M\models$ "$\theta^M$ is a consistent complete theory containing $\mathsf{ZFC}$."

Again because of the "coarseness" of TUT, it's hard to see how TUT pushes back against 2-dangerousness more than 1-dangerousness. But this is exactly what GIT2 does distinguish between: GIT2 says that there are no 2-dangerous formulas, but there are 1-dangerous formulas by exactly the same trick as above.

That said ...

Embarrassingly, shortly after I posted the first version of this answer I remembered the paper Existentially closed structures and Godel's second incompleteness theorem. It's been on my to-read pile for a while, and this question reminded me of it. It turns out that this paper may come pretty close to doing what you want!

Briefly, A/B look at the notion of a 1-closed model of an appropriate theory. For simplicity, we want everything to be in the language of arithmetic and axiomatized by $\Pi^0_2$ sentences (in the arithmetical, not Levy, hierarchy); for example, rather than look at $\mathsf{ZFC}$ itself we'd look at the set of $\Pi^0_2$ theorems of $\mathsf{ZFC}$. 1-closed models of such theories are guaranteed to exist, by an easy construction.

So let $T$ be such a theory. By a really cute compactness argument, A/B show that if $\mathcal{M}$ were a 1-closed model of $T$ satisfying $Con(T)$, then the $\Sigma^0_1$-theory-with-parameters of $\mathcal{M}$ would be $\Pi^0_1$-definable over $\mathcal{M}$.

It's here that TUT - in an extended form - kicks in. Specifically, the proof of TUT shows more than is usually claimed: it shows that - even in nonstandard models - we can never have a truth predicate for a syntactic class $\Gamma$ expressible by a formula whose negation is also in $\Gamma$. This gives a contradiction with the above, so any 1-closed model of $T$ must satisfy $\neg Con(T)$ ... and so $T\not\vdash Con(T)$. Woohoo! See here for a bit more detail.

Related Question