# Tarski's truth theorem — semantic or syntactic?

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

• Let the enumeration be recursive. Implement it inside the theory. – Monroe Eskew Apr 27 '20 at 17:34
• @MonroeEskew In fact we just need the enumeration to be definable. – Noah Schweber Apr 27 '20 at 18:21
• @MonroeEskew Your comment doesn't seem to address the two questions I asked. – Pace Nielsen Apr 27 '20 at 19:06
• This is a theorem about models. It is about undefinability of "truth" which means satisfaction. We are showing that for any given model $M$ of ZFC (although this holds in more generality) is no formula $\phi(v)$ in the language of set theory such that $M \models \phi(x)$ iff $x$ is a standard natural number coding a sentence that is true in $M$. If you like, we can restrict our attention to one preferred model, say "V". I don't know how to phrase this result as a purely syntactic / provability result-- it's about satisfaction. – Monroe Eskew Apr 27 '20 at 19:34
• @MonroeEskew "If you like, we can restrict our attention to one preferred model, say "V"" FWIW I think (per my answer) that this is what Jech's doing - working implicitly in NBG and proving "$Th(V)$ is not definable in $V$." – Noah Schweber Apr 27 '20 at 19:35

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

• @PaceNielsen What is a truth predicate for ZFC? Truth predicates only make sense for structures. – Noah Schweber Apr 27 '20 at 19:00
• @PaceNielsen You can also take from this argument the syntactic result that there is no formula $\phi(v)$ such that for every sentence $\sigma$, ZFC proves $\phi(\#\sigma) \leftrightarrow \sigma$. Because given $\phi(v)$, you can construct a particular $\sigma$ that is provably equivalent to $\neg\phi(\#\sigma)$. This is just Goedel's fixed point lemma. – Monroe Eskew Apr 27 '20 at 19:43
• @PaceNielsen Yes, that's just Godel's diagonal lemma (and it's provable in $I\Sigma_1$ for example). – Noah Schweber Apr 27 '20 at 20:00
• @PaceNielsen- See for example the end of the first chapter of Kunen’s book. – Monroe Eskew Apr 27 '20 at 20:04
• @PaceNielsen Well, for an arbitrary numbering there's not much that can be said. For example, map all the true sentences onto the evens and the false sentences onto the odds. So some constraint is needed to get anything useful. The key properties we need for these sorts of results are representability, or invariant definability, properties: for example, we want there to be a formula $\psi$ such that for every standard $i,j,k$ we have $T\vdash\psi(i,j,k)$ iff $i=\#(\#^{-1}(j)\wedge\#^{-1}(k))$ and $T\vdash\neg\psi(i,j,k)$ otherwise. (cont'd) – Noah Schweber Apr 27 '20 at 20:13

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.

• I like this trichotomy. Doesn't the fixed point lemma require more than just $T$ being a first-order theory? Also, this result is talking about validity rather than truth; am I right in saying that truth is representable iff validity is representable? – Pace Nielsen Apr 28 '20 at 15:47
• I have proved the fixed point lemma. Validity is more general than truth. Truth is validity when the theory is complete, that is, the theory of a model. – Rodrigo Freire Apr 28 '20 at 18:33
• The Diagonalization Lemma (= the fixed point lemma) requires something like the Robinson Arithmetic Q. The diagonalization function must be (strongly) representable. In the language of set theory, the very weak "baby set theory" i.e. "the adjunctive set theory" will do. – Panu Raatikainen May 2 '20 at 18:05

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.