# Is there some kind of equivalence between Turing Machines and a formal system of axioms?

I know that the set of provable propositions in a sufficiently complex formal system is recursively enumerable but non-recursive, and so no Turing Machine could decide all the propositions that could be decided from the axioms and rules of procedures of the system.

But in his book "Shadows of the Mind", Roger Penrose uses a version of Gödel's theorem based on Turing Machines (or computations generally). He says that for a given Turing Machine H which is supposed to take as input another Turing Machine M acting on n, H sometimes determines whether M halts or not. From then, he shows that there always is a certain computation k (acting on input k by diagonal slash) which H cannot handle: H can't determine whether the computation k halts or not, when in fact it does not halt.

Is this proof different than the standard Gödel theorem? Does this show a kind of equivalence between algorithms and formal systems?

• Gödel incomplete theorems can be stated purely in term of halting of certain Turing machines, yes. May 14 at 18:36
• @reuns then what's the difference between the Turing Machine M described in my post and a (sufficiently complex) formal system? May 15 at 4:23