<blockquote>
  <p>can we essential say that the concept
  of provability in a formal system
  (proof calculus) is identical to the
  concept of computability in recursion
  theory (Turing machines/lambda
  calculus)?</p>
</blockquote>

<p>These are very similar but not identical, because some of the steps in the proof calculus may represent non-computable operations.</p>

<p>For example, you could have a proof assistant verify a $ZFC$ proof that the powerset of the naturals $\wp(N)$ exists, and this will be a short proof with two steps (Axiom of Infinity followed by Axiom of Powerset), but neither of these steps are themselves computable.</p>

<p>Similarly, G&ouml;del's Completeness Theorem tells us that any valid formula in first order logic has a proof, but Trakhtenbrot's Theorem tells us that, over finite models, the validity of first order formulae is undecideable.  </p>

<p>So finite proofs don't necessarily correspond to computable operations. </p>

CC BY-SA 2.5
2011-01-13T02:07:14.480Z
@Marc: Noldorin's question talks about algorithms producing a proof, not about algorithms which perform steps of a proof. In your example, it is interesting whether an automatic theorem prover could produce the proof of existence of P(N), and whether it can produce a proof in every case.
You're basically stating that steps of a proof are not effective, or that classical logic is not constructive - the usual example is that you can prove the existence of something by contradiction, your one is more original.
Blaisorblade
CC BY-SA 2.5
2011-01-13T13:44:29.587Z
@Blaisorblade: Computation is necessarily constructive, mathematics is not.  Many people get themselves confused when they assume that all that is true in computation and all that is true in classical mathematics are the same (possibly modulo "a few simple rules").  Understanding the distinction between the two is at the heart of my answer to this question; I just gave what I think is the most straightforward way of explaining it.
Marc Hamann
CC BY-SA 2.5
2010-09-24T16:54:31.173Z
Thanks for your answer. So to clarify, how exactly are those steps of your example not computable - in what sense, should I say? To clarify, when I say proofs are computable, I mean that the rules of inference are computable... (Is there any other way of thinking about it?)
Noldorin
CC BY-SA 2.5
2010-09-24T17:28:42.533Z
The set of naturals is recursively enumerable, but an attempt to generate all the naturals would obviously not terminate, so it isn't strictly computable.  The powerset of the naturals isn't even recursively enumerable, and most elements of it aren't recursively enumerable, so it is "even less" computable.
Marc Hamann
CC BY-SA 2.5
2010-09-24T17:34:33.663Z
Your other question about how to think about this is rather trickier and bigger in scope than I think is suitable here.  Suffice it to say that if you consider non-computable steps with computable inference rules to be computable, then the Halting Problem is computable by simply assuming an Axiom of Halting that posits a halting oracle.   Seems like cheating to me. ;-)
Marc Hamann
CC BY-SA 2.5
2010-09-24T21:09:16.700Z
@Marc: The book I'm reading at the moment says that the set of all natural numbers *is* computable in that if you input n to the Turing machine, the machine can output the nth natural number. Indeed, the powerset cannot be computed by a Turing machine.
Noldorin
CC BY-SA 2.5
2010-09-24T21:16:02.230Z
Also, I'm not sure I quite follow your reasoning about assuming an Axiom of Halting... Turing machines don't have "axioms" so to speak? I think I still need to be convinced that "all valid proofs in a formal system are computable proofs" is not true. This strikes me as intuitively correct.
Noldorin
CC BY-SA 2.5
2010-09-24T21:20:46.170Z
And it would seem the answer to the halting problem is a direct consequence of Church's theorem, which interestingly uses something very akin to Godel numbering in its proof...
Noldorin
CC BY-SA 2.5
2010-09-25T02:12:17.957Z
@Noldorin: I'm not sure which book you are reading, but what you described is the same thing as recursively enumerable.
Marc Hamann
CC BY-SA 2.5
2010-09-25T02:13:53.710Z
Turing machines don't have axioms, but proof systems do.  The whole point is that a proof system with non-computable axioms can do things that TMs can't.
Marc Hamann
CC BY-SA 2.5
2010-09-25T02:19:16.937Z
The halting problem is not soluble by any computational system.  This is a pretty basic fact of the theory of computation, and I would recommend any basic text in that area to clarify this issue for you.
Marc Hamann
CC BY-SA 2.5
2010-09-25T14:20:11.037Z
@Marc: I think you misunderstand my question. Of course I understand the halting problem, the question goes somewhat deeper...
Noldorin
CC BY-SA 2.5
2010-09-26T16:25:56.177Z
@Marc: It seems I sort of have the answer to that part of the question with the Curry-Howard isomorphism though. :) Thanks for all your help!
Noldorin
CC BY-SA 2.5
2010-09-23T20:24:02.233Z
2010-09-23T20:24:02.233Z
Marc Hamann
<p>Although this is not quite what you are asking about, it is in the same vein and hopefully you (and other readers of your question) will find it of interest.  You should definitely read up on the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard correspondence</a>, which says that the category of programs is, in a specific sense, isomorphic to the category of <em>constructive</em> proofs.  (This is discussing proofs and computability at a different level than the other answers.)</p>

