Tarski’s Truth Theorem – Semantic or Syntactic?

lo.logicmodel-theoryset-theory

I was reading the sketch of the proof of Tarski's theorem in Jech's "Set Theory", which appears as Theorem 12.7, thinking that it would be an interesting result to really understand. As stated in the book, it is essentially a syntactic result (after fixing a Gödel numbering). However, after reading other proofs of Tarski's result, and really delving into the sketched proof, I believe that there is a serious error in Jech's proof, and now I'm not sure the result holds at the syntactic level.

Here is the problem as I see it. In the second sentence of the proof the formulas are enumerated as $$\varphi_0,\varphi_1,\varphi_2,\ldots.$$ Now, this is an enumeration outside ZFC, so the subscripts are metamathematical numbers. But in the next formula, which reads, $$x\in \omega \land \neg T(\#(\varphi_x(x))),$$ the subscript $x$ on $\varphi$ is being treated as a formal natural number—an element of $\omega$.

If we have a model of set theory, where $\omega$ matches the metamathematical natural numbers, maybe we could make this formula work. My question is whether or not we can somehow avoid making such a strong assumption. If not, what's the easiest way to assert such a matching (say, without forcing an interpretation of all of ZFC, just of the natural number part)?

Best Answer

If I recall correctly, Jech is using as his metatheory the class theory $\mathsf{NBG}$. In this context, "true" is a proxy for "true in the (class-sized) structure $V$."

Specifically, the (more) formal version of the natural-language Theorem $12.7$ is the following:

$Th(V)$ is not definable in $V$.

The definition of $Th(V)$ is taking place on the class level: it's a set of natural numbers defined by quantifying over classes. The same is true for the property "definable in $V$." So even though it looks like Jech is using a weirdly un-referring notion of "truth," it is in fact just the usual notion of truth with respect to a specific structure - that structure being $V$, and that whole facet of the argument being (annoyingly, perhaps) kept implicit. Note that this makes the whole "correctness-about-$\omega$" issue moot: Theorem $12.7$ is about a structure which by definition has the right $\omega$.

An in-my-opinion more satisfying version of the result, which makes correctness-about-$\omega$ nontrivial, is the following:

$T$ proves that for all $\mathcal{M}\models\mathsf{ZFC}$, $Th(\mathcal{M})$ is not the standard part of a definable subset of $\mathcal{M}$.

Here $T$ is a very weak theory indeed: $\mathsf{ACA_0^+}$ suffices (really the only need for strength being the requirement that the theory of a structure is actually a thing that makes sense in the first place - see e.g. here). Note that this version of the result does not apply only to models which are correct about $\omega$.

EDIT: And as Monroe Eskew pointed out below, if we drop models entirely we can go even lower. We can prove over a very weak base theory (e.g. $I\Sigma_1$ is already overkill) the following:

If $\mathsf{ZFC}$ is consistent, then there is no formula $\varphi$ such that for all sentences $\psi$ $\mathsf{ZFC}$ proves $\varphi(\#\psi)\leftrightarrow\psi$.

Related Question