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!
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"):


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.
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.