CC BY-SA 2.5
2010-09-26T13:16:34.410Z
Absolutely... I was aware of the Curry-Howard correspondence but didn't want to bring it in to the question and complicate things further. Thanks for pointing it out though. I'm not quite sure if this is the link I'm looking for, or if it's somewhat more restrictive/narrow than I want to saw. What do you think, are there any clarifications to be made here?
Noldorin
CC BY-SA 2.5
2010-09-26T01:26:26.887Z
2010-09-26T01:26:26.887Z
Joshua Grochow
<p>I'll try to answer your question from the point of view you take, in short; I'm also trying to relate the two theorems in a different way.</p>

<p>Gödel's first incompleteness theorem states that in a consistent formal system with sufficient arithmetic power, there is a statement P such that no proof either of it or of its negation exists. This does not imply that there is no decision algorithm for the set of theorems of the theory, which would also say that nor P nor not P are theorems. Church-Turing's theorem result says that such an algorithm does not exist. That's the also the core of the answer by Kaveh, I hope to have explained it clearer.</p>

<p>I'll now try to prove that Church-Turing's theorem implies Gödel's theorem, please explain me where and if I'm wrong.
The set of theorems Thm is partially decidable, and suppose R is a program which recognizes it (i.e., halts with "yes" if the input is in Thm, continues running otherwise).
Let's use this to build a new algorithm: Given a statement Q, to see whether it's provable, run R in parallel on Q and not Q, by interleaving their execution, and stopping when the first of them halts, and producing "No" if "not Q" was proved, and "Yes" otherwise; this gives a computable algorithm. Assuming by contradiction that all statements can be proved or disproved, this algorithm would solve the Entscheidungsproblem, but that's absurd! Therefore, there must be a statement which can't be proved or disproved.</p>

CC BY-SA 2.5
2011-01-13T02:26:04.227Z
2011-01-13T02:26:04.227Z
Blaisorblade
<p>First, I suggest you read Kleene's &quot;Metamathematics&quot; as a good book on these topics. First two chapters of volume I of Odifreddi's &quot;Classical Recursion Theory&quot; can also be helpful in understanding the relation between these concepts.</p>
<blockquote>
<p>We know that Church's theorem (or rather, the independent proofs of Hilbert's Entscheidungsproblem  by Alonzo Church and Alan Turing) proved that in general we cannot calculate whether a given mathematical statement in a formal system is true or false.</p>
</blockquote>
<p>I think you are referring to Church's theorem that the set of theorems of first order logic is not decidable. It is important to note that the language is first order.</p>
<blockquote>
<p>As I understand, the Church-Turing thesis provides a pretty clear description of the equivalence (isomorphism) between Church's lambda calculus and Turing machines, hence we effectively have a unified model for computability.</p>
</blockquote>
<p>No. The equivalence if lambda-computability and Turing-computability is a <em>theorem</em> of Kleene. It is not a thesis. It is considered as evidence supporting Church's thesis.</p>
<blockquote>
<p>Note: As far as I know, Turing's proof makes use of the fact that the halting problem is undecidable. Correct me if I'm wrong.</p>
<p>Now, Gödel's first incompleteness theorem states that not all statements in a consistent formal system may be proven within this system. In many ways, this appears to me to be saying exactly the same thing to me as Church's theorems, considering lambda calculus and Turning machines are both effectively formal systems of sorts!</p>
</blockquote>
<p>No. Godel's theorem states that for every <span class="math-container">$\omega$</span><em>-consistent</em>, <em>recursively enumerable</em> theory which <em>contains enough arithmetic</em>, there is a sentence <span class="math-container">$\varphi$</span> s.t. <span class="math-container">$\varphi$</span> and <span class="math-container">$\lnot \varphi$</span> are not provable in it.</p>
<p>This does not state the same thing. It does not say anything about set of theorems of the theory being undecidable.</p>
<blockquote>
<p>This is however my holistic interpretation, and I was hoping someone could shed some light on the details. Are these two theorems effectively equivalent? Are there any subtleties to be observed? If these theories are essentially looking at the same universal truth in different ways, why were they approached from such different angles? (There were more or less 6 years between Godel's proof and Church's).</p>
</blockquote>
<p>Over the years there has been lots of abuse of Godel's theorems (and similar theorems). One should be very careful in making interpretations of them. As far as I have seen, the abuses are usually result of forgetting to mention some condition in the theorem or combining the theorems by some other beliefs. A careful look shows that theses theorems, although related, are not equivalent.</p>
<blockquote>
<p>Finally, can we essential say that the concept of provability in a formal system (proof calculus) is identical to the concept of computability in recursion theory (Turing machines/lambda calculus)?</p>
</blockquote>
<p>I don't understand what you mean by &quot;identical&quot;. Certainly there are many relations between computability and provability. I may be able to make a more helpful comment if you clarify what you mean by these being identical.</p>
<h3>update</h3>
<p>Lets consider the set of well-formed sentences in the language of arithmetic as <span class="math-container">$L$</span>. Let <span class="math-container">$T$</span> be (the axioms of) a theory satisfying the conditions of first incompleteness theorem. Let <span class="math-container">$Thm(T)$</span> be the set of theorems of the theory <span class="math-container">$T$</span> and <span class="math-container">$\lnot Thm(T)$</span> be the set of sentences whose negation is a theorem of <span class="math-container">$T$</span>. Let <span class="math-container">$True$</span> be the set of sentences that are true in the standard model, and <span class="math-container">$False$</span> the set of false sentences. A sentence is in <span class="math-container">$True$</span> iff its negation is in <span class="math-container">$False$</span>. Also every sentence is either true or false, i.e. <span class="math-container">$L = True \cup False$</span>.</p>
<p>The Godel's incompleteness theorem states that <span class="math-container">$Thm(T) \cup \lnot Thm(T)$</span> is a proper subset of <span class="math-container">$L$</span>. Therefore truth in the standard model and provability in <span class="math-container">$T$</span> are different.</p>
<p>Note that <span class="math-container">$Thm(T)$</span> is r.e., Church's theorem states that <span class="math-container">$Thm(T)$</span> is not decidable.</p>
<p>On the relation between provability in formal system and computability. One is the following: If the system is effective, then the set of derivable expression in it is r.e., and the system is a special case of a grammar. Grammars is another way for defining the concept of computable which is equivalent to Turing machine computability.</p>

