The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Dear Coq users,

 

I came across a simple intuitive proof of Gödel's incompleteness theorem using undecidability of the halting problem during the preparation of my automata course for undergraduates.

I think this idea should be known because it is natural and simple.

I wonder how well-known this idea is and would like to know a reference if any.

 

Here is my proof.

================================================

I first slightly modified Gödel's theorem as follows, which I don't
think changes the essence of the theorem.

 

For every “sensible” proof system, there exists a proposition P such
that neither P nor ¬P has a proof.

 

Here by “sensible” we mean that the proof system can express “A
Turing machine M halts” as a proposition. More precisely, in the
proof system we should be able to define a predicate, say halt, that
satisfies the following: (i) if halt(M) has a proof, then the Turing
machin M halts; and (ii) if ¬halt(M) has a proof, then M does not
halt.

 

The idea of the proof is very simple. Assume (HYP) that either P or ¬P
has a proof for every proposition P. Then we can define an algorithm
that solves the halting problem as follows. Since all proofs of the
proof system is countable, we can generate them as pf_1, pf_2, ...
Given an input Turing machine M, one can easily check whehter
pf_i is a proof of halt(M) or a proof of ¬halt(M) for i=1,2,3,... one
by one. Then by (HYP), this process should terminate and find either a
proof of halt(M) or that of ¬halt(M). Since the proof system is
sensible, this algorithm solves the halting problem, which is a
contradiction. Thus, (HYP) is false.

=================================================

Any comments are welcome.

Thanks.

 

Best regards,

Gil