Is it possible to prove Tarski's Undefinability theorem from Turing's Halting Problem? 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?
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.