The relation of Gödel's Incompleteness Theorems to the Church-Turing Thesis

This may be a naive question, but here goes. (Edit -- it is not getting upvotes, but nobody has offered a response either; perhaps the question is more difficult, obscure, or unclear than I thought?)

Gödel's First Incompleteness Theorem can be proven as a corollary of the undecidability of the halting problem (e.g. Sipser Ch. 6; blog post by Scott Aaronson).

From what I understand (confirmed by the comments), this proof does not depend on the Church-Turing thesis. We derive a contradiction by showing that, in a complete and consistent formal system, a Turing Machine could solve the halting problem. (If on the other hand we had just shown that some effective procedure could decide the halting problem, we would need to also assume the Church-Turing thesis to get a contradiction.)

So, we might say that this result provides a bit of intuitive support for the Church-Turing thesis, because it shows that a limitation of Turing Machines implies a universal limitation. (Aaronson's blog post certainly supports this view.)

My question is whether we can gain something more concrete by going in reverse: What formal implications do Gödel's theorems have for the Church-Turing thesis? For instance, it seems intuitively possible that the First Incompleteness theorem implies that no effective procedure can determine if an arbitrary Turing Machine halts; the reasoning might go that the existence of such a procedure implies ability to construct a complete $\omega$-consistent theory. Is this correct? Are there any results along these lines?

(I'm asking out of curiosity -- I don't study logic myself -- so I apologize if this is well-known or not research-level. In that case, consider this a reference request! Thanks for any comments or responses!)

Question that sounds related, but isn't: Church's Theorem and Gödel's Incompleteness Theorems

EDIT: I'll try to make the question more clear! First -- my naive intuition is that Gödel's Incompleteness should imply at least some limitations on what is or is not computable. These limitations would be unconditional, i.e., they should apply to all models of computation rather than just Turing Machines.

So I am wondering if this is the case (there must be some implication, right?). Assuming it is, I'm most curious about how it impacts the Church-Turing Thesis -- the notion that anything effectively calculable can be computed by a Turing Machine. For example, it seems possible that the existence of an effective procedure for deciding whether a Turing Machine halts would contradict the First Incompleteness Theorem. This result would demonstrate that no possible method of computation can be "much" more powerful than Turing Machines; but is this result true? I have a couple similar questions in the comments. I would be very interested to hear an answer to one of these questions, a pointer to an answer in the literature, an explanation of why my entire reasoning is off-base, or any other comments!

• Both proofs give the same result and need similar assumptions. None of them needs Church-Turing Thesis. CTT is only needed if you want to make a claim about vague and intuitive concept of "algorithmic computability". – Kaveh Dec 2 '12 at 6:14
• ps: the question seems more suitable for Computer Science or Mathematics. – Kaveh Dec 2 '12 at 6:17
• I do not understand the question. Can someone explain what is being asked? – Andrej Bauer Dec 2 '12 at 20:19
• I don't agree that this question is more appropriate for CS or Mathematics. It seems right on topic here: the main problem is trying to pin down what's being asked, and that discussion is ongoing. – Suresh Venkat Dec 2 '12 at 22:12
• tl;dr: Theorems cannot formally imply anything about intuitive notions. The Church-Turing thesis is an informal statement about the intuitive notion of "effective computation". Therefore, Gödel's theorems cannot formally imply anything about the Church-Turing thesis. – Jeffε Dec 3 '12 at 7:31

Here is a philosophical answer that may entertain you.

Gödel's incompleteness theorems are about the formal system of Peano arithmetic. As such they say nothing about models of computation, at least not without some amount of interpretation.

Peano arithmetic easily shows existence of non-computable functions. For example, being a classical theory expressive enough to talk about Turing machines, it shows the particular instance of excluded middle which says that every Turing machine halts or runs forever. Nevertheless, from the work of Gödel an important notion of computability arose, namely that of a (primitive) recursive function. So it is not the theorems themselves that connect to computability, but rather the method of proof which establishes them.

The gist of the incompleteness theorems can be expressed in an abstract form using provability logic, which is a kind of modal logic. This gives the incompleteness theorems a wide range of applicability well beyond Peano arithmetic and computability. As soon as certain fixed-point principles are satisfied, incompleteness kicks in. These fixed-point principles are satisfied by traditional computability theory, which therefore falls victim to incompleteness, by which I mean existence of inseparable c.e. sets. Because the provable and refutable sentences of Peano arithmetic form inseparable c.e. sets, the traditional Gödel's incompleteness theorems can be seen as a corollary to incompleteness phenomena in computability. (I am being philosophically vague and your head will hurt if you try to understand me as a mathematician.)

I suppose we can take two stands on how all this relates to the informal notion of effectivity ("stuff that can actually be computed"):

1. For all we know, we are just a rather large finite automaton, capable of contemplating fictional super-heroes called "Turing machines" that are able to calculate with unbounded numbers (gasp!). If this is the case, Gödel was just a very good story-teller. How his stories translate to effectivity is then a matter of some (necessarily inaccurate) application of imagination to reality.

2. Because incompleteness phenomena arise naturally in many contexts, and certainly in all reasonable notions of computability, we conclude that the same has to be the case for effectivity. For example, suppose we could send Turing machines into black holes to compute a la Joel Hamkin's infinite-time Turing machines. This gives us immense computational power in which the halting oracle is a kindergarten toy. But still, the model satisfies the basic conditions that allow us to show the existence of inserparable sets. And therefore once again, computation is not all-powerful and incompleteness is a fact of life.

• A minor addendum to Andrej's answer: provability logic shows up over and over again all over logic and CS. In lies at the heart of the modal mu-calculus and temporal logic, calculi for multistage computation, and the metric semantics of recursive types. This recurrence suggests that Goedel's result is really about self-reference, and that the heart of his proof is the fixed point theorem which shows that numbers can encode syntax trees. (Less exaltedly, Goedel's fixed point theorem says you can write all formulas in ASCII!) – Neel Krishnaswami Dec 3 '12 at 14:44
• Philosophical, entertaining, and also very instructive -- thank you! – usul Dec 3 '12 at 22:31
• For all we know, we are just a rather large finite automaton... — "For all we know"? Isn't this obvious? – Jeffε Dec 4 '12 at 19:03
• We could be a medium-sized finite automaton. – Andrej Bauer Dec 4 '12 at 22:50
• @JɛﬀE Those are just the points at which our current understanding of physics breaks down, not necessarily where nature itself does. I'm a 'discretist' myself at heart (I lean towards some form of loop quantum gravity), but ruling out true analog computation of one form or another seems legitimately hard. – Steven Stadnicki Dec 6 '12 at 0:51

I would like to emphasis Neel's comment, the main tools for both undecidability of halting and Godel's incompleteness theorems are:

1. encoding syntactic concepts like proofs, computation, etc. by numbers/strings and relations/functions over them;
2. Godel's fixed point theorem.

The encoding of syntactic objects and concepts might seem obvious today that we are used to digital computers but it is an ingenious idea essential for universal computers and software. All that is needed for proving existence of a universal simulator are in his paper.

Godel also shows that we can represent these syntactic concepts and generally TM computable relations/functions by simple arithmetical formulas.

Godel's incompleteness proof in short is as follows:

Let $T$ be a strong enough consistent theory with c.e. axioms, then

1. there is a formula $Provable_T(x)$ in the language of $T$ that represents provability of the formula encoded by $x$ in $T$,
2. by Godel's fixed point theorem, there is a formula $G$ which is a fixed point for $\lnot Provable(x)$, i.e. $T \vdash G \leftrightarrow \lnot Provable_T(\ulcorner G \urcorner)$.

Undecidability of halting problem for TMs uses similar ingredients:

1. there is a TM $Halt(x)$ that recognizes if the TM encoded by $x$ halts,
2. Kleene's fixed point to find a TM $N$ s.t. $N$ accepts iff $\lnot Halt(\langle M \rangle)$ accepts.

Undecidability of halting for TMs gives incompleteness because we can represent $Halt(x)$ in $T$ and we can computably enumerate the theorems of $T$, and if $T$ is complete we can decide whether a given TM halts or not by checking if the corresponding formula is provable in $T$.

The reverse is also simple: if a theory $T$ is c.e., then the provability in $T$ is decidable using the halting problem, therefore we could construct a complete theory by just adding more and more formulas whose negations are not provable. Therefore if the halting problem was decidable, then we could have a complete c.e. extension of $T$.

The proofs are very similar and use the same ingredients (though for someone whose is more familiar with TMs but not much with logic the undecidability of halting problem might look simpler: the particular instance of fixed point theorem used in the undecidability proof might look simpler than the particular instance of the fixed point used in Godel's theorem though they are essentially the same, but the essential ideas are just encoding syntactic objects and concepts using numbers/strings and formulas/functions about them, and applying a fixed point theorem).

I think you can use stronger models of computation for the theorems, you can take computability w.r.t. oracle $O$, consider the halting problem for TM's with access to oracle $O$, and consider arithmetic which has a predicate $P_O(x)$ and axioms defining the graph of $O$. We will have a similar situation for computability with respect to $O$.

ps:
Note that Godel's theorems are published in 1931, whereas Turing's undecidability is published in 1936. At the time of publication of Godel's paper TMs were not defined and Godel was using another equivalent model. IIRC, Godel was not completely satisfied with his result as settling the original goal of Hilbert's program because he was not convinced that the model of computation he used really captured the intuitive notion of algorithmic computability, he was only satisfied after Turing's philosophical argument about TMs capturing the intuitive notion of algorithmic computability. I think you can read more about this in Godel's collected works.

• Awesome, thanks, this is also very illuminating! – usul Dec 4 '12 at 20:26