The Coq mailing list

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

Dear Louis,

Thanks for the reference.

Kleene's Mathematical Logic presents essentially exactly the same proof.

I will use this as a reference for the proof.

Best,

Gil

On Sun, Dec 1, 2013 at 7:44 PM, Louis Garde <louis.garde AT free.fr> wrote:

According to Kleene's Mathematical logic (1967, chapter 43, note 178), the first use of an undecidable problem to demonstrate incompleteness is due to Kleene in 1936.

Le 1 déc. 2013 à 07:04, Chung-Kil Hur <gil.hur AT gmail.com> a écrit :

> 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