Tarski's truth theorem — semantic or syntactic?

Question

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)?

Answer 1

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$.

Answer 2

Tarski's theorem, as given in Undecidable theories, page 46, allows arbitrary numbering and is completely syntactic. I think this abstract version given by Tarski himself is the most clear. Let me summarize it here with some inessential variations.

Let $T$ be a consistent first-order theory (any consistent first-order theory). If $\varphi\mapsto \ulcorner\varphi\urcorner$ is a naming of formulas (any assignment of closed terms to formulas), then either the diagonalization function (the function $\varphi\mapsto \varphi(\ulcorner\varphi\urcorner)$) is not representable (under that naming), or the set of theorems is not representable (under the given naming), or both are not representable.

In the case of ZF, assuming it to be consistent, we know that if we choose a recursive naming, we can represent the diagonalization function but not the set of theorems. Also, we can easily choose a (nonrecursive) naming which allows us to represent the set of theorems, but, then, the diagonalization will not be representable.

The proof is quite simple. If the diagonalization is representable, the fixed-point lemma can be proved quite simply. Assume that $V$ is a formula representing the set of theorems. Apply the fixed point lemma to get $\varphi$, a sentence satisfying $T\vdash\varphi\leftrightarrow \neg V(\ulcorner\varphi\urcorner)$.

If $T\vdash\varphi$, then, since $V$ represents the theorems, $T\vdash V(\ulcorner\varphi\urcorner)$, and $T$ is inconsistent. If $T\nvdash \varphi$, then, since $V$ represents the theorems, $T\vdash\neg V(\ulcorner\varphi\urcorner)$, and $T\vdash \varphi$ by the choice of $\varphi$. Therefore, $T\vdash \varphi$ and it is inconsistent by the previous argument.

EDIT

Motivated by the question in the comment, I will prove the fixed point lemma I have used above:

We are assuming that $T$ is a first-order theory and that the diagonalization is represented in $T$ under the arbitrary naming $\varphi\mapsto\ulcorner\varphi\urcorner$. It means that there is a formula $D(x,y)$ such that $T\vdash\forall y(D(\ulcorner\phi\urcorner, y)\leftrightarrow y=\ulcorner\phi(\ulcorner\phi\urcorner)\urcorner)$.

Now, let $W(y)$ be an arbitrary formula. Let $\phi(x)$ be the formula $\exists y(D(x,y)\wedge W(y))$ and let $\varphi$ be the sentence $\phi(\ulcorner\phi\urcorner)$, the diagonalization of $\phi$. This sentence is a fixed point for $W(y)$.

Indeed, $\varphi$ is $\exists y(D(\ulcorner\phi\urcorner,y)\wedge W(y))$, which, from the hypothesis on the representation of the diagonalization, is equivalent to $\exists y(y=\ulcorner\varphi\urcorner\wedge W(y))$. The last sentence is logically equivalent to $W(\ulcorner\varphi\urcorner)$, and we are done.

Therefore, Tarski's result applies to arbitrary first-order theories and to arbitrary namings. The moral is that no matter what first-order theory and naming of formulas you choose, the representation of at least one of two simple metatheoretical notions (diagonalization and theoremhood) within the object theory will always fail.

Answer 3

In arithmetic, you can use numbers ("Gödel numbers") to code formulas, and numerals in the very language to name them. In set theory, you can similarly use finite sets, e.g. von Neumann ordinals, to code formulas, and simple set theoretical expressions to name them. This is done directly e.g. in Melvin Fitting: Incompleteness in the Land of Sets (Studies in Logic). But because we know that arithmetic can be interpreted in set theory, and in that sense arithmetic can be done inside set theory, we can also just assume that all the Gödelian techniques can be transported to set theory.