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?