# 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. Commented May 14, 2022 at 18:36
• @reuns then what's the difference between the Turing Machine M described in my post and a (sufficiently complex) formal system? Commented May 15, 2022 at 4:23

## 1 Answer

You need to be a little careful here: some formal systems are weak enough that we can easily decide the truth of any proposition. For instance, a formal system describing some particular finite structure.

If a Turing machine halts, there's a proof that it halts which is just the sequence of steps that it took.

On the other hand, you can build a Turing machine that hunts for a proof of any proposition (by searching all strings in an infinite loop to check if they're valid proofs, and also proofs of that particular proposition) and halts if it finds it.

• But for a sufficiently complex formal system, capable of coding basic arithmetic, the set of theorems in this system is not computable (enumerable but non-recursive) right? So I don't see how a Turing Machine could be equivalent to a (sufficiently complex) formal system. (since that machine could not deal with all the decidable propositions of the system) But then Penrose shows how Gödel's theorem can be stated purely in computational terms based on Turing Machines. So I guess I wanted to know at this point if there is an equivalence between the two? Commented May 15, 2022 at 0:43