28
$\begingroup$

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 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)?

Improve this question
$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – David Thornley Sep 23 '10 at 19:52
  • 2
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 24 '10 at 5:50
  • $\begingroup$ @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. $\endgroup$ – Noldorin Sep 24 '10 at 16:49
  • $\begingroup$ @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. $\endgroup$ – Noldorin Sep 24 '10 at 16:50
  • 2
    $\begingroup$ @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! $\endgroup$ – Noldorin Sep 28 '10 at 13:06
20
$\begingroup$

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.

Improve this answer
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Noldorin Sep 24 '10 at 16:57
  • $\begingroup$ 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? $\endgroup$ – Noldorin Sep 24 '10 at 17:03
  • $\begingroup$ 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? $\endgroup$ – Noldorin Sep 24 '10 at 17:13
  • $\begingroup$ 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. $\endgroup$ – Kaveh Sep 24 '10 at 17:47
  • $\begingroup$ "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. $\endgroup$ – Kaveh Sep 24 '10 at 18:02
17
$\begingroup$

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.

Improve this answer
$\endgroup$
  • $\begingroup$ 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?) $\endgroup$ – Noldorin Sep 24 '10 at 16:54
  • 1
    $\begingroup$ 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. $\endgroup$ – Marc Hamann Sep 24 '10 at 17:28
  • $\begingroup$ 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. ;-) $\endgroup$ – Marc Hamann Sep 24 '10 at 17:34
  • $\begingroup$ @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. $\endgroup$ – Noldorin Sep 24 '10 at 21:09
  • $\begingroup$ 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. $\endgroup$ – Noldorin Sep 24 '10 at 21:16
10
$\begingroup$

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

Improve this answer
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Noldorin Sep 26 '10 at 13:16
1
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.