CC BY-SA 2.5
2010-09-24T16:57:59.107Z
Thanks for your answer. I refer to Church's theorem as stated on the Wikipedia page: "In 1936 and 1937 Alonzo Church and Alan Turing respectively[1], published independent papers showing that it is impossible to decide algorithmically whether statements in arithmetic are true or false. This result is now known as Church's Theorem or the Church–Turing Theorem (not to be confused with the Church–Turing thesis).". Cheers for the correction on the Church-Turing thesis too, I shall make note of that. Are you in accordance with David Thornley's comment on my question then?
Noldorin
CC BY-SA 2.5
2010-09-24T17:03:01.093Z
Regarding the description of Godel's first incompleteness theorem, I fully accept your (more precise) definition, though is it not equivalent to my corrected version in the question/the comment on Marc Hamann's answer? Finally, is there any way we can be specific about how exactly these theorems relate to each other, despite not being equivalent?
Noldorin
CC BY-SA 2.5
2010-09-24T17:13:13.913Z
Oh, and regarding my meaning of "identical". Perhaps you could amend the following statement so that it's correct (adding necessary conditions/caveats): Any valid proof in a consistent formal system may be represented by a computable function in a Turing machine?
Noldorin
CC BY-SA 2.5
2010-09-24T17:47:04.670Z
The theory should be r.e. otherwise incompleteness theorem does not hold. (take all true sentences in the standard model, it satisfies all other conditions.) I will add an update to my answer.
Kaveh
CC BY-SA 2.5
2010-09-24T18:02:52.923Z
"Any valid proof in a consistent formal system may be represented by a computable function in a Turing machine?" I don't understand what you mean by "represent". A proof is just a finite string of symbols.
Kaveh
CC BY-SA 2.5
2010-09-24T21:04:43.617Z
I have heard the term "recursively enumerable" applied to sets, but not to theories. What do you mean by a theory being r.e.? Also, by "represent", I mean there exists some isomorphism between A and B.
Noldorin
CC BY-SA 2.5
2010-09-24T21:18:19.340Z
Ah, I suspect when you say a theory is recursively enumerable, you mean the set of all theorems is such(?) I suppose there exist many formal systems that are not r.e. then...
Noldorin
CC BY-SA 2.5
2010-09-26T11:47:11.813Z
Yes, of course there are formal systems which are not effective. And about the isomorphism between proofs and computable functions, see Joshua's answer about proofs (in some formal systems) and programs (not computable functions). And in the Curry-Howard isomorphism what would correspond to a computable function is a formula, not a proof.
Kaveh
CC BY-SA 2.5
2010-09-26T14:12:12.810Z
A possible source of your confusion can be the fact that many words in logic are overloaded, like the word "decide". It is both used for a theory being "complete" as in Godel's theorem and for the set of theorems of a theory being recursive as in Church's theorem. (The word "complete" is also overloaded.) The relation of these topics with philosophy and other sciences has made their misuse common specially in popular science related works. Reading a good *textbook* on these topics (recursion/computability theory, logic, incompleteness theorem, ...) can clarify the picture.
Kaveh
CC BY-SA 2.5
2010-09-26T16:28:00.353Z
@Kaveh: Thanks again for the clarification. I know what you mean about overloaded terms, and indeed about pop sci too. (I garnered a fair amount of my information from *An Emperor's New Mind*. The author is of course highly distinguished, though it's always easy to misinterpret). I have two good answers here, but I'll gladly accept yours for the degree of thoroughness. :)
Noldorin
CC BY-SA 2.5
2010-09-26T16:51:48.893Z
Thank you. :) Roger Penrose is of course highly distinguished, but don't forget that there are also many other highly distinguished experts who disagree with him (, which is completely normal in philosophy). Note: Odifreddi's book also contains a short discussion on these issues.
Kaveh
CC BY-SA 2.5
2010-09-26T19:12:51.180Z
@Kaveh: Oh, sure. I do however believe that what he has to say about the foundations of mathematics and computability theory is fairly uncontroversial. His discussions of the nature of the mind, intelligence, and consciousness are however much more novel/controversial (they disagree at the core with the ideas in the other famous pop sci book on the subject; Godel, Escher and Bach).
Noldorin
CC BY-SA 2.5
2010-09-23T23:04:31.790Z
2010-09-24T18:04:53.747Z
2020-06-17T09:38:08.363Z
Kaveh
<p>I have recently been reading up on some of the ideas and history of the ground-breaking work done by various logicians and mathematicians regarding computability. While the individual concepts are fairly clear to me, I'm am trying to get a firm grasp of there inter-relations and the abstract level at which they are all linked.</p>

