<p>I would like to emphasis <a href="https://cstheory.stackexchange.com/questions/14565/the-relation-of-godels-incompleteness-theorems-to-the-church-turing-thesis#comment39499_14589">Neel's comment</a>, the main tools for both undecidability of halting and Godel's incompleteness theorems are: </p>

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

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

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

<p>Godel's incompleteness proof in short is as follows: </p>

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

<ol>
<li>there is a formula $Provable_T(x)$ in the language of $T$ that represents provability of the formula encoded by $x$ in $T$,</li>
<li>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)$.</li>
</ol>

<p>Undecidability of halting problem for TMs uses similar ingredients: </p>

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

<p>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$.</p>

<p>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$.</p>

<p>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).</p>

<p>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$.</p>

<p>ps:<br>
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.</p>

CC BY-SA 3.0
2012-12-04T20:26:39.330Z
Awesome, thanks, this is also very illuminating!
usul
CC BY-SA 4.0
2023-08-07T09:15:12.250Z
Does Kleene fixed point theorem case lead to form of modal logic as well?
uhbif19
CC BY-SA 3.0
2012-12-04T07:47:12.180Z
2012-12-04T23:24:53.327Z
2017-04-13T12:32:28.743Z
Kaveh
<p>Here is a philosophical answer that may entertain you.</p>

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

<p>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 <em>(primitive) recursive function</em>. So it is not the theorems themselves that connect to computability, but rather the <em>method</em> of proof which establishes them.</p>

<p>The gist of the incompleteness theorems can be expressed in an abstract form using <a href="http://plato.stanford.edu/entries/logic-provability/">provability logic</a>, 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.)</p>

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

<ol>
<li><p>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.</p></li>
<li><p>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 <a href="http://jdh.hamkins.org/asurveyofinfinitetimeturingmachines/">Joel Hamkin's infinite-time Turing machines</a>. 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.</p></li>
</ol>

CC BY-SA 3.0
2012-12-03T14:44:07.747Z
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
CC BY-SA 3.0
2012-12-03T22:31:38.840Z
Philosophical, entertaining, and also very instructive -- thank you!
usul
CC BY-SA 3.0
2012-12-03T22:37:56.107Z
*"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."* This (with Kaveh's comment on Turing-equivalence) seems to give a semi-concrete question: If we were to find an effective means of computation that could decide if a given TM halts, would that imply that we could construct a complete, consistent model of arithmetic? (Or at least decide if Peano arithmetic is both?) (I'd argue this reduction seems relevant to Church-Turing also.)
usul
CC BY-SA 3.0
2012-12-04T01:21:55.927Z
Sure, isn't this what kaveh said in one of his comments?
Andrej Bauer
CC BY-SA 3.0
2012-12-04T19:03:01.133Z
_For all we know, we are just a rather large finite automaton..._ — "For all we know"?  Isn't this obvious?
Jeffε
CC BY-SA 3.0
2012-12-04T22:50:08.967Z
We could be a medium-sized finite automaton.
Andrej Bauer
CC BY-SA 3.0
2012-12-05T23:28:51.227Z
@JɛﬀE That likely depends on what you think the underlying computation model of the universe is!  It's at least conceivable that we're arbitrary-precision analog computers and thus could actually have 'infinite' data packed into us... (n.b.: I don't necessarily subscribe to this view myself, but it's legitimately scientific and I don't know of anything that rules it out)
Steven Stadnicki
CC BY-SA 3.0
2012-12-06T00:01:43.073Z
@StevenStadnicki  http://en.wikipedia.org/wiki/Planck_length and http://en.wikipedia.org/wiki/Planck_time ?
Jeffε
CC BY-SA 3.0
2012-12-06T00:51:31.877Z
@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
CC BY-SA 4.0
2023-08-07T09:34:59.740Z
@NeelKrishnaswami Could you provide some keywords/papers on those links to mu-calculus/temporal logic?
uhbif19
CC BY-SA 3.0
2012-12-03T14:13:27.137Z
2012-12-03T14:13:27.137Z
Andrej Bauer
<p>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?)</p>

