Mixing
Why does the unsolvability of the Halting Problem give a negative solution to the decision problem?
$begingroup$
So Hilbert famously asked for a formalization of all of mathematics which was computationally decidable. Gödel is credited with shattering the idea that "all of mathematics" can be formalized. After all, one can't even formalize all of elementary arithmetic. But the decision problem (Entscheidungsproblem) was still considered open until Church/Turing.
I've read a fair number of popular accounts of this period. They always end with "finally the unsolvability of the Halting Problem completely shattered Hilbert's dream" and no further explanation. I feel like there are a few steps missing here. Why exactly does the unsolvability of the Halting Problem go against the decision problem?
Presumably the argument is: a formalization of all of mathematics has to be able to formalize Turing machines. Hence, it contains sentences of the form "Turing machine T halts". A decision procedure for such a formal system would therefore solve the Halting Problem. And that can't be done.
But Turing machines were a very new invention at the time. Why didn't people try to rescue the decision problem by saying Turing machines weren't an objective for formalization? And why does nobody seem to feel obligated to show that the decision problem can't be solved regardless?
decidability
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
$endgroup$
add a comment |
$begingroup$
So Hilbert famously asked for a formalization of all of mathematics which was computationally decidable. Gödel is credited with shattering the idea that "all of mathematics" can be formalized. After all, one can't even formalize all of elementary arithmetic. But the decision problem (Entscheidungsproblem) was still considered open until Church/Turing.
I've read a fair number of popular accounts of this period. They always end with "finally the unsolvability of the Halting Problem completely shattered Hilbert's dream" and no further explanation. I feel like there are a few steps missing here. Why exactly does the unsolvability of the Halting Problem go against the decision problem?
Presumably the argument is: a formalization of all of mathematics has to be able to formalize Turing machines. Hence, it contains sentences of the form "Turing machine T halts". A decision procedure for such a formal system would therefore solve the Halting Problem. And that can't be done.
But Turing machines were a very new invention at the time. Why didn't people try to rescue the decision problem by saying Turing machines weren't an objective for formalization? And why does nobody seem to feel obligated to show that the decision problem can't be solved regardless?
decidability
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
$endgroup$
$begingroup$
@reuns Not in full detail. But I gather that it can be done using Gödel's ideas. That's not a trivial line of argument though. So the question "why does nobody ever spell out these final steps?" still stands.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:39
$begingroup$
Given a program $P$ written in java language, is it clear to you how to formalize "the program $P$ halts" into an arithmetic statement ? To forbid those kind of statement you can disallow infinite quantification, that is only $forall n le N$ is allowed, with $N$ fixed once for all. Your theory is then decidable, but it can't formalize arithmetic. To me the most down-to-earth approach is formalizing mathematical theories in the Turing/program/computability framework, so "$exists n, f(n)$" becomes "does exists_n(f) halt".
$endgroup$
– reuns
Jan 27 at 18:41
add a comment |
$begingroup$
So Hilbert famously asked for a formalization of all of mathematics which was computationally decidable. Gödel is credited with shattering the idea that "all of mathematics" can be formalized. After all, one can't even formalize all of elementary arithmetic. But the decision problem (Entscheidungsproblem) was still considered open until Church/Turing.
I've read a fair number of popular accounts of this period. They always end with "finally the unsolvability of the Halting Problem completely shattered Hilbert's dream" and no further explanation. I feel like there are a few steps missing here. Why exactly does the unsolvability of the Halting Problem go against the decision problem?
Presumably the argument is: a formalization of all of mathematics has to be able to formalize Turing machines. Hence, it contains sentences of the form "Turing machine T halts". A decision procedure for such a formal system would therefore solve the Halting Problem. And that can't be done.
But Turing machines were a very new invention at the time. Why didn't people try to rescue the decision problem by saying Turing machines weren't an objective for formalization? And why does nobody seem to feel obligated to show that the decision problem can't be solved regardless?
decidability
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
$endgroup$
So Hilbert famously asked for a formalization of all of mathematics which was computationally decidable. Gödel is credited with shattering the idea that "all of mathematics" can be formalized. After all, one can't even formalize all of elementary arithmetic. But the decision problem (Entscheidungsproblem) was still considered open until Church/Turing.
I've read a fair number of popular accounts of this period. They always end with "finally the unsolvability of the Halting Problem completely shattered Hilbert's dream" and no further explanation. I feel like there are a few steps missing here. Why exactly does the unsolvability of the Halting Problem go against the decision problem?
Presumably the argument is: a formalization of all of mathematics has to be able to formalize Turing machines. Hence, it contains sentences of the form "Turing machine T halts". A decision procedure for such a formal system would therefore solve the Halting Problem. And that can't be done.
But Turing machines were a very new invention at the time. Why didn't people try to rescue the decision problem by saying Turing machines weren't an objective for formalization? And why does nobody seem to feel obligated to show that the decision problem can't be solved regardless?
decidability
decidability
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
asked Jan 27 at 18:00
Sebastian OberhoffSebastian Oberhoff
582311
582311
$begingroup$
@reuns Not in full detail. But I gather that it can be done using Gödel's ideas. That's not a trivial line of argument though. So the question "why does nobody ever spell out these final steps?" still stands.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:39
$begingroup$
Given a program $P$ written in java language, is it clear to you how to formalize "the program $P$ halts" into an arithmetic statement ? To forbid those kind of statement you can disallow infinite quantification, that is only $forall n le N$ is allowed, with $N$ fixed once for all. Your theory is then decidable, but it can't formalize arithmetic. To me the most down-to-earth approach is formalizing mathematical theories in the Turing/program/computability framework, so "$exists n, f(n)$" becomes "does exists_n(f) halt".
$endgroup$
– reuns
Jan 27 at 18:41
add a comment |
$begingroup$
@reuns Not in full detail. But I gather that it can be done using Gödel's ideas. That's not a trivial line of argument though. So the question "why does nobody ever spell out these final steps?" still stands.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:39
$begingroup$
Given a program $P$ written in java language, is it clear to you how to formalize "the program $P$ halts" into an arithmetic statement ? To forbid those kind of statement you can disallow infinite quantification, that is only $forall n le N$ is allowed, with $N$ fixed once for all. Your theory is then decidable, but it can't formalize arithmetic. To me the most down-to-earth approach is formalizing mathematical theories in the Turing/program/computability framework, so "$exists n, f(n)$" becomes "does exists_n(f) halt".
$endgroup$
– reuns
Jan 27 at 18:41
$begingroup$
@reuns Not in full detail. But I gather that it can be done using Gödel's ideas. That's not a trivial line of argument though. So the question "why does nobody ever spell out these final steps?" still stands.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:39
$begingroup$
@reuns Not in full detail. But I gather that it can be done using Gödel's ideas. That's not a trivial line of argument though. So the question "why does nobody ever spell out these final steps?" still stands.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:39
$begingroup$
Given a program $P$ written in java language, is it clear to you how to formalize "the program $P$ halts" into an arithmetic statement ? To forbid those kind of statement you can disallow infinite quantification, that is only $forall n le N$ is allowed, with $N$ fixed once for all. Your theory is then decidable, but it can't formalize arithmetic. To me the most down-to-earth approach is formalizing mathematical theories in the Turing/program/computability framework, so "$exists n, f(n)$" becomes "does exists_n(f) halt".
$endgroup$
– reuns
Jan 27 at 18:41
$begingroup$
Given a program $P$ written in java language, is it clear to you how to formalize "the program $P$ halts" into an arithmetic statement ? To forbid those kind of statement you can disallow infinite quantification, that is only $forall n le N$ is allowed, with $N$ fixed once for all. Your theory is then decidable, but it can't formalize arithmetic. To me the most down-to-earth approach is formalizing mathematical theories in the Turing/program/computability framework, so "$exists n, f(n)$" becomes "does exists_n(f) halt".
$endgroup$
– reuns
Jan 27 at 18:41
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
Even assuming we're okay drastically restricting the scope of mathematics to be decided - which flies in the face of the whole idea of the program - there's still a fundamnetal issue: the arithmetizability of computation. Basically, in order to rescue decidability you'd have to restrict all the way down to triviality.
This is a riff on Godel's incompleteness theorem. Just as with GIT we used arithmetic to talk about proofs, we can talk about Turing machines in the language of arithmetic. (I don't know when this was first explicitly stated, but it's pretty much immediate once Godel's ideas are understood - certainly Kleene's $T$-predicate, which appeared only seven years after Turing's paper, does the job.) The point is that from a computable solution to the Entscheidungsproblem we can construct a computable consistent completion of PA (just go through sentences one by one with a consistency-preserving greedy algorithm), but by the arithmetization of computation (plus Rosser's improvement of GIT as originally stated) Godel's incompleteness theorem applies to any computably axiomatizable consistent extension of PA.
Indeed, looking a bit closer we get that even the $Sigma_1$ fragment of the consequences of PA is not computable. Since the $Delta_0$ fragment (= bounded quantifiers only) is trivially computable, this says that incompleteness hits arithmetic as hard as it possibly could. And at this point there's really nothing left to do.
Combining all this with the fact that restricting the scope goes against the whole spirit of the program to begin with, I think that explains why the conclusion was (and is) pretty universal. Note that the study of decidable fragments of arithmetic is definitely alive and well, it's just recognized as a fundamentally different thing than Hilbert's program.
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
$endgroup$
$begingroup$
This argument still assumes that the formal system under consideration is sound, right? If one merely assumes consistency, then a decision procedure may decide that "Turing machine $T$ halts" is provable even though it doesn't halt ($omega$-inconsistency).
$endgroup$
– Sebastian Oberhoff
Jan 28 at 15:51
add a comment |
$begingroup$
There were several proofs of undecidability and incompleteness using very different tools, from Church, Post, Godel and Turing. They are all equivalent.
Godel's proof is the probably the most direct, because it used nothing more abstract than ordinary arithmetic.
Turing's may be the most consequential, because it has been used to provide a definition of "computability", which is an incredibly rich subject on its own.
Both Godel and Turing's proof depended on the idea of self-reference, where a system as a whole is represented as an object of the system. With Turing, we are talking about what happens when a program takes a program as input. With Godel, we are looking at what happens when we encode a theorem of arithmetic as an integer. You can see the parallel here and have a sense of how they are equivalent.
With Godel's proof, there is no escaping the fact that arithmetic must be either undecidable or incomplete.
If you are new to the subject, I recommend Douglas Hofstadter's classic Godel, Escher, Bach, an entertaining book that can give you tools to visualize how these proofs work.
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
$endgroup$
$begingroup$
I'm an amateur veteran at these topics. I've read GEB several times. I don't see how your comment addresses the question.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:23
$begingroup$
The point is that Turing's proof is just one of many. If Turing hadn't participated in the project, the other proofs would have been sufficient. You don't need Turing machines to prove undecidability, so throwing them out has no effect on Hilbert's program.
$endgroup$
– Charles Gillingham
Feb 8 at 4:55
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3089898%2fwhy-does-the-unsolvability-of-the-halting-problem-give-a-negative-solution-to-th%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Even assuming we're okay drastically restricting the scope of mathematics to be decided - which flies in the face of the whole idea of the program - there's still a fundamnetal issue: the arithmetizability of computation. Basically, in order to rescue decidability you'd have to restrict all the way down to triviality.
This is a riff on Godel's incompleteness theorem. Just as with GIT we used arithmetic to talk about proofs, we can talk about Turing machines in the language of arithmetic. (I don't know when this was first explicitly stated, but it's pretty much immediate once Godel's ideas are understood - certainly Kleene's $T$-predicate, which appeared only seven years after Turing's paper, does the job.) The point is that from a computable solution to the Entscheidungsproblem we can construct a computable consistent completion of PA (just go through sentences one by one with a consistency-preserving greedy algorithm), but by the arithmetization of computation (plus Rosser's improvement of GIT as originally stated) Godel's incompleteness theorem applies to any computably axiomatizable consistent extension of PA.
Indeed, looking a bit closer we get that even the $Sigma_1$ fragment of the consequences of PA is not computable. Since the $Delta_0$ fragment (= bounded quantifiers only) is trivially computable, this says that incompleteness hits arithmetic as hard as it possibly could. And at this point there's really nothing left to do.
Combining all this with the fact that restricting the scope goes against the whole spirit of the program to begin with, I think that explains why the conclusion was (and is) pretty universal. Note that the study of decidable fragments of arithmetic is definitely alive and well, it's just recognized as a fundamentally different thing than Hilbert's program.
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
$endgroup$
$begingroup$
This argument still assumes that the formal system under consideration is sound, right? If one merely assumes consistency, then a decision procedure may decide that "Turing machine $T$ halts" is provable even though it doesn't halt ($omega$-inconsistency).
$endgroup$
– Sebastian Oberhoff
Jan 28 at 15:51
add a comment |
$begingroup$
Even assuming we're okay drastically restricting the scope of mathematics to be decided - which flies in the face of the whole idea of the program - there's still a fundamnetal issue: the arithmetizability of computation. Basically, in order to rescue decidability you'd have to restrict all the way down to triviality.
This is a riff on Godel's incompleteness theorem. Just as with GIT we used arithmetic to talk about proofs, we can talk about Turing machines in the language of arithmetic. (I don't know when this was first explicitly stated, but it's pretty much immediate once Godel's ideas are understood - certainly Kleene's $T$-predicate, which appeared only seven years after Turing's paper, does the job.) The point is that from a computable solution to the Entscheidungsproblem we can construct a computable consistent completion of PA (just go through sentences one by one with a consistency-preserving greedy algorithm), but by the arithmetization of computation (plus Rosser's improvement of GIT as originally stated) Godel's incompleteness theorem applies to any computably axiomatizable consistent extension of PA.
Indeed, looking a bit closer we get that even the $Sigma_1$ fragment of the consequences of PA is not computable. Since the $Delta_0$ fragment (= bounded quantifiers only) is trivially computable, this says that incompleteness hits arithmetic as hard as it possibly could. And at this point there's really nothing left to do.
Combining all this with the fact that restricting the scope goes against the whole spirit of the program to begin with, I think that explains why the conclusion was (and is) pretty universal. Note that the study of decidable fragments of arithmetic is definitely alive and well, it's just recognized as a fundamentally different thing than Hilbert's program.
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
$endgroup$
$begingroup$
This argument still assumes that the formal system under consideration is sound, right? If one merely assumes consistency, then a decision procedure may decide that "Turing machine $T$ halts" is provable even though it doesn't halt ($omega$-inconsistency).
$endgroup$
– Sebastian Oberhoff
Jan 28 at 15:51
add a comment |
$begingroup$
Even assuming we're okay drastically restricting the scope of mathematics to be decided - which flies in the face of the whole idea of the program - there's still a fundamnetal issue: the arithmetizability of computation. Basically, in order to rescue decidability you'd have to restrict all the way down to triviality.
This is a riff on Godel's incompleteness theorem. Just as with GIT we used arithmetic to talk about proofs, we can talk about Turing machines in the language of arithmetic. (I don't know when this was first explicitly stated, but it's pretty much immediate once Godel's ideas are understood - certainly Kleene's $T$-predicate, which appeared only seven years after Turing's paper, does the job.) The point is that from a computable solution to the Entscheidungsproblem we can construct a computable consistent completion of PA (just go through sentences one by one with a consistency-preserving greedy algorithm), but by the arithmetization of computation (plus Rosser's improvement of GIT as originally stated) Godel's incompleteness theorem applies to any computably axiomatizable consistent extension of PA.
Indeed, looking a bit closer we get that even the $Sigma_1$ fragment of the consequences of PA is not computable. Since the $Delta_0$ fragment (= bounded quantifiers only) is trivially computable, this says that incompleteness hits arithmetic as hard as it possibly could. And at this point there's really nothing left to do.
Combining all this with the fact that restricting the scope goes against the whole spirit of the program to begin with, I think that explains why the conclusion was (and is) pretty universal. Note that the study of decidable fragments of arithmetic is definitely alive and well, it's just recognized as a fundamentally different thing than Hilbert's program.
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
$endgroup$
Even assuming we're okay drastically restricting the scope of mathematics to be decided - which flies in the face of the whole idea of the program - there's still a fundamnetal issue: the arithmetizability of computation. Basically, in order to rescue decidability you'd have to restrict all the way down to triviality.
This is a riff on Godel's incompleteness theorem. Just as with GIT we used arithmetic to talk about proofs, we can talk about Turing machines in the language of arithmetic. (I don't know when this was first explicitly stated, but it's pretty much immediate once Godel's ideas are understood - certainly Kleene's $T$-predicate, which appeared only seven years after Turing's paper, does the job.) The point is that from a computable solution to the Entscheidungsproblem we can construct a computable consistent completion of PA (just go through sentences one by one with a consistency-preserving greedy algorithm), but by the arithmetization of computation (plus Rosser's improvement of GIT as originally stated) Godel's incompleteness theorem applies to any computably axiomatizable consistent extension of PA.
Indeed, looking a bit closer we get that even the $Sigma_1$ fragment of the consequences of PA is not computable. Since the $Delta_0$ fragment (= bounded quantifiers only) is trivially computable, this says that incompleteness hits arithmetic as hard as it possibly could. And at this point there's really nothing left to do.
Combining all this with the fact that restricting the scope goes against the whole spirit of the program to begin with, I think that explains why the conclusion was (and is) pretty universal. Note that the study of decidable fragments of arithmetic is definitely alive and well, it's just recognized as a fundamentally different thing than Hilbert's program.
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
answered Jan 27 at 19:22
Noah SchweberNoah Schweber
127k10151293
127k10151293
$begingroup$
This argument still assumes that the formal system under consideration is sound, right? If one merely assumes consistency, then a decision procedure may decide that "Turing machine $T$ halts" is provable even though it doesn't halt ($omega$-inconsistency).
$endgroup$
– Sebastian Oberhoff
Jan 28 at 15:51
add a comment |
$begingroup$
This argument still assumes that the formal system under consideration is sound, right? If one merely assumes consistency, then a decision procedure may decide that "Turing machine $T$ halts" is provable even though it doesn't halt ($omega$-inconsistency).
$endgroup$
– Sebastian Oberhoff
Jan 28 at 15:51
$begingroup$
This argument still assumes that the formal system under consideration is sound, right? If one merely assumes consistency, then a decision procedure may decide that "Turing machine $T$ halts" is provable even though it doesn't halt ($omega$-inconsistency).
$endgroup$
– Sebastian Oberhoff
Jan 28 at 15:51
$begingroup$
This argument still assumes that the formal system under consideration is sound, right? If one merely assumes consistency, then a decision procedure may decide that "Turing machine $T$ halts" is provable even though it doesn't halt ($omega$-inconsistency).
$endgroup$
– Sebastian Oberhoff
Jan 28 at 15:51
add a comment |
$begingroup$
There were several proofs of undecidability and incompleteness using very different tools, from Church, Post, Godel and Turing. They are all equivalent.
Godel's proof is the probably the most direct, because it used nothing more abstract than ordinary arithmetic.
Turing's may be the most consequential, because it has been used to provide a definition of "computability", which is an incredibly rich subject on its own.
Both Godel and Turing's proof depended on the idea of self-reference, where a system as a whole is represented as an object of the system. With Turing, we are talking about what happens when a program takes a program as input. With Godel, we are looking at what happens when we encode a theorem of arithmetic as an integer. You can see the parallel here and have a sense of how they are equivalent.
With Godel's proof, there is no escaping the fact that arithmetic must be either undecidable or incomplete.
If you are new to the subject, I recommend Douglas Hofstadter's classic Godel, Escher, Bach, an entertaining book that can give you tools to visualize how these proofs work.
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
$endgroup$
$begingroup$
I'm an amateur veteran at these topics. I've read GEB several times. I don't see how your comment addresses the question.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:23
$begingroup$
The point is that Turing's proof is just one of many. If Turing hadn't participated in the project, the other proofs would have been sufficient. You don't need Turing machines to prove undecidability, so throwing them out has no effect on Hilbert's program.
$endgroup$
– Charles Gillingham
Feb 8 at 4:55
add a comment |
$begingroup$
There were several proofs of undecidability and incompleteness using very different tools, from Church, Post, Godel and Turing. They are all equivalent.
Godel's proof is the probably the most direct, because it used nothing more abstract than ordinary arithmetic.
Turing's may be the most consequential, because it has been used to provide a definition of "computability", which is an incredibly rich subject on its own.
Both Godel and Turing's proof depended on the idea of self-reference, where a system as a whole is represented as an object of the system. With Turing, we are talking about what happens when a program takes a program as input. With Godel, we are looking at what happens when we encode a theorem of arithmetic as an integer. You can see the parallel here and have a sense of how they are equivalent.
With Godel's proof, there is no escaping the fact that arithmetic must be either undecidable or incomplete.
If you are new to the subject, I recommend Douglas Hofstadter's classic Godel, Escher, Bach, an entertaining book that can give you tools to visualize how these proofs work.
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
$endgroup$
$begingroup$
I'm an amateur veteran at these topics. I've read GEB several times. I don't see how your comment addresses the question.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:23
$begingroup$
The point is that Turing's proof is just one of many. If Turing hadn't participated in the project, the other proofs would have been sufficient. You don't need Turing machines to prove undecidability, so throwing them out has no effect on Hilbert's program.
$endgroup$
– Charles Gillingham
Feb 8 at 4:55
add a comment |
$begingroup$
There were several proofs of undecidability and incompleteness using very different tools, from Church, Post, Godel and Turing. They are all equivalent.
Godel's proof is the probably the most direct, because it used nothing more abstract than ordinary arithmetic.
Turing's may be the most consequential, because it has been used to provide a definition of "computability", which is an incredibly rich subject on its own.
Both Godel and Turing's proof depended on the idea of self-reference, where a system as a whole is represented as an object of the system. With Turing, we are talking about what happens when a program takes a program as input. With Godel, we are looking at what happens when we encode a theorem of arithmetic as an integer. You can see the parallel here and have a sense of how they are equivalent.
With Godel's proof, there is no escaping the fact that arithmetic must be either undecidable or incomplete.
If you are new to the subject, I recommend Douglas Hofstadter's classic Godel, Escher, Bach, an entertaining book that can give you tools to visualize how these proofs work.
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
$endgroup$
There were several proofs of undecidability and incompleteness using very different tools, from Church, Post, Godel and Turing. They are all equivalent.
Godel's proof is the probably the most direct, because it used nothing more abstract than ordinary arithmetic.
Turing's may be the most consequential, because it has been used to provide a definition of "computability", which is an incredibly rich subject on its own.
Both Godel and Turing's proof depended on the idea of self-reference, where a system as a whole is represented as an object of the system. With Turing, we are talking about what happens when a program takes a program as input. With Godel, we are looking at what happens when we encode a theorem of arithmetic as an integer. You can see the parallel here and have a sense of how they are equivalent.
With Godel's proof, there is no escaping the fact that arithmetic must be either undecidable or incomplete.
If you are new to the subject, I recommend Douglas Hofstadter's classic Godel, Escher, Bach, an entertaining book that can give you tools to visualize how these proofs work.
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
answered Jan 27 at 18:12
Charles GillinghamCharles Gillingham
294112
294112
$begingroup$
I'm an amateur veteran at these topics. I've read GEB several times. I don't see how your comment addresses the question.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:23
$begingroup$
The point is that Turing's proof is just one of many. If Turing hadn't participated in the project, the other proofs would have been sufficient. You don't need Turing machines to prove undecidability, so throwing them out has no effect on Hilbert's program.
$endgroup$
– Charles Gillingham
Feb 8 at 4:55
add a comment |
$begingroup$
I'm an amateur veteran at these topics. I've read GEB several times. I don't see how your comment addresses the question.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:23
$begingroup$
The point is that Turing's proof is just one of many. If Turing hadn't participated in the project, the other proofs would have been sufficient. You don't need Turing machines to prove undecidability, so throwing them out has no effect on Hilbert's program.
$endgroup$
– Charles Gillingham
Feb 8 at 4:55
$begingroup$
I'm an amateur veteran at these topics. I've read GEB several times. I don't see how your comment addresses the question.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:23
$begingroup$
I'm an amateur veteran at these topics. I've read GEB several times. I don't see how your comment addresses the question.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:23
$begingroup$
The point is that Turing's proof is just one of many. If Turing hadn't participated in the project, the other proofs would have been sufficient. You don't need Turing machines to prove undecidability, so throwing them out has no effect on Hilbert's program.
$endgroup$
– Charles Gillingham
Feb 8 at 4:55
$begingroup$
The point is that Turing's proof is just one of many. If Turing hadn't participated in the project, the other proofs would have been sufficient. You don't need Turing machines to prove undecidability, so throwing them out has no effect on Hilbert's program.
$endgroup$
– Charles Gillingham
Feb 8 at 4:55
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3089898%2fwhy-does-the-unsolvability-of-the-halting-problem-give-a-negative-solution-to-th%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
$begingroup$
@reuns Not in full detail. But I gather that it can be done using Gödel's ideas. That's not a trivial line of argument though. So the question "why does nobody ever spell out these final steps?" still stands.
$endgroup$
– Sebastian Oberhoff
Jan 27 at 18:39
$begingroup$
Given a program $P$ written in java language, is it clear to you how to formalize "the program $P$ halts" into an arithmetic statement ? To forbid those kind of statement you can disallow infinite quantification, that is only $forall n le N$ is allowed, with $N$ fixed once for all. Your theory is then decidable, but it can't formalize arithmetic. To me the most down-to-earth approach is formalizing mathematical theories in the Turing/program/computability framework, so "$exists n, f(n)$" becomes "does exists_n(f) halt".
$endgroup$
– reuns
Jan 27 at 18:41