<p>We know that Church's theorem (or rather, the independent proofs of Hilbert's <a href="http://en.wikipedia.org/wiki/Entscheidungsproblem">Entscheidungsproblem</a> by Alonzo Church and Alan Turing) proved that in general we cannot calculate whether a given mathematical statement in a formal system is true or false. As I understand, the Church-Turing thesis provides a pretty clear description of the equivalence (isomorphism) between Church's lambda calculus and Turing machines, hence we effectively have a unified model for computability. (Note: As far as I know, Turing's proof makes use of the fact that the halting problem is undecidable. Correct me if I'm wrong.)</p>

<p>Now, Gödel's first incompleteness theorem states that not all statements in a consistent formal system with sufficient arithmetic power may be proven or disproven (decided) within this system. In many ways, this appears to me to be saying exactly the same thing to me as Church's theorems, considering lambda calculus and Turning machines are both effectively formal systems of sorts!</p>

<p>This is however my holistic interpretation, and I was hoping someone could shed some light on the details. Are these two theorems effectively equivalent? Are there any subtleties to be observed? If these theories are essentially looking at the same universal truth in different ways, why were they approached from such different angles? (There were more or less 6 years between Godel's proof and Church's). Finally, can we essential say that the concept of <em>provability</em> in a formal system (proof calculus) is identical to the concept of <em>computability</em> in recursion theory (Turing machines/lambda calculus)?</p>