<p>Gödel's First Incompleteness Theorem can be proven as a corollary of the undecidability of the halting problem (e.g. Sipser Ch. 6; <a href="http://www.scottaaronson.com/blog/?p=710" rel="nofollow noreferrer">blog post by Scott Aaronson</a>).</p>

<p>From what I understand (confirmed by the comments), this proof does <em>not</em> 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 <em>effective procedure</em> could decide the halting problem, we would need to also assume the Church-Turing thesis to get a contradiction.)</p>

<p>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.)</p>

<p>My question is whether we can gain something more concrete by going in reverse: <strong>What formal implications do Gödel's theorems have for the Church-Turing thesis?</strong> 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?</p>

<p>(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!)</p>

<p>Question that sounds related, but isn't: <a href="https://cstheory.stackexchange.com/questions/1612/churchs-theorem-and-godels-incompleteness-theorems">Church's Theorem and Gödel's Incompleteness Theorems</a></p>

<hr>

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

<p>So I am wondering if this is the case (there must be <em>some</em> 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!</p>

CC BY-SA 3.0
2012-12-02T06:14:50.363Z
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
CC BY-SA 3.0
2012-12-02T06:17:36.883Z
ps: the question seems more suitable for [cs.se] or [math.se].
Kaveh
CC BY-SA 3.0
2012-12-02T07:43:04.790Z
@Kaveh thanks for the response. I'm not sure if the story I'm trying to tell is clear, but I am actually interested in what *formal/precise* claims we can make about "algorithmic computability" when starting from Gödel. (The motivation comes from the more fuzzy support for the CTT that we seem to get from the proof of Incompleteness using halting.) I may try posting to math or logic later if this post doesn't work out.
usul
CC BY-SA 3.0
2012-12-02T20:19:55.093Z
I do not understand the question. Can someone explain what is being asked?
Andrej Bauer
CC BY-SA 3.0
2012-12-02T21:54:59.730Z
Sorry that I'm unclear! It is vague/open-ended. Let me illustrate with related/specific questions: (1) What do the Incompleteness Theorems prove about the limits of computability (independent of the model of computation)? (2) *E.g.*, do they show that no model of computation can effectively decide whether a Turing Machine halts? (3) Is the construction of a consistent, complete formal system Turing-equivalent to the halting problem? To some more "difficult" computational problem? (4) Do there seem to be "gaps" between the power of Turing Machines and the limitations implied by Incompleteness?
usul
CC BY-SA 3.0
2012-12-02T21:55:57.313Z
Answers to such questions might provide more concrete support to (or cast doubt on!) the notion that Turing-completeness fully captures the notion of "effectively calculable". I hope that helps show what I'm asking.
usul
CC BY-SA 3.0
2012-12-02T22:12:01.850Z
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
CC BY-SA 3.0
2012-12-02T22:58:12.420Z
I appear to be doing badly at that, haha, but I may lack the expertise to ask a more precise/better-phrased question. Also, as an interested non-expert with an open-ended question, I would be very happy with thoughts/comments/references on the topic, rather than expecting some definitive case-closed "solution" type of response!
usul
CC BY-SA 3.0
2012-12-03T00:31:33.050Z
I think I'll reserve judgement on that till we decide what the question actually is.
Suresh Venkat
CC BY-SA 3.0
2012-12-03T06:32:44.537Z
Godel's theorems don't imply anything about "the intuitive notion of computability", the theorem holds only for theories which are *recursively enumerable* and here recursively enumerable is enumerability of axioms by Turing machines. Your confusion comes from not knowing that Godel's theorem is about such theories and the notion of computability is explicitly stated in the theorems. (this is the reason I think this is not suitable for cstheory, i.e. you don't seem to know the basics about logic and Godel's theorems.)
Kaveh
CC BY-SA 3.0
2012-12-03T06:50:42.230Z
"What do the Incompleteness Theorems prove about the limits of computability (independent of the model of computation)?" *nothing, they are not about models of computation*, "do they show that no model of computation can effectively decide whether a Turing Machine halts?" *obviously no, take TM's with an oracle for the Halting problem for TMs*
Kaveh
CC BY-SA 3.0
2012-12-03T06:50:56.443Z
"Is the construction of a consistent, complete formal system Turing-equivalent to the halting problem?" *depends on what you mean by a formal system, for first-order arithmetic which the theorems talk about, the answer is yes* "Do there seem to be "gaps" between the power of Turing Machines and the limitations implied by Incompleteness?" *the theorems are not about models of computations, they don't imply a limitation on models of computation, they are about a specific model of computation in which we assume the axioms of the theory are enumerable, and extensions of a specific theory.*
Kaveh
CC BY-SA 3.0
2012-12-03T06:59:50.140Z
ps: the more general questions of how hard it is to compute a consistent complete extension of a given consistent theory is well studied in computable model theory, in short Henkin's construction can be made effective if we can decide provability in the theory, so the complete extension is in the Turing-jump of the the theory (IIRC). Another simple trick is to encode the graph of an arbitrary partial function using a function symbol and stating axioms for the partial values, a complete extension of the theory will give a total extension of the partial function.
Kaveh
CC BY-SA 3.0
2012-12-03T07:31:27.320Z
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ε
CC BY-SA 3.0
2012-12-03T13:56:17.490Z
Another way of putting it: the Church-Turing thesis is essentially about what we mean by the word *computability*: not about properties of any particular mathematical way to model computability.
reinierpost
CC BY-SA 3.0
2012-12-03T22:13:55.157Z
@Kaveh thanks for the responses; you are exactly right about my confusion (I had foolishly and incorrectly assumed that, as Gödel's proofs preceded Church's and Turing's, they did not rely on any sort of "universal" model of computation like $\mu$-recursive functions). That is very interesting!
usul
<lo.logic><computability><church-turing-thesis>
The relation of Gödel's Incompleteness Theorems to the Church-Turing Thesis
usul
# The relation of Gödel's Incompleteness Theorems to the Church-Turing Thesis

(Asked by: username_0 on 2012-12-02)

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](http://www.scottaaronson.com/blog/?p=710)).

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](https://cstheory.stackexchange.com/questions/1612/churchs-theorem-and-godels-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!

**Tags:** lo.logic, computability, church-turing-thesis

> **Comments:**
> **username_1**: 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".  
> **username_1**: ps: the question seems more suitable for [cs.se] or [math.se].  
> **username_0**: @username_1 thanks for the response. I'm not sure if the story I'm trying to tell is clear, but I am actually interested in what *formal/precise* claims we can make about "algorithmic computability" when starting from Gödel. (The motivation comes from the more fuzzy support for the CTT that we seem to get from the proof of Incompleteness using halting.) I may try posting to math or logic later if this post doesn't work out.  
> **username_2**: I do not understand the question. Can someone explain what is being asked?  
> **username_0**: Sorry that I'm unclear! It is vague/open-ended. Let me illustrate with related/specific questions: (1) What do the Incompleteness Theorems prove about the limits of computability (independent of the model of computation)? (2) *E.g.*, do they show that no model of computation can effectively decide whether a Turing Machine halts? (3) Is the construction of a consistent, complete formal system Turing-equivalent to the halting problem? To some more "difficult" computational problem? (4) Do there seem to be "gaps" between the power of Turing Machines and the limitations implied by Incompleteness?  
> **username_0**: Answers to such questions might provide more concrete support to (or cast doubt on!) the notion that Turing-completeness fully captures the notion of "effectively calculable". I hope that helps show what I'm asking.  
> **username_3**: 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.  
> **username_0**: I appear to be doing badly at that, haha, but I may lack the expertise to ask a more precise/better-phrased question. Also, as an interested non-expert with an open-ended question, I would be very happy with thoughts/comments/references on the topic, rather than expecting some definitive case-closed "solution" type of response!  
> **username_3**: I think I'll reserve judgement on that till we decide what the question actually is.  
> **username_1**: Godel's theorems don't imply anything about "the intuitive notion of computability", the theorem holds only for theories which are *recursively enumerable* and here recursively enumerable is enumerability of axioms by Turing machines. Your confusion comes from not knowing that Godel's theorem is about such theories and the notion of computability is explicitly stated in the theorems. (this is the reason I think this is not suitable for cstheory, i.e. you don't seem to know the basics about logic and Godel's theorems.)  
> **username_1**: "What do the Incompleteness Theorems prove about the limits of computability (independent of the model of computation)?" *nothing, they are not about models of computation*, "do they show that no model of computation can effectively decide whether a Turing Machine halts?" *obviously no, take TM's with an oracle for the Halting problem for TMs*  
> **username_1**: "Is the construction of a consistent, complete formal system Turing-equivalent to the halting problem?" *depends on what you mean by a formal system, for first-order arithmetic which the theorems talk about, the answer is yes* "Do there seem to be "gaps" between the power of Turing Machines and the limitations implied by Incompleteness?" *the theorems are not about models of computations, they don't imply a limitation on models of computation, they are about a specific model of computation in which we assume the axioms of the theory are enumerable, and extensions of a specific theory.*  
> **username_1**: ps: the more general questions of how hard it is to compute a consistent complete extension of a given consistent theory is well studied in computable model theory, in short Henkin's construction can be made effective if we can decide provability in the theory, so the complete extension is in the Turing-jump of the the theory (IIRC). Another simple trick is to encode the graph of an arbitrary partial function using a function symbol and stating axioms for the partial values, a complete extension of the theory will give a total extension of the partial function.  
> **username_4**: 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.  
> **username_5**: Another way of putting it: the Church-Turing thesis is essentially about what we mean by the word *computability*: not about properties of any particular mathematical way to model computability.  
> **username_0**: @username_1 thanks for the responses; you are exactly right about my confusion (I had foolishly and incorrectly assumed that, as Gödel's proofs preceded Church's and Turing's, they did not rely on any sort of "universal" model of computation like $\mu$-recursive functions). That is very interesting!  

---

## 2 answers

### Answer by username_2 on 2012-12-03. Score: 12 | Accepted answer

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](http://plato.stanford.edu/entries/logic-provability/), 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](http://jdh.hamkins.org/asurveyofinfinitetimeturingmachines/). 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.

> **Comments:**
> **username_7**: 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!)  
> **username_0**: Philosophical, entertaining, and also very instructive -- thank you!  
> **username_0**: *"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."* This (with username_1's comment on Turing-equivalence) seems to give a semi-concrete question: If we were to find an effective means of computation that could decide if a given TM halts, would that imply that we could construct a complete, consistent model of arithmetic? (Or at least decide if Peano arithmetic is both?) (I'd argue this reduction seems relevant to Church-Turing also.)  
> **username_2**: Sure, isn't this what kaveh said in one of his comments?  
> **username_4**: _For all we know, we are just a rather large finite automaton..._ — "For all we know"?  Isn't this obvious?  
> **username_2**: We could be a medium-sized finite automaton.  
> **username_8**: @JɛﬀE That likely depends on what you think the underlying computation model of the universe is!  It's at least conceivable that we're arbitrary-precision analog computers and thus could actually have 'infinite' data packed into us... (n.b.: I don't necessarily subscribe to this view myself, but it's legitimately scientific and I don't know of anything that rules it out)  
> **username_4**: @StevenStadnicki  http://en.wikipedia.org/wiki/Planck_length and http://en.wikipedia.org/wiki/Planck_time ?  
> **username_8**: @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.  
> **username_6**: @NeelKrishnaswami Could you provide some keywords/papers on those links to mu-calculus/temporal logic?  

---

### Answer by username_1 on 2012-12-04. Score: 9

I would like to emphasis [Neel's comment](https://cstheory.stackexchange.com/questions/14565/the-relation-of-godels-incompleteness-theorems-to-the-church-turing-thesis#comment39499_14589), 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.

> **Comments:**
> **username_0**: Awesome, thanks, this is also very illuminating!  
> **username_6**: Does Kleene fixed point theorem case lead to form of modal logic as well?  

---

