4 ms·
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 unpr
by 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 agoAs 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 agoCould you give a reference for this claim of Wittgenstein’s, please?
- carlehewitt 8y agoA 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
- vyodaiken 8y agoThat seems entirely circular.
- carlehewitt 8y agoGö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.
- anderskaseorg 8y agoThe 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.
- IngoBlechschmid 8y agoWow! 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!