6 ms·

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 o

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.

pdonis 8y ago
> 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.
- chongli 8y ago
  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.
  - QuinnWilton 8y ago
    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 http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html
  - deleted 8y ago
    [deleted]
- jcranmer 8y ago
  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).
  - pdonis 8y ago
    > 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"?
    - jcranmer 8y ago
      That is correct. I did say this was on the fly ;-)
IngoBlechschmid 8y ago
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.
- carlehewitt 8y ago
  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.
  - mietek 8y ago
    Could you give a reference for this claim of Wittgenstein’s, please?
    - carlehewitt 8y ago
      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 https://hal.archives-ouvertes.fr/hal-01566393
  - 8y ago
amluto 8y ago
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.
bitL 8y ago
cough Hypercomputation cough
- IngoBlechschmid 8y ago
  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/superturingmaschinen/slides-warwick2017.pdf https://rawgit.com/iblech/mathezirkel-kurs/master/superturin...
xyzzyz 8y ago
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.

pdonis 8y ago

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

chongli 8y ago
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.
- QuinnWilton 8y ago
  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 http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html
- deleted 8y ago
  [deleted]
jcranmer 8y ago
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).
- pdonis 8y ago
  > 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"?
  - jcranmer 8y ago
    That is correct. I did say this was on the fly ;-)

IngoBlechschmid 8y ago

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.

carlehewitt 8y ago
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.
- mietek 8y ago
  Could you give a reference for this claim of Wittgenstein’s, please?
  - carlehewitt 8y ago
    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 https://hal.archives-ouvertes.fr/hal-01566393
- 8y ago

amluto 8y ago

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.

bitL 8y ago

cough Hypercomputation cough

IngoBlechschmid 8y ago
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/superturingmaschinen/slides-warwick2017.pdf https://rawgit.com/iblech/mathezirkel-kurs/master/superturin...

xyzzyz 8y ago

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.