In the Wikipedia page for Turing's Halting problem, they mention that you can prove Gödel's First Incompleteness theorem from it. This is the relevant quote:

Assume that we have a sound (and hence consistent) and complete axiomatization of all true first-order logic statements about natural numbers. Then we can build an algorithm that enumerates all these statements. This means that there is an algorithm N(n) that, given a natural number n, computes a true first-order logic statement about natural numbers, and that for all true statements, there is at least one n such that N(n) yields that statement. Now suppose we want to decide if the algorithm with representation a halts on input i. We know that this statement can be expressed with a first-order logic statement, say H(a, i). Since the axiomatization is complete it follows that either there is an n such that N(n) = H(a, i) or there is an n' such that N(n') = ¬ H(a, i). So if we iterate over all n until we either find H(a, i) or its negation, we will always halt, and furthermore, the answer it gives us will be true (by soundness). This means that this gives us an algorithm to decide the halting problem. Since we know that there cannot be such an algorithm, it follows that the assumption that there is a consistent and complete axiomatization of all true first-order logic statements about natural numbers must be false.

After reading this proof, I wondered if a very similar proof by contradiction could also prove Tarski's Undefinability theorem?

I was thinking of something along the following lines:

Imagine that a truth predicate isTrue($\ulcorner s \urcorner$) for any arbitrary logic sentence s were computable. In that case, this predicate would also be able to compute the truth status for any arbitrary H(a,i). Therefore, we would be able to compute isTrue($\ulcorner H(a,i) \urcorner$) for any possible H(a,i). Consequently, such isTrue($\ulcorner s \urcorner$) predicate would solve Turing's Halting problem, while we already know that it is fundamentally unsolvable. Therefore, such truth predicate is not computable.

Is there a flaw or a problem with this proof strategy?

The fact that the Wikipedia page mentions this proof strategy for Gödel's First Incompleteness but not for Tarski's Undefinability got me wondering. Maybe it does not work for Tarski after all? What's the catch?

  • $\begingroup$ I think you're misrepresenting the statement of Tarski's theorem: it's not about computability, but about representability in a (sufficiently nice) logic. $\endgroup$
    – cody
    Commented Dec 24, 2019 at 13:41
  • $\begingroup$ According to WP: "Tarski's undefinability theorem: There is no L-formula True(n) that defines T*. That is, there is no L-formula True(n) such that for every L-formula A, True(g(A)) ↔ A holds." If it is "undefinable", then it is also "uncomputable"? Isn't definability a prerequisite requirement for computability? $\endgroup$
    – erik
    Commented Dec 25, 2019 at 5:47
  • 2
    $\begingroup$ Correct, but you are using the converse: you are trying to prove that something is undefinable because it is uncomputable. This is not true in general. $\endgroup$
    – cody
    Commented Dec 25, 2019 at 16:25

1 Answer 1


As cody observed, the problem with that strategy is that definable relations need not be computable. For example, the Halting Problem is definable in $(\mathbb{N}; +,\times)$ (see Kleene's $T$-predicate).

That said, a relativized form of the incomputability of the Halting Problem, applied to iterates of the Turing jump, does do the job:

  • First, we show that for each $n$ and each $\Sigma_n$ formula $\varphi$ the set $\{x: \varphi(x)\}$ is computable from ${\bf 0^{(n)}}$, uniformly in $n$ and $\varphi$.

  • Next, we show that for each $n$ the set ${\bf 0^{(n)}}$ is itself definable by some $\Sigma_n$ formula $\psi_n$. This is an application of Kleene's $T$-predicate.

  • Now we're good to go. Suppose we had a $\Sigma_n$ formula $\varphi$ defining the set of (Godel numbers of) true sentences in the language of arithmetic. Then ${\bf 0^{(n)}}$ could compute ${\bf 0^{(n+1)}}$ as follows: given $k$, we ask ${\bf 0^{(n)}}$ whether $\varphi(\underline{\ulcorner\psi_{n+1}(\underline{k})\urcorner})$ holds. (Here "$\underline{i}$" denotes the numeral corresponding to the number $i$, and "$\ulcorner\theta\urcorner$" is the Godel number of $\theta$.)

  • But that gives ${\bf 0^{(n+1)}}=({\bf 0^{(n)}})'\le_T{\bf 0^{(n)}}$, a contradiction by the relativized unsolvability of the Halting Problem.

  • $\begingroup$ Super! I will need some time to read up and get used to the formalisms that you have used, but it certainly looks exactly what I was looking for! $\endgroup$
    – erik
    Commented Dec 26, 2019 at 5:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.