# Does godel's incompleteness theorem still hold if we have a TM that can do an infinity amount of computations?

I have heard whisperings that if we have a turing machine that is allowed to compute infinitely many steps in finite time, then we can solve the halting problem.

This made me wonder, if we have such a TM, do Godel's incompleteness theorems then not hold anymore?

My intuition is: If the TM can make an infinite amount of computations, it can simply check the truth-value of any formula, by checking all natural numbers. e.g. if we have a formula $\forall x \phi (x)$, the infinite-TM can simply check for every natural number $n$ whether $\phi(n)$ holds.

• What do you mean by making "Godel's theorem not hold anymore"? – Ariel Mar 17 '18 at 9:06
• @Ariel My interpretation of this question is: If we relax our notion of decidability to ITTM-decidability, are there still absolutely undecidable statements? – Arno Mar 17 '18 at 10:05

There is some ambiguity in how to define these new machines, essentially based on the question whether we can nest the "bursts of doing infinitely many steps in some finite time" or not. In the weakest interpretation, we essentially just get an oracle Turing machine with access to the Halting problem. In the strongest, we get the Infinite Time Turing Machines (ITTM).

Both machines can easily decide the ordinary Halting problem. However, the proof of non-computability of the Halting problem uses very little prerequisites. In particular, it shows that none of our machines can solve their own Halting problems.

So while an ITTM can decide truth of all basic arithmetic formulas (by just searching through the natural numbers whenever required), they cannot decide all $\Sigma^1_2$-formulas. And to properly define and work with ITTMs, we need $\Sigma^1_2$-formulas. So we have just pushed undecidability further out, but we have not removed it.

A $\Sigma^1_2$-formula is one of the form $$\exists A \subseteq \mathbb{N} \ \ \forall B \subseteq \mathbb{N} \ \ \phi(A,B)$$ where $\phi$ is a formula which contains only quantification over numbers, but not over sets of numbers.

• Ah thanks. So just to confirm. All first order formulas could be provable or disprovable with such a TM? And basically this can be phrased differently I think as follows (please tell me whether I'm right). The standard proof calculi (to which godel's theorem applies) provide proofs that consists of a finite amount of applications of the logical axioms. However, when we allow for countably infinite proofs, that is proofs that are constructed using an infinite amount of applications of the axioms, then godel's theorem no longer applies to that new proof calculus. Is that correct? – user56834 Mar 17 '18 at 10:12
• An ITTM can decide the truth of a any first-order formula, yes. We could then built a proof calculus with infinite proofs in a way that provability there corresponds to ITTM computations. In such a calculus, every true first-order formula is provable. However, the calculus will be so powerful that limiting it to first order formula is "unfair" (because you can't reason about its workings in first-order alone). Allowing more complicated formula then brings back incompleteness. – Arno Mar 17 '18 at 10:28
• Could you explain what you mean by "unfair"? I can see why we wouldn't be able to talk about that system in first order logic, but i don't see how that matters, since the ITTM only needs to reason about first order formulas in arithmetic, but not about itself. – user56834 Mar 17 '18 at 11:26
• Also, do you happen to have a reference for this? – user56834 Mar 30 '18 at 8:33
• Also, do you know which part of the proof of Godel's incompleteness theorem breaks down once we use ITTM's? – user56834 Apr 2 '18 at 8:52