Church's Theorem and Gödel's Incompleteness Theorems

Question

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

Answer 1

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.

Answer 2

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.

Answer 3

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

Answer 4

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.