Hacker News Reader

Comment by repsilat | Hacker News Reader

It's super easy to prove if you assume the Halting Problem is undecidable. Basically,

1. Assume every either T or ~T is provable for all theorems T, and that our logic is consistent. (The opposite of the incompleteness theorem.)

2. For every Turing machine, there is a proof that it halts or a proof that it doesn't halt.

3. A machine that enumerates and validates proofs will find one of those proofs, so the Halting Problem is decidable -- a contradiction.

Easy peasy. (The proof of the Halting Problem undecidability from the Incompleteness Theorem is similarly straightforward.)

Godel did his work first though, so he didn't have that machinery (hmm) available.

View on HN

This proof using Turing machines is indeed very slick! Its elegance is balanced by its nonconstructiveness: Gödel's proof yields an explicit example for an unprovable statement (namely a formal rendering of "this statement is not provable"), while the Turing machine proof doesn't.

Also let me add a remark on a certain subtlety: Step 3 only works if we assume that, if a claim about the halting behaviour of Turing machines has a proof in the studied formal system, then it's actually true.

This assumption is believed to be warranted for the standard formal systems of mathematics such as Peano Arithmetic (PA) or Zermelo–Fraenkel set theory (ZF), but Gödel's proof also applies to formal systems for which this assumption doesn't hold, or for which the assumption does hold but cannot be proven in a weak metatheory.

These systems are typically not very useful as vehicles to carry out formalized mathematics, but they are nevertheless very interesting and fundamental to the study of logic. An example for such an anti-real formal system is PA adjoined by an axiom expressing that PA is inconsistent.

As Wittgenstein correctly pointed out, Gödel's proposition "I'm unprovable" is not a proposition in Russell's system because it leads to inconsistency. Consequently, Gödel's incompleteness results are not valid for Russell's system. The proposition "I'm unprovable" cannot be constructed as a fixed point of P |-> ~|-P because ~|-P has order one greater than the order of P.

Could you give a reference for this claim of Wittgenstein’s, please?

A reference is:

Ludwig Wittgenstein. 1956. Remarks on the Foundations of Mathematics, Revised Edition Basil Blackwell. 1978.

There is a discussion here:

https://hal.archives-ouvertes.fr/hal-01566393

That seems entirely circular.

Gödel's proposition "I'mUnprovable" cannot be constructed as a fixed point of P |-> ~|-P because ~|-P has order one greater than the order of P.

The Turing machine proof does yield an explicit unprovable statement when you combine it with the (constructive) proof of the undecidability of the Halting problem. Let H be the Turing machine that, when given a Turing machine M, searches for a proof (in the formal system under consideration) that M halts or a proof that M doesn’t halt. Build the machine Q that quines itself to apply H to the code of Q itself, then either loops forever or halts according to the opposite of what H purportedly proved. Then the true statement “Q doesn’t halt” is unprovable in the formal system.

It’s more work to formalize all the details here than in Gödel’s proof, because now you have to explain how the formal system can reason about Turing machines reasoning about Turing machines rather than just how the formal system can reason about itself, but it works just as well.

Wow! Didn't notice that. I stand corrected. Your rendition of the proof even dispenses of the assumption that the formal system correctly judges the halting behaviour of Turing machines.

Thank you for this. Else I'd have perpetuated that myth further!

If you actually want to make the proof above as rigorous as Goedel’s original proof, you’ll find that it will be exactly as technical as the original. The technical difficulty in the proof above is hidden in the step 2 — what you need to show is that every statement of a form “the Turing machine T = {..., ..., ...} halts on input ...” is expressible in the language of first order arithmetic. To do that, you need to do exactly the same work as Goedel did, with all the finite string encoding etc.

> It's super easy to prove if you assume the Halting Problem is undecidable.

Well, sure, because proving the Halting Problem is undecidable is about as hard as proving Godel's Theorem without having the undecidability of the Halting Problem to start from.

It isn't, actually. The proof of the undecidability of the halting problem is rather straightforward. You just assume you have a program that determines whether or not its input halts or loops. Then you write a program that uses your assumption as a helper and does the opposite:

If the input halts, then loop

If the input loops, then halt

You then pass the program itself as input to itself and you get a contradiction.

Here's my favourite version of this proof, in the style of a poem by Dr. Seuss: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html

The proof of the Halting Problem's undecidability is a lot less technically challenging. Here it is, off the top of my head:

Assume you have a program HALT(n) that will return 1 if the Turing machine described by string n halts when fed itself as input and returns 0 otherwise. Construct the program BOOM(n) that runs forever if HALT(n) returns 1 and returns 0 if HALT(n) returns 1. Now consider HALT(BOOM). If HALT(BOOM) is 1, then BOOM(BOOM) halts by definition of HALT, but BOOM runs forever in that case. If it returned 0, then it runs forever, but BOOM(BOOM) in fact halted. Something must give, and the only thing that has room to give is that HALT itself can be constructed (since the encoding of Turing machines to numbers is well-defined, and the construction of BOOM is well-defined and possible iff HALT is well-defined and possible).

> Construct the program BOOM(n) that runs forever if HALT(n) returns 1 and returns 0 if HALT(n) returns 1.

I assume you mean "returns 0 if HALT(n) returns 0"?

That is correct. I did say this was on the fly ;-)

I’m personally a fan of using Chaitin’s constant (Ω). It’s easy to show that, for some finite n, the nth digit of n is uncomputable. It follows that statements of the form “the nth binary digit of Ω 0” can neither be proven nor disproven.

cough Hypercomputation cough

Hypercomputation is a fascinating concept; I particularly like infinite-time Turing machines, which can continue computing "at the end of time" (day ω), at the day after that (ω + 1), the day after that (ω + 2), at the second end of time (day ω ⋅ 2), the day after that (day ω ⋅ 2 + 1), and so on.

Infinite-time Turing machines can readily solve the halting problem for ordinary Turing machines, but (by the same proof) not for themselves.

The theory of infinite-time Turing machines is in some regards parallel to the theory of ordinary Turing machines and in others quite different.

I particularly enjoy the Lost Melody Theorem: There is a specific infinitely long 0/1 sequence for which

(a) it's possible to devise an infinite-time Turing machine which will correctly detect whether that 0/1 sequence is written on the input tape, but

(b) there is no infinite-time Turing machine which will, starting on an empty tape, write out that 0/1 sequence to the output tape.

It's like when you would recognize a song but cannot sing it. Some details are here: https://rawgit.com/iblech/mathezirkel-kurs/master/superturin...

Reply on news.ycombinator.com