CC BY-SA 2.5
2010-09-23T19:52:06.167Z
You're not quite right on the Church-Turing Thesis.  The lambda calculus and Turing machine were both formally specified.  The Church-Turing Thesis is that anything that we can reasonably call calculation can be performed on a Turing machine (or in lambda calculus, or anything equivalent).  Since nobody's come up with an exception, it's pretty generally accepted, but it's obviously impossible to prove.
David Thornley
CC BY-SA 2.5
2010-09-24T05:50:21.007Z
Please be careful when you talk about these things. For example, you said "Gödel's first incompleteness theorem states that not all statements in a consistent formal system may be proven within this system". This is rubbish. If a system is consistent then the statement 1 = 0 is not provable. What you have to say is that a formal system (satisfying such and such conditions) does not *decide* all sentences.
Andrej Bauer
CC BY-SA 2.5
2010-09-24T16:49:14.770Z
@David Thornley: Thanks for the correction. So the equivalence between lambda calculus and Turing machines is formally proved (a theorem of Kleene judging by another answer) but the Church-Turing thesis is more like a hypothesis with a lot of supporting evidence, but no actual proof.
Noldorin
CC BY-SA 2.5
2010-09-24T16:50:28.403Z
@Andrej: If I change "proven" to "proven or disproven" and "formal system" to "formal system with sufficient arithmetic capability" then I'm pretty sure it's correct.
Noldorin
CC BY-SA 2.5
2010-09-27T22:01:51.210Z
@Noldorin:  Correct.  The lack of proof is due to the fact that "calculation" is not a mathematically defined term.  Any attempt to give it a formal definition in any sort of reasonable manner has resulted in something equivalent to a Turing machine, so nobody actually doubts it.
David Thornley
CC BY-SA 2.5
2010-09-28T08:04:28.243Z
@Noldorin: Yes, exactly that was my point. You have to change "proven" to "proven or disproven" (which is what "decidable" means). We're not here to write wrong statements that others have to reinterpret until they make sense.
Andrej Bauer
CC BY-SA 2.5
2010-09-28T13:06:55.040Z
@Andrej: Right. Pleae don't imply this is some sort of crime though. Mistakes are inevitable to people trying to learn (or experienced academics even), and it's not their job t owrite everything faultless!
Noldorin
CC BY-SA 2.5
2010-09-28T15:42:30.657Z
Can who-ever down-voted please leave a reason?
Noldorin
CC BY-SA 2.5
2010-09-28T19:19:24.740Z
@Noldrin: I apologize if my comments were too harsh. It's just that when someone asks about a high level ("holistic") understanding of a theorem, I'd expect that the theorems will be stated correctly. Otherwise, it's hard to know whether we should offer opinions about the high-level understanding of the theorems, or should we explain what the theorems actually say?
Andrej Bauer
CC BY-SA 2.5
2010-09-28T19:40:35.743Z
@Andrej: That's fair enough. And I'm happy to take both sorts of responses. Paraphrasing theorems is a difficult task, even if you understand the jist of them. The thing is, I'm the sort of thinker that tends to go for a holistic view first and then fills in the details. Either way, no worries.
Noldorin
<lo.logic><computability><turing-machines>
Church's Theorem and Gödel's Incompleteness Theorems
Noldorin
# Church's Theorem and Gödel's Incompleteness Theorems

(Asked by: username_0 on 2010-09-23)

I have recently been reading up on some of the ideas and history of the ground-breaking work done by various logicians and mathematicians regarding computability. While the individual concepts are fairly clear to me, I'm am trying to get a firm grasp of there inter-relations and the abstract level at which they are all linked.

We know that Church's theorem (or rather, the independent proofs of Hilbert's [Entscheidungsproblem](http://en.wikipedia.org/wiki/Entscheidungsproblem) by Alonzo Church and Alan Turing) proved that in general we cannot calculate whether a given mathematical statement in a formal system is true or false. As I understand, the Church-Turing thesis provides a pretty clear description of the equivalence (isomorphism) between Church's lambda calculus and Turing machines, hence we effectively have a unified model for computability. (Note: As far as I know, Turing's proof makes use of the fact that the halting problem is undecidable. Correct me if I'm wrong.)

Now, Gödel's first incompleteness theorem states that not all statements in a consistent formal system with sufficient arithmetic power may be proven or disproven (decided) within this system. In many ways, this appears to me to be saying exactly the same thing to me as Church's theorems, considering lambda calculus and Turning machines are both effectively formal systems of sorts!

This is however my holistic interpretation, and I was hoping someone could shed some light on the details. Are these two theorems effectively equivalent? Are there any subtleties to be observed? If these theories are essentially looking at the same universal truth in different ways, why were they approached from such different angles? (There were more or less 6 years between Godel's proof and Church's). Finally, can we essential say that the concept of *provability* in a formal system (proof calculus) is identical to the concept of *computability* in recursion theory (Turing machines/lambda calculus)?

**Tags:** lo.logic, computability, turing-machines
> **Comments:**
> **username_1**: You're not quite right on the Church-Turing Thesis.  The lambda calculus and Turing machine were both formally specified.  The Church-Turing Thesis is that anything that we can reasonably call calculation can be performed on a Turing machine (or in lambda calculus, or anything equivalent).  Since nobody's come up with an exception, it's pretty generally accepted, but it's obviously impossible to prove.  
> **username_2**: Please be careful when you talk about these things. For example, you said "Gödel's first incompleteness theorem states that not all statements in a consistent formal system may be proven within this system". This is rubbish. If a system is consistent then the statement 1 = 0 is not provable. What you have to say is that a formal system (satisfying such and such conditions) does not *decide* all sentences.  
> **username_0**: @David Thornley: Thanks for the correction. So the equivalence between lambda calculus and Turing machines is formally proved (a theorem of Kleene judging by another answer) but the Church-Turing thesis is more like a hypothesis with a lot of supporting evidence, but no actual proof.  
> **username_0**: @Andrej: If I change "proven" to "proven or disproven" and "formal system" to "formal system with sufficient arithmetic capability" then I'm pretty sure it's correct.  
> **username_1**: @Noldorin:  Correct.  The lack of proof is due to the fact that "calculation" is not a mathematically defined term.  Any attempt to give it a formal definition in any sort of reasonable manner has resulted in something equivalent to a Turing machine, so nobody actually doubts it.  
> **username_2**: @Noldorin: Yes, exactly that was my point. You have to change "proven" to "proven or disproven" (which is what "decidable" means). We're not here to write wrong statements that others have to reinterpret until they make sense.  
> **username_0**: @Andrej: Right. Pleae don't imply this is some sort of crime though. Mistakes are inevitable to people trying to learn (or experienced academics even), and it's not their job t owrite everything faultless!  
> **username_0**: Can who-ever down-voted please leave a reason?  
> **username_2**: @Noldrin: I apologize if my comments were too harsh. It's just that when someone asks about a high level ("holistic") understanding of a theorem, I'd expect that the theorems will be stated correctly. Otherwise, it's hard to know whether we should offer opinions about the high-level understanding of the theorems, or should we explain what the theorems actually say?  
> **username_0**: @Andrej: That's fair enough. And I'm happy to take both sorts of responses. Paraphrasing theorems is a difficult task, even if you understand the jist of them. The thing is, I'm the sort of thinker that tends to go for a holistic view first and then fills in the details. Either way, no worries.  

---

## 4 answers

### Answer by username_6 on 2010-09-23. Score: 21 | Accepted answer

First, I suggest you read Kleene's "Metamathematics" as a good book on these topics. First two chapters of volume I of Odifreddi's "Classical Recursion Theory" can also be helpful in understanding the relation between these concepts.

> We know that Church's theorem (or rather, the independent proofs of Hilbert's Entscheidungsproblem by Alonzo Church and Alan Turing) proved that in general we cannot calculate whether a given mathematical statement in a formal system is true or false.

