In this article, Scott Aaronson talks about using Turing Machines for proving the Rosser Theorem.
What is the relationship between the numbering that Gödel used in his proof of incompleteness and Turing Machines?
[Math] the relationship between Turing Machines and Gödel’s Incompleteness Theorem
computability-theorycomputer sciencelo.logic
Related Solutions
The key idea Feferman is exploiting is that there can be two different enumerations of the axioms of a theory, so that the theory does not prove that the two enumerations give the same theory.
Here is an example. Let $A$ be a set of the axioms defined by some formula $\phi(n)$ (that is, $\phi(x)$ holds for exactly those $x$ that are in $A$). Define a new formula $\psi(n)$ like so:
$\psi(n) \equiv \phi(n) \land \text{Con}( \langle x \leq n : \phi(x)\rangle)$
Where Con(σ) is a formula which says that no contradiction is provable from the axioms listed in the sequence σ.
In the case where $A$ is the set of axioms for a suitable consistent theory $T$ that satisfies the second incompleteness theorem, the following hold:
(1) In the standard model, we have $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because $T$ really is consistent.
(2) T does not prove that $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because this equivalence implies that T is consistent.
(3) If we use $\psi$ to define a formula Conψ(T), then T will prove (under the assumption that the empty theory is consistent, if this is not provable in T) that the theory defined by ψ is consistent. However, T will not prove Conφ(T), which is the usual consistency sentence for T.
This kind of example is presented in a more precise way in Feferman's 1960 paper that you mentioned, along with precise hypotheses on the theory and sharper results.
My opinion is that we cannot regard a proof of Conψ(T) as a proof of the consistency of T, because although φ and ψ are extensionally identical, they do not intensionally represent the same theory. Feferman expresses a similar idea on his p. 69. Of course, this is a matter of philosophy or interpretation rather than a formal mathematical question.
Addendum
The difference between extensional and intensional equality is easiest to explain by example. Let A be the empty set and let B be the set of integers larger than 1 that do not have a unique prime factorization. Then we know B is also the empty set: so A and B are extensionally equal. But the definition of B is much different than the definition of A: so A and B are intensionally different.
This distinction is often important in contexts like computability and formal logic where the things that you work with are actually definitions (also called codes, indices, Gödel numbers, or notations) rather than the objects being defined. In many cases, extensional equality is problematic, because of computability or effectiveness problems. For example, in my answer above, we know that φ and ψ define the same set in the real world, but this fact requires proof, and that proof may be impossible in the object theory we are dealing with. On the other hand, intensional equality is easy to decide, provided you are working directly with definitions.
Yes, this line of thought is perfectly fine.
A set is decidable if and only if it has complexity $\Delta_1$ in the arithmetic hiearchy, which provides a way to measure the complexity of a definable set in terms of the complexity of its defining formulas. In particular, a set is decidable when both it and its complement can be characterized by an existential statement $\exists n\ \varphi(x,n)$, where $\varphi$ has only bounded quantifiers.
Thus, if you have a mathematical structure whose set of truths exceeds this level of complexity, then the theory cannot be decidable.
To show that the true theory of arithmetic has this level of complexity amounts to showing that the arithmetic hierarchy does not collapse. For every $n$, there are sets of complexity $\Sigma_n$ not arising earlier in the hierarchy. This follows inductively, starting with a universal $\Sigma_1$ set.
Tarski's theorem on the non-definability of truth goes somewhat beyond the statement you quote, since he shows that the collection of true statements of arithmetic is not only undecidable, but is not even definable---it does not appear at any finite level of the arithmetic hiearchy.
Finally, it may be worth remarking on the fact that there are two distinct uses of the word undecidable in this context. On the one hand, an assertion $\sigma$ is not decided by a theory $T$, if $T$ neither proves nor refutes $\sigma$. On the other hand, a set of numbers (or strings, or statements, etc.) is undecidable, if there is no Turing machine program that correctly computes membership in the set. The connection between the two notions is that if a (computably axiomatizable) theory $T$ is complete, then its set of theorems is decidable, since given any statement $\sigma$, we can search for a proof of $\sigma$ or a proof of $\neg\sigma$, and eventually we will find one or the other. Another way to say this is that every computably axiomatization of arithmetic must have an undecidable sentence, for otherwise arithmetic truth would be decidable, which is impossible by the halting problem (or because the arithmetic hierarchy does not collapse, or any number of other ways).
Best Answer
It's simple. If the halting problem is undecidable, then PA is not complete, since otherwise, you could solve the halting problem by searching for proofs in PA. And the same argument works for any sound computably axiomatizable theory $T$ able to express arithmetic. Given a Turing machine $M$ on input $i$, you formulate the assertion $\sigma$ asserting that $M$ halts on $i$, and then search for a proof in $T$ of $\sigma$ or a proof of $\neg\sigma$. If your theory were complete, then you'll find one or the other, and this would solve the halting problem. Since the halting problem is not solvable, there must be sentences of this form that are not settled by the theory.
This argument proves the first incompleteness theorem as an elementary consequence of the halting problem. The second incompleteness theorem takes a bit more work.
There is more discussion on Are the two meanings of undecidability related? and How undecidable is the spectral gap problem?