Timeline for Computability viewpoint of Gödel/Rosser's incompleteness theorem
Current License: CC BY-SA 4.0
26 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| 2 days ago | comment | added | user21820 | @Nithuya: You might be interested in this post. | |
| 2 days ago | comment | added | Nithuya | Thank you very much. I also wonder what's the link with second incompletenes theorem and Hilbert-Bernays-Löb conditions. I'm a bit tired now though I might come back later to study this in more depth. | |
| 2 days ago | comment | added | user21820 | @Nithuya: I also added an extra bit after that for not necessarily classical T. =) | |
| 2 days ago | history | edited | user21820 | CC BY-SA 4.0 | added 818 characters in body |
| 2 days ago | comment | added | user21820 | @Nithuya: I'm not using contrapositive, but you did identify a mistake. Indeed, knowing that H(C,C) halts doesn't tell us whether it outputs "true" or "false", so we cannot conclude that C(C) does not halt. You're also correct that it works for ( T is inconsistent and classical ⇒ D(D) halts ). I must have proven for W' and accidentally thought it applied to Q' too. | |
| Nov 25 at 2:43 | comment | added | Nithuya | Your argument does work for "T inconsistent" => "D(D) halts" though. | |
| Nov 25 at 1:31 | comment | added | Nithuya | I don't get why "Q' true" implies "T consistent". You seem to suppose T inconsistent so I guess you're doing a reasoning by contraposition, aiming to prove "Q' false" i.e "Q true". But "Q true" means "C(C) halts", yet your conclusion is "C(C) does not halt". Am I missing something? Also if T is inconsistent, we know H(C,C) halts but we don't know whether its true or false, it depends on if H finds first a proof s1 of Q or a proof s2 of Q'. Since C(C) halts iff H(C,C) halts on "false", I don't get how you make a proof out of this. | |
| Nov 12, 2023 at 17:25 | comment | added | Hypnosifl | Thanks! I will pick up Rautenberg's book and see if I can follow the explanation of the beta-function. | |
| Nov 12, 2023 at 8:54 | comment | added | user21820 | Although Rautenberg does not explicitly mention programs, it is obvious once you understand the content. In particular, he writes "Moreover, Δ1 contains precisely the recursive predicates, from which it easily follows that Σ1 consists just of all r.e. predicates", which implies what I claimed. Note that if you follow my instructions in my above comment, you would get a Σ1-sentence, so if you really want to you can get exactly the same strong claim without the need for any convoluted path (i.e. Rautenberg's). | |
| Nov 12, 2023 at 8:44 | comment | added | user21820 | @Hypnosifl: Yes. I stated clearly in my post that "program" means "program in L" and includes all possible programs. PA⁻ can reason about programs exactly as I claimed. Not only that, this is a standard result that is proven rigorously in any good introductory logic textbook, like Rautenberg's, which even proves it for Robinson's Q (which is far weaker than PA⁻). You can do it yourself simply by understanding the beta-function and associated proofs, and then actually using the recipe given in my post under "Encoding program execution in a string". | |
| Nov 11, 2023 at 20:47 | comment | added | Hypnosifl | Do you mean that for any Turing machine T acting on an input tape whose initial state has some finite symbol string N, we can use Godel's beta-function + proofs to show there is a formula of first-order arithmetic that is provable from PA- iff T(N) halts? Or will this only work for some specific class of possible T(N), like primitive recursive functions? | |
| Nov 11, 2023 at 15:59 | comment | added | user21820 | @Hypnosifl: No. It's relatively easy to prove that PA⁻ can reason about programs, without invoking the MRDP theorem. You need only Godel's beta-function and associated proofs. | |
| Nov 10, 2023 at 18:54 | comment | added | Hypnosifl | When you say it's a requirement of the proof that the formal system T can "reason about programs", does that mean that in order to apply this to axioms of Peano arithmetic (including PA-), we need to supplement proof with the MRDP theorem, which from description at quora.com/… implies that for any Turing machine acting on a given input, the question of whether it halts is equivalent to a question about whether a specific Diophantine equation has any solutions? | |
| Jan 30, 2021 at 17:03 | comment | added | user21820 | For future reference, this discussion was continued here. | |
| Jan 30, 2021 at 14:09 | comment | added | user21820 | [cont] For the second-order induction axiom to ever have any 'force' in a foundational system, the system needs to have set-construction axioms as well. For example ACA0 has a single second-order set induction axiom, and also has arithmetical comprehension axioms to construct sets, but look, ACA0 is in fact conservative over PA! So the set induction axiom actually failed to improve what arithmetical sentences can be proven! What is happening? I suggest you think very carefully about the foundational issues here. As mentioned in a previous comment, we can discuss more in the Logic chat-room. =) | |
| Jan 30, 2021 at 14:03 | comment | added | user21820 | @Lostdefinition: Smullyan does not disagree with what I wrote. His comments are misleading to beginners. PA has induction and is incomplete. PA− has no induction and is also incomplete. Talking about going beyond first-order induction is in fact not meaningful because there is simply no such thing in reality. Think about it, there is no formal system for second-order PA with full second-order semantics, so it's simply meaningless to ascribe 'force' to the second-order induction axiom in any foundational sense (which is what the incompleteness theorems are really about). [cont] | |
| Jan 30, 2021 at 13:13 | comment | added | Lost definition | In misconceptions: "It is not due to induction". Smullyan disagrees (see Gödel Incompleteness Theorems, p. 112), he says incompleteness is due to lack of induction. It's because first-order "induction doesn't express the full force of mathematical induction". | |
| Mar 21, 2019 at 10:29 | comment | added | Giorgio Mossa | @user21820 Thank you so much. That is the a truly enlightening answer. | |
| Jan 30, 2018 at 8:45 | comment | added | user21820 | @Taroccoesbrocco: Thank you! You are also welcome to the Logic chat-room for any logic-related discussion. =) | |
| Jan 29, 2018 at 18:45 | comment | added | Taroccoesbrocco | Monumental! A good example of self-answering. | |
| Dec 31, 2017 at 7:53 | history | edited | user21820 | CC BY-SA 3.0 | added 753 characters in body |
| Dec 19, 2017 at 15:28 | vote | accept | user21820 | ||
| Nov 2, 2017 at 14:06 | history | edited | user21820 | CC BY-SA 3.0 | Added Philip White's reference. |
| Nov 2, 2017 at 12:45 | history | edited | user21820 | CC BY-SA 3.0 | Added a link to an archive of the reference cited by Scott's blog post. |
| Oct 24, 2017 at 6:03 | history | edited | user21820 | CC BY-SA 3.0 | added 679 characters in body |
| Oct 23, 2017 at 18:18 | history | answered | user21820 | CC BY-SA 3.0 |