I think you are referring to Church's theorem that the set of theorems of first order logic is not decidable. It is important to note that the language is first order.

> As I understand, the Church-Turing thesis provides a pretty clear description of the equivalence (isomorphism) between Church's lambda calculus and Turing machines, hence we effectively have a unified model for computability.

No. The equivalence if lambda-computability and Turing-computability is a *theorem* of Kleene. It is not a thesis. It is considered as evidence supporting Church's thesis.

> Note: As far as I know, Turing's proof makes use of the fact that the halting problem is undecidable. Correct me if I'm wrong.
>
> Now, Gödel's first incompleteness theorem states that not all statements in a consistent formal system may be proven within this system. In many ways, this appears to me to be saying exactly the same thing to me as Church's theorems, considering lambda calculus and Turning machines are both effectively formal systems of sorts!

No. Godel's theorem states that for every $\omega$*-consistent*, *recursively enumerable* theory which *contains enough arithmetic*, there is a sentence $\varphi$ s.t. $\varphi$ and $\lnot \varphi$ are not provable in it.

This does not state the same thing. It does not say anything about set of theorems of the theory being undecidable.

> This is however my holistic interpretation, and I was hoping someone could shed some light on the details. Are these two theorems effectively equivalent? Are there any subtleties to be observed? If these theories are essentially looking at the same universal truth in different ways, why were they approached from such different angles? (There were more or less 6 years between Godel's proof and Church's).

Over the years there has been lots of abuse of Godel's theorems (and similar theorems). One should be very careful in making interpretations of them. As far as I have seen, the abuses are usually result of forgetting to mention some condition in the theorem or combining the theorems by some other beliefs. A careful look shows that theses theorems, although related, are not equivalent.

> Finally, can we essential say that the concept of provability in a formal system (proof calculus) is identical to the concept of computability in recursion theory (Turing machines/lambda calculus)?

I don't understand what you mean by "identical". Certainly there are many relations between computability and provability. I may be able to make a more helpful comment if you clarify what you mean by these being identical.

### update

Lets consider the set of well-formed sentences in the language of arithmetic as $L$. Let $T$ be (the axioms of) a theory satisfying the conditions of first incompleteness theorem. Let $Thm(T)$ be the set of theorems of the theory $T$ and $\lnot Thm(T)$ be the set of sentences whose negation is a theorem of $T$. Let $True$ be the set of sentences that are true in the standard model, and $False$ the set of false sentences. A sentence is in $True$ iff its negation is in $False$. Also every sentence is either true or false, i.e. $L = True \cup False$.

The Godel's incompleteness theorem states that $Thm(T) \cup \lnot Thm(T)$ is a proper subset of $L$. Therefore truth in the standard model and provability in $T$ are different.

Note that $Thm(T)$ is r.e., Church's theorem states that $Thm(T)$ is not decidable.

On the relation between provability in formal system and computability. One is the following: If the system is effective, then the set of derivable expression in it is r.e., and the system is a special case of a grammar. Grammars is another way for defining the concept of computable which is equivalent to Turing machine computability.

> **Comments:**
> **username_0**: Thanks for your answer. I refer to Church's theorem as stated on the Wikipedia page: "In 1936 and 1937 Alonzo Church and Alan Turing respectively[1], published independent papers showing that it is impossible to decide algorithmically whether statements in arithmetic are true or false. This result is now known as Church's Theorem or the Church–Turing Theorem (not to be confused with the Church–Turing thesis).". Cheers for the correction on the Church-Turing thesis too, I shall make note of that. Are you in accordance with David Thornley's comment on my question then?  
> **username_0**: Regarding the description of Godel's first incompleteness theorem, I fully accept your (more precise) definition, though is it not equivalent to my corrected version in the question/the comment on Marc Hamann's answer? Finally, is there any way we can be specific about how exactly these theorems relate to each other, despite not being equivalent?  
> **username_0**: Oh, and regarding my meaning of "identical". Perhaps you could amend the following statement so that it's correct (adding necessary conditions/caveats): Any valid proof in a consistent formal system may be represented by a computable function in a Turing machine?  
> **username_6**: The theory should be r.e. otherwise incompleteness theorem does not hold. (take all true sentences in the standard model, it satisfies all other conditions.) I will add an update to my answer.  
> **username_6**: "Any valid proof in a consistent formal system may be represented by a computable function in a Turing machine?" I don't understand what you mean by "represent". A proof is just a finite string of symbols.  
> **username_0**: I have heard the term "recursively enumerable" applied to sets, but not to theories. What do you mean by a theory being r.e.? Also, by "represent", I mean there exists some isomorphism between A and B.  
> **username_0**: Ah, I suspect when you say a theory is recursively enumerable, you mean the set of all theorems is such(?) I suppose there exist many formal systems that are not r.e. then...  
> **username_6**: Yes, of course there are formal systems which are not effective. And about the isomorphism between proofs and computable functions, see Joshua's answer about proofs (in some formal systems) and programs (not computable functions). And in the Curry-Howard isomorphism what would correspond to a computable function is a formula, not a proof.  
> **username_6**: A possible source of your confusion can be the fact that many words in logic are overloaded, like the word "decide". It is both used for a theory being "complete" as in Godel's theorem and for the set of theorems of a theory being recursive as in Church's theorem. (The word "complete" is also overloaded.) The relation of these topics with philosophy and other sciences has made their misuse common specially in popular science related works. Reading a good *textbook* on these topics (recursion/computability theory, logic, incompleteness theorem, ...) can clarify the picture.  
> **username_0**: @Kaveh: Thanks again for the clarification. I know what you mean about overloaded terms, and indeed about pop sci too. (I garnered a fair amount of my information from *An Emperor's New Mind*. The author is of course highly distinguished, though it's always easy to misinterpret). I have two good answers here, but I'll gladly accept yours for the degree of thoroughness. :)  
> **username_6**: Thank you. :) Roger Penrose is of course highly distinguished, but don't forget that there are also many other highly distinguished experts who disagree with him (, which is completely normal in philosophy). Note: Odifreddi's book also contains a short discussion on these issues.  
> **username_0**: @Kaveh: Oh, sure. I do however believe that what he has to say about the foundations of mathematics and computability theory is fairly uncontroversial. His discussions of the nature of the mind, intelligence, and consciousness are however much more novel/controversial (they disagree at the core with the ideas in the other famous pop sci book on the subject; Godel, Escher and Bach).  

---

### Answer by username_3 on 2010-09-23. Score: 17

> can we essential say that the concept
> of provability in a formal system
> (proof calculus) is identical to the
> concept of computability in recursion
> theory (Turing machines/lambda
> calculus)?

These are very similar but not identical, because some of the steps in the proof calculus may represent non-computable operations.

For example, you could have a proof assistant verify a $ZFC$ proof that the powerset of the naturals $\wp(N)$ exists, and this will be a short proof with two steps (Axiom of Infinity followed by Axiom of Powerset), but neither of these steps are themselves computable.

Similarly, Gödel's Completeness Theorem tells us that any valid formula in first order logic has a proof, but Trakhtenbrot's Theorem tells us that, over finite models, the validity of first order formulae is undecideable.

So finite proofs don't necessarily correspond to computable operations.

> **Comments:**
> **username_0**: Thanks for your answer. So to clarify, how exactly are those steps of your example not computable - in what sense, should I say? To clarify, when I say proofs are computable, I mean that the rules of inference are computable... (Is there any other way of thinking about it?)  
> **username_3**: The set of naturals is recursively enumerable, but an attempt to generate all the naturals would obviously not terminate, so it isn't strictly computable.  The powerset of the naturals isn't even recursively enumerable, and most elements of it aren't recursively enumerable, so it is "even less" computable.  
> **username_3**: Your other question about how to think about this is rather trickier and bigger in scope than I think is suitable here.  Suffice it to say that if you consider non-computable steps with computable inference rules to be computable, then the Halting Problem is computable by simply assuming an Axiom of Halting that posits a halting oracle.   Seems like cheating to me. ;-)  
> **username_0**: @Marc: The book I'm reading at the moment says that the set of all natural numbers *is* computable in that if you input n to the Turing machine, the machine can output the nth natural number. Indeed, the powerset cannot be computed by a Turing machine.  
> **username_0**: Also, I'm not sure I quite follow your reasoning about assuming an Axiom of Halting... Turing machines don't have "axioms" so to speak? I think I still need to be convinced that "all valid proofs in a formal system are computable proofs" is not true. This strikes me as intuitively correct.  
> **username_0**: And it would seem the answer to the halting problem is a direct consequence of Church's theorem, which interestingly uses something very akin to Godel numbering in its proof...  
> **username_3**: @Noldorin: I'm not sure which book you are reading, but what you described is the same thing as recursively enumerable.  
> **username_3**: Turing machines don't have axioms, but proof systems do.  The whole point is that a proof system with non-computable axioms can do things that TMs can't.  
> **username_3**: The halting problem is not soluble by any computational system.  This is a pretty basic fact of the theory of computation, and I would recommend any basic text in that area to clarify this issue for you.  
> **username_0**: @Marc: I think you misunderstand my question. Of course I understand the halting problem, the question goes somewhat deeper...  
> **username_0**: @Marc: It seems I sort of have the answer to that part of the question with the Curry-Howard isomorphism though. :) Thanks for all your help!  
> **username_4**: @Marc: Noldorin's question talks about algorithms producing a proof, not about algorithms which perform steps of a proof. In your example, it is interesting whether an automatic theorem prover could produce the proof of existence of P(N), and whether it can produce a proof in every case. You're basically stating that steps of a proof are not effective, or that classical logic is not constructive - the usual example is that you can prove the existence of something by contradiction, your one is more original.  
> **username_3**: @Blaisorblade: Computation is necessarily constructive, mathematics is not.  Many people get themselves confused when they assume that all that is true in computation and all that is true in classical mathematics are the same (possibly modulo "a few simple rules").  Understanding the distinction between the two is at the heart of my answer to this question; I just gave what I think is the most straightforward way of explaining it.  

---

### Answer by username_5 on 2010-09-26. Score: 10

Although this is not quite what you are asking about, it is in the same vein and hopefully you (and other readers of your question) will find it of interest. You should definitely read up on the [Curry-Howard correspondence](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence), which says that the category of programs is, in a specific sense, isomorphic to the category of *constructive* proofs. (This is discussing proofs and computability at a different level than the other answers.)

> **Comments:**
> **username_0**: Absolutely... I was aware of the Curry-Howard correspondence but didn't want to bring it in to the question and complicate things further. Thanks for pointing it out though. I'm not quite sure if this is the link I'm looking for, or if it's somewhat more restrictive/narrow than I want to saw. What do you think, are there any clarifications to be made here?  

---

### Answer by username_4 on 2011-01-13. Score: 1

I'll try to answer your question from the point of view you take, in short; I'm also trying to relate the two theorems in a different way.

Gödel's first incompleteness theorem states that in a consistent formal system with sufficient arithmetic power, there is a statement P such that no proof either of it or of its negation exists. This does not imply that there is no decision algorithm for the set of theorems of the theory, which would also say that nor P nor not P are theorems. Church-Turing's theorem result says that such an algorithm does not exist. That's the also the core of the answer by Kaveh, I hope to have explained it clearer.

I'll now try to prove that Church-Turing's theorem implies Gödel's theorem, please explain me where and if I'm wrong.
The set of theorems Thm is partially decidable, and suppose R is a program which recognizes it (i.e., halts with "yes" if the input is in Thm, continues running otherwise).
Let's use this to build a new algorithm: Given a statement Q, to see whether it's provable, run R in parallel on Q and not Q, by interleaving their execution, and stopping when the first of them halts, and producing "No" if "not Q" was proved, and "Yes" otherwise; this gives a computable algorithm. Assuming by contradiction that all statements can be proved or disproved, this algorithm would solve the Entscheidungsproblem, but that's absurd! Therefore, there must be a statement which can't be proved or disproved.


---

