What was the exact form of Gödel's original Second Incompleteness Theorem?
$begingroup$
Gödel's second incompleteness theorem is usually stated as:
Any consistent formal system $F$ capable of elementary arithmetic can't prove its own consistency.
I'm having trouble deducing this statement using just the pieces Gödel had available in 1931. As I understand it those were:
Suppose $G$ is provable. Then this can be converted into a proof of $neg G$. Hence, $F$ is inconsistent.
Suppose $neg G$ is provable. Then $F$ "believes" that $G$ can be proven. This doesn't necessarily have to be true. But at the very least $F$ is unsound.
The best I'm able to deduce from this is this:
Any sound formal system $F$ capable of elementary arithmetic can't prove its own consistency.
Take the contrapositive of the first of the previous deductions. Because consistency is a syntactic property this can be fully formalized in $F$ as "$F$ is consistent $implies$ $neg G$ is provable". Moreover, there really isn't anything stopping us from actually proving this theorem in $F$. But then, provided $F$ is sound, $F$ can't prove its own consistency. If it could, then using modus ponens it could prove $neg G$. However, that would make $F$ unsound. $square$
This is a decidedly weaker version of the second incompleteness theorem. And I don't see how to plug the hole without invoking Rosser's Theorem. Is this all that Gödel had in 1931?
proof-verification incompleteness
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
$endgroup$
|
show 2 more comments
$begingroup$
Gödel's second incompleteness theorem is usually stated as:
Any consistent formal system $F$ capable of elementary arithmetic can't prove its own consistency.
I'm having trouble deducing this statement using just the pieces Gödel had available in 1931. As I understand it those were:
Suppose $G$ is provable. Then this can be converted into a proof of $neg G$. Hence, $F$ is inconsistent.
Suppose $neg G$ is provable. Then $F$ "believes" that $G$ can be proven. This doesn't necessarily have to be true. But at the very least $F$ is unsound.
The best I'm able to deduce from this is this:
Any sound formal system $F$ capable of elementary arithmetic can't prove its own consistency.
Take the contrapositive of the first of the previous deductions. Because consistency is a syntactic property this can be fully formalized in $F$ as "$F$ is consistent $implies$ $neg G$ is provable". Moreover, there really isn't anything stopping us from actually proving this theorem in $F$. But then, provided $F$ is sound, $F$ can't prove its own consistency. If it could, then using modus ponens it could prove $neg G$. However, that would make $F$ unsound. $square$
This is a decidedly weaker version of the second incompleteness theorem. And I don't see how to plug the hole without invoking Rosser's Theorem. Is this all that Gödel had in 1931?
proof-verification incompleteness
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
$endgroup$
2
$begingroup$
The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:33
$begingroup$
@Peter This only shows "$F$ is inconsistent $implies$ $F$ can prove it's own consistency". What I want is the other direction: "$F$ can prove it's own consistency $implies$ $F$ is inconsistent".
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 14:41
$begingroup$
This is of course the hard part. If we assume that $F$ is consistent, then $G$ and $"not G"$ cannot be both deduced. This leads to the contradiction you mentioned.
$endgroup$
– Peter
Dec 23 '18 at 14:45
$begingroup$
Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:54
$begingroup$
@Peter I still don't see at what point you tightened the reasoning compared to my argument.
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 15:02
|
show 2 more comments
$begingroup$
Gödel's second incompleteness theorem is usually stated as:
Any consistent formal system $F$ capable of elementary arithmetic can't prove its own consistency.
I'm having trouble deducing this statement using just the pieces Gödel had available in 1931. As I understand it those were:
Suppose $G$ is provable. Then this can be converted into a proof of $neg G$. Hence, $F$ is inconsistent.
Suppose $neg G$ is provable. Then $F$ "believes" that $G$ can be proven. This doesn't necessarily have to be true. But at the very least $F$ is unsound.
The best I'm able to deduce from this is this:
Any sound formal system $F$ capable of elementary arithmetic can't prove its own consistency.
Take the contrapositive of the first of the previous deductions. Because consistency is a syntactic property this can be fully formalized in $F$ as "$F$ is consistent $implies$ $neg G$ is provable". Moreover, there really isn't anything stopping us from actually proving this theorem in $F$. But then, provided $F$ is sound, $F$ can't prove its own consistency. If it could, then using modus ponens it could prove $neg G$. However, that would make $F$ unsound. $square$
This is a decidedly weaker version of the second incompleteness theorem. And I don't see how to plug the hole without invoking Rosser's Theorem. Is this all that Gödel had in 1931?
proof-verification incompleteness
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
$endgroup$
Gödel's second incompleteness theorem is usually stated as:
Any consistent formal system $F$ capable of elementary arithmetic can't prove its own consistency.
I'm having trouble deducing this statement using just the pieces Gödel had available in 1931. As I understand it those were:
Suppose $G$ is provable. Then this can be converted into a proof of $neg G$. Hence, $F$ is inconsistent.
Suppose $neg G$ is provable. Then $F$ "believes" that $G$ can be proven. This doesn't necessarily have to be true. But at the very least $F$ is unsound.
The best I'm able to deduce from this is this:
Any sound formal system $F$ capable of elementary arithmetic can't prove its own consistency.
Take the contrapositive of the first of the previous deductions. Because consistency is a syntactic property this can be fully formalized in $F$ as "$F$ is consistent $implies$ $neg G$ is provable". Moreover, there really isn't anything stopping us from actually proving this theorem in $F$. But then, provided $F$ is sound, $F$ can't prove its own consistency. If it could, then using modus ponens it could prove $neg G$. However, that would make $F$ unsound. $square$
This is a decidedly weaker version of the second incompleteness theorem. And I don't see how to plug the hole without invoking Rosser's Theorem. Is this all that Gödel had in 1931?
proof-verification incompleteness
proof-verification incompleteness
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
edited Dec 23 '18 at 14:42
mrtaurho
6,19771641
6,19771641
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
asked Dec 23 '18 at 14:22
Sebastian OberhoffSebastian Oberhoff
587311
587311
2
$begingroup$
The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:33
$begingroup$
@Peter This only shows "$F$ is inconsistent $implies$ $F$ can prove it's own consistency". What I want is the other direction: "$F$ can prove it's own consistency $implies$ $F$ is inconsistent".
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 14:41
$begingroup$
This is of course the hard part. If we assume that $F$ is consistent, then $G$ and $"not G"$ cannot be both deduced. This leads to the contradiction you mentioned.
$endgroup$
– Peter
Dec 23 '18 at 14:45
$begingroup$
Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:54
$begingroup$
@Peter I still don't see at what point you tightened the reasoning compared to my argument.
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 15:02
|
show 2 more comments
2
$begingroup$
The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:33
$begingroup$
@Peter This only shows "$F$ is inconsistent $implies$ $F$ can prove it's own consistency". What I want is the other direction: "$F$ can prove it's own consistency $implies$ $F$ is inconsistent".
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 14:41
$begingroup$
This is of course the hard part. If we assume that $F$ is consistent, then $G$ and $"not G"$ cannot be both deduced. This leads to the contradiction you mentioned.
$endgroup$
– Peter
Dec 23 '18 at 14:45
$begingroup$
Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:54
$begingroup$
@Peter I still don't see at what point you tightened the reasoning compared to my argument.
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 15:02
2
2
$begingroup$
The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:33
$begingroup$
The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:33
$begingroup$
@Peter This only shows "$F$ is inconsistent $implies$ $F$ can prove it's own consistency". What I want is the other direction: "$F$ can prove it's own consistency $implies$ $F$ is inconsistent".
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 14:41
$begingroup$
@Peter This only shows "$F$ is inconsistent $implies$ $F$ can prove it's own consistency". What I want is the other direction: "$F$ can prove it's own consistency $implies$ $F$ is inconsistent".
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 14:41
$begingroup$
This is of course the hard part. If we assume that $F$ is consistent, then $G$ and $"not G"$ cannot be both deduced. This leads to the contradiction you mentioned.
$endgroup$
– Peter
Dec 23 '18 at 14:45
$begingroup$
This is of course the hard part. If we assume that $F$ is consistent, then $G$ and $"not G"$ cannot be both deduced. This leads to the contradiction you mentioned.
$endgroup$
– Peter
Dec 23 '18 at 14:45
$begingroup$
Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:54
$begingroup$
Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:54
$begingroup$
@Peter I still don't see at what point you tightened the reasoning compared to my argument.
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 15:02
$begingroup$
@Peter I still don't see at what point you tightened the reasoning compared to my argument.
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 15:02
|
show 2 more comments
1 Answer
1
active
oldest
votes
$begingroup$
The negation of "$G$ is provable" isn't "$neg G$ is provable". It's "$G$ isn't provable" = $G$. The contrapositive of the first deduction is thus "$F$ is consistent $implies$ $G$". Now suppose $F$ is consistent and can prove its own consistency. Then $F$ can prove $G$, rendering it inconsistent. ⚡
And all is well.
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
$endgroup$
$begingroup$
I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid.
$endgroup$
– Noah Schweber
Dec 23 '18 at 16:39
add a comment |
Your Answer
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%2f3050379%2fwhat-was-the-exact-form-of-g%25c3%25b6dels-original-second-incompleteness-theorem%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
The negation of "$G$ is provable" isn't "$neg G$ is provable". It's "$G$ isn't provable" = $G$. The contrapositive of the first deduction is thus "$F$ is consistent $implies$ $G$". Now suppose $F$ is consistent and can prove its own consistency. Then $F$ can prove $G$, rendering it inconsistent. ⚡
And all is well.
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
$endgroup$
$begingroup$
I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid.
$endgroup$
– Noah Schweber
Dec 23 '18 at 16:39
add a comment |
$begingroup$
The negation of "$G$ is provable" isn't "$neg G$ is provable". It's "$G$ isn't provable" = $G$. The contrapositive of the first deduction is thus "$F$ is consistent $implies$ $G$". Now suppose $F$ is consistent and can prove its own consistency. Then $F$ can prove $G$, rendering it inconsistent. ⚡
And all is well.
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
$endgroup$
$begingroup$
I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid.
$endgroup$
– Noah Schweber
Dec 23 '18 at 16:39
add a comment |
$begingroup$
The negation of "$G$ is provable" isn't "$neg G$ is provable". It's "$G$ isn't provable" = $G$. The contrapositive of the first deduction is thus "$F$ is consistent $implies$ $G$". Now suppose $F$ is consistent and can prove its own consistency. Then $F$ can prove $G$, rendering it inconsistent. ⚡
And all is well.
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
$endgroup$
The negation of "$G$ is provable" isn't "$neg G$ is provable". It's "$G$ isn't provable" = $G$. The contrapositive of the first deduction is thus "$F$ is consistent $implies$ $G$". Now suppose $F$ is consistent and can prove its own consistency. Then $F$ can prove $G$, rendering it inconsistent. ⚡
And all is well.
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
edited Dec 23 '18 at 16:57
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
answered Dec 23 '18 at 15:24
Sebastian OberhoffSebastian Oberhoff
587311
587311
$begingroup$
I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid.
$endgroup$
– Noah Schweber
Dec 23 '18 at 16:39
add a comment |
$begingroup$
I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid.
$endgroup$
– Noah Schweber
Dec 23 '18 at 16:39
$begingroup$
I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid.
$endgroup$
– Noah Schweber
Dec 23 '18 at 16:39
$begingroup$
I've upvoted since this is correct, but I strongly think you should delete the self-deprecation - all this stuff is quite reasonable to find confusing, and for similar readers' sake we should avoid implying that these issues are stupid.
$endgroup$
– Noah Schweber
Dec 23 '18 at 16:39
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%2f3050379%2fwhat-was-the-exact-form-of-g%25c3%25b6dels-original-second-incompleteness-theorem%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
2
$begingroup$
The condition that the system is consistent is crucial. Otherwise it could prove everything, in particular its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:33
$begingroup$
@Peter This only shows "$F$ is inconsistent $implies$ $F$ can prove it's own consistency". What I want is the other direction: "$F$ can prove it's own consistency $implies$ $F$ is inconsistent".
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 14:41
$begingroup$
This is of course the hard part. If we assume that $F$ is consistent, then $G$ and $"not G"$ cannot be both deduced. This leads to the contradiction you mentioned.
$endgroup$
– Peter
Dec 23 '18 at 14:45
$begingroup$
Goedel showed that , if $F$ is consistent , THEN it cannot prove its own consistency.
$endgroup$
– Peter
Dec 23 '18 at 14:54
$begingroup$
@Peter I still don't see at what point you tightened the reasoning compared to my argument.
$endgroup$
– Sebastian Oberhoff
Dec 23 '18 at 15:02