Mixing
Legitimacy of Consistency Proofs
$begingroup$
In this question I asked yesterday I put forward two interpretations of a statements such as "System X is consistent". (a) we can think of it as saying no finite sequence of applications of logical rules to the axioms of the system will result in a contradiction and (b) we can view it as a proof in some given formal System Y (where Y could or could not be the same as X) of some appropriate formalization of a sentence like "there doesn't exist a proof of 0 = 1 in System X". Taking the example of PA (Peano Arithmetic) we see that in sense (b), its consistency has been proved in various formal systems, such as ZF as well as much weaker systems. Godel's second incompleteness theorem says that we cannot prove consistency of System X in sense (b) in System X for sufficiently strong systems.
Now the question is why would we trust any proof of consistency of System X in sense (b) in System X. The mere fact we are trying to prove consistency suggests we doubt it in some sense, further if we have System X is inconsistent it is trivial to prove that it is consistent in sense (b). So let System Z be some formal system for which Godel incompleteness does not apply. Say there is some proof the consistency of System Z in System Z. Would that proof be expressing anything meaningful? It seems any proof undertaken in System Z implicitly assumes the consistency of System Z and we could not know, if System Z were to be inconsistent, if your consistency proof was subtly exploiting that inconsistency.
Thus we are forced to ask what the implications of 2nd incompleteness are. I see the import of 2nd incompleteness is this: "we cannot bootstrap consistency proofs". That is we cannot take some exceedingly simple system, System A, that we believe we can take to be manifestly consistent, and from that construct a chain of stronger systems B, C, D, ..., PA, ..., ZF, ... s.t. $vdash_A$ Cons(B), $vdash_B$ Cons(C), ...
Edit: At Carl Mummert's request I am adding a direct statement of a question. The most pertinent question is: Does $vdash_X$ Cons(X) have semantic content? That is does proving the consistency of a System X in System X mean anything, P2 argues why I don't believe it does. P3 then endeavors to understand what the semantic content of Godel's Second Incompleteness Theorem is. So a secondary question is: does that analysis make sense, or does 2nd incompleteness say more?
logic foundations incompleteness
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
$endgroup$
|
show 3 more comments
$begingroup$
In this question I asked yesterday I put forward two interpretations of a statements such as "System X is consistent". (a) we can think of it as saying no finite sequence of applications of logical rules to the axioms of the system will result in a contradiction and (b) we can view it as a proof in some given formal System Y (where Y could or could not be the same as X) of some appropriate formalization of a sentence like "there doesn't exist a proof of 0 = 1 in System X". Taking the example of PA (Peano Arithmetic) we see that in sense (b), its consistency has been proved in various formal systems, such as ZF as well as much weaker systems. Godel's second incompleteness theorem says that we cannot prove consistency of System X in sense (b) in System X for sufficiently strong systems.
Now the question is why would we trust any proof of consistency of System X in sense (b) in System X. The mere fact we are trying to prove consistency suggests we doubt it in some sense, further if we have System X is inconsistent it is trivial to prove that it is consistent in sense (b). So let System Z be some formal system for which Godel incompleteness does not apply. Say there is some proof the consistency of System Z in System Z. Would that proof be expressing anything meaningful? It seems any proof undertaken in System Z implicitly assumes the consistency of System Z and we could not know, if System Z were to be inconsistent, if your consistency proof was subtly exploiting that inconsistency.
Thus we are forced to ask what the implications of 2nd incompleteness are. I see the import of 2nd incompleteness is this: "we cannot bootstrap consistency proofs". That is we cannot take some exceedingly simple system, System A, that we believe we can take to be manifestly consistent, and from that construct a chain of stronger systems B, C, D, ..., PA, ..., ZF, ... s.t. $vdash_A$ Cons(B), $vdash_B$ Cons(C), ...
Edit: At Carl Mummert's request I am adding a direct statement of a question. The most pertinent question is: Does $vdash_X$ Cons(X) have semantic content? That is does proving the consistency of a System X in System X mean anything, P2 argues why I don't believe it does. P3 then endeavors to understand what the semantic content of Godel's Second Incompleteness Theorem is. So a secondary question is: does that analysis make sense, or does 2nd incompleteness say more?
logic foundations incompleteness
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
$endgroup$
$begingroup$
If "System Z" is "suffiently strong", G's Theorem precludes that "there is some proof the consistency of System Z in System Z". The simplest translation of G's 2nd Incompl Th is "a consistent system cannot prove its own consistency".
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:28
$begingroup$
Yeah, I stated let System Z be a system s.t. Godel incompleteness doesn't apply, i.e. one in which you cannot formalize a sufficient amount of arithmetic. The crux of my question is should we care if $vdash_X$ Cons(X) for any System X. As if $vdash_X neg$Cons(X) then $vdash_X$ Cons(X) so it seems $vdash_X$ Cons(X) has no semantic content.
$endgroup$
– Keefer Rowan
Jan 23 at 16:33
2
$begingroup$
See Self-verifying theories and the post How to think about theories that prove their own inconsistency?
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:47
2
$begingroup$
I agree that a proof of Con(T) from T or stronger wouldn’t necessarily be convincing to a skeptic. And also agree taking proof from $T$ as meaningful is implicitly assuming Con(T), or at least the consistency of the fragment you use. On the other hand I think “I believe PA is consistent because ZF proves it and I believe ZF is arithmetically sound” is reasonable, even if it misses the point a bit. More interesting are the proofs of Gentzen, Godel, and Friedman, from much more conservative assumptions, in some ways weaker than even PA, though of course by GIT they are not strictly weaker.
$endgroup$
– spaceisdarkgreen
Jan 23 at 17:32
1
$begingroup$
Could you please edit the post to include a more direct and succinct statement of the question? I'd like to think about an answer but I am not sure what you are asking.
$endgroup$
– Carl Mummert
Jan 24 at 19:23
|
show 3 more comments
$begingroup$
In this question I asked yesterday I put forward two interpretations of a statements such as "System X is consistent". (a) we can think of it as saying no finite sequence of applications of logical rules to the axioms of the system will result in a contradiction and (b) we can view it as a proof in some given formal System Y (where Y could or could not be the same as X) of some appropriate formalization of a sentence like "there doesn't exist a proof of 0 = 1 in System X". Taking the example of PA (Peano Arithmetic) we see that in sense (b), its consistency has been proved in various formal systems, such as ZF as well as much weaker systems. Godel's second incompleteness theorem says that we cannot prove consistency of System X in sense (b) in System X for sufficiently strong systems.
Now the question is why would we trust any proof of consistency of System X in sense (b) in System X. The mere fact we are trying to prove consistency suggests we doubt it in some sense, further if we have System X is inconsistent it is trivial to prove that it is consistent in sense (b). So let System Z be some formal system for which Godel incompleteness does not apply. Say there is some proof the consistency of System Z in System Z. Would that proof be expressing anything meaningful? It seems any proof undertaken in System Z implicitly assumes the consistency of System Z and we could not know, if System Z were to be inconsistent, if your consistency proof was subtly exploiting that inconsistency.
Thus we are forced to ask what the implications of 2nd incompleteness are. I see the import of 2nd incompleteness is this: "we cannot bootstrap consistency proofs". That is we cannot take some exceedingly simple system, System A, that we believe we can take to be manifestly consistent, and from that construct a chain of stronger systems B, C, D, ..., PA, ..., ZF, ... s.t. $vdash_A$ Cons(B), $vdash_B$ Cons(C), ...
Edit: At Carl Mummert's request I am adding a direct statement of a question. The most pertinent question is: Does $vdash_X$ Cons(X) have semantic content? That is does proving the consistency of a System X in System X mean anything, P2 argues why I don't believe it does. P3 then endeavors to understand what the semantic content of Godel's Second Incompleteness Theorem is. So a secondary question is: does that analysis make sense, or does 2nd incompleteness say more?
logic foundations incompleteness
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
$endgroup$
In this question I asked yesterday I put forward two interpretations of a statements such as "System X is consistent". (a) we can think of it as saying no finite sequence of applications of logical rules to the axioms of the system will result in a contradiction and (b) we can view it as a proof in some given formal System Y (where Y could or could not be the same as X) of some appropriate formalization of a sentence like "there doesn't exist a proof of 0 = 1 in System X". Taking the example of PA (Peano Arithmetic) we see that in sense (b), its consistency has been proved in various formal systems, such as ZF as well as much weaker systems. Godel's second incompleteness theorem says that we cannot prove consistency of System X in sense (b) in System X for sufficiently strong systems.
Now the question is why would we trust any proof of consistency of System X in sense (b) in System X. The mere fact we are trying to prove consistency suggests we doubt it in some sense, further if we have System X is inconsistent it is trivial to prove that it is consistent in sense (b). So let System Z be some formal system for which Godel incompleteness does not apply. Say there is some proof the consistency of System Z in System Z. Would that proof be expressing anything meaningful? It seems any proof undertaken in System Z implicitly assumes the consistency of System Z and we could not know, if System Z were to be inconsistent, if your consistency proof was subtly exploiting that inconsistency.
Thus we are forced to ask what the implications of 2nd incompleteness are. I see the import of 2nd incompleteness is this: "we cannot bootstrap consistency proofs". That is we cannot take some exceedingly simple system, System A, that we believe we can take to be manifestly consistent, and from that construct a chain of stronger systems B, C, D, ..., PA, ..., ZF, ... s.t. $vdash_A$ Cons(B), $vdash_B$ Cons(C), ...
Edit: At Carl Mummert's request I am adding a direct statement of a question. The most pertinent question is: Does $vdash_X$ Cons(X) have semantic content? That is does proving the consistency of a System X in System X mean anything, P2 argues why I don't believe it does. P3 then endeavors to understand what the semantic content of Godel's Second Incompleteness Theorem is. So a secondary question is: does that analysis make sense, or does 2nd incompleteness say more?
logic foundations incompleteness
logic foundations incompleteness
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
edited Jan 24 at 19:30
Keefer Rowan
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
asked Jan 23 at 16:13
Keefer RowanKeefer Rowan
20510
20510
$begingroup$
If "System Z" is "suffiently strong", G's Theorem precludes that "there is some proof the consistency of System Z in System Z". The simplest translation of G's 2nd Incompl Th is "a consistent system cannot prove its own consistency".
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:28
$begingroup$
Yeah, I stated let System Z be a system s.t. Godel incompleteness doesn't apply, i.e. one in which you cannot formalize a sufficient amount of arithmetic. The crux of my question is should we care if $vdash_X$ Cons(X) for any System X. As if $vdash_X neg$Cons(X) then $vdash_X$ Cons(X) so it seems $vdash_X$ Cons(X) has no semantic content.
$endgroup$
– Keefer Rowan
Jan 23 at 16:33
2
$begingroup$
See Self-verifying theories and the post How to think about theories that prove their own inconsistency?
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:47
2
$begingroup$
I agree that a proof of Con(T) from T or stronger wouldn’t necessarily be convincing to a skeptic. And also agree taking proof from $T$ as meaningful is implicitly assuming Con(T), or at least the consistency of the fragment you use. On the other hand I think “I believe PA is consistent because ZF proves it and I believe ZF is arithmetically sound” is reasonable, even if it misses the point a bit. More interesting are the proofs of Gentzen, Godel, and Friedman, from much more conservative assumptions, in some ways weaker than even PA, though of course by GIT they are not strictly weaker.
$endgroup$
– spaceisdarkgreen
Jan 23 at 17:32
1
$begingroup$
Could you please edit the post to include a more direct and succinct statement of the question? I'd like to think about an answer but I am not sure what you are asking.
$endgroup$
– Carl Mummert
Jan 24 at 19:23
|
show 3 more comments
$begingroup$
If "System Z" is "suffiently strong", G's Theorem precludes that "there is some proof the consistency of System Z in System Z". The simplest translation of G's 2nd Incompl Th is "a consistent system cannot prove its own consistency".
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:28
$begingroup$
Yeah, I stated let System Z be a system s.t. Godel incompleteness doesn't apply, i.e. one in which you cannot formalize a sufficient amount of arithmetic. The crux of my question is should we care if $vdash_X$ Cons(X) for any System X. As if $vdash_X neg$Cons(X) then $vdash_X$ Cons(X) so it seems $vdash_X$ Cons(X) has no semantic content.
$endgroup$
– Keefer Rowan
Jan 23 at 16:33
2
$begingroup$
See Self-verifying theories and the post How to think about theories that prove their own inconsistency?
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:47
2
$begingroup$
I agree that a proof of Con(T) from T or stronger wouldn’t necessarily be convincing to a skeptic. And also agree taking proof from $T$ as meaningful is implicitly assuming Con(T), or at least the consistency of the fragment you use. On the other hand I think “I believe PA is consistent because ZF proves it and I believe ZF is arithmetically sound” is reasonable, even if it misses the point a bit. More interesting are the proofs of Gentzen, Godel, and Friedman, from much more conservative assumptions, in some ways weaker than even PA, though of course by GIT they are not strictly weaker.
$endgroup$
– spaceisdarkgreen
Jan 23 at 17:32
1
$begingroup$
Could you please edit the post to include a more direct and succinct statement of the question? I'd like to think about an answer but I am not sure what you are asking.
$endgroup$
– Carl Mummert
Jan 24 at 19:23
$begingroup$
If "System Z" is "suffiently strong", G's Theorem precludes that "there is some proof the consistency of System Z in System Z". The simplest translation of G's 2nd Incompl Th is "a consistent system cannot prove its own consistency".
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:28
$begingroup$
If "System Z" is "suffiently strong", G's Theorem precludes that "there is some proof the consistency of System Z in System Z". The simplest translation of G's 2nd Incompl Th is "a consistent system cannot prove its own consistency".
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:28
$begingroup$
Yeah, I stated let System Z be a system s.t. Godel incompleteness doesn't apply, i.e. one in which you cannot formalize a sufficient amount of arithmetic. The crux of my question is should we care if $vdash_X$ Cons(X) for any System X. As if $vdash_X neg$Cons(X) then $vdash_X$ Cons(X) so it seems $vdash_X$ Cons(X) has no semantic content.
$endgroup$
– Keefer Rowan
Jan 23 at 16:33
$begingroup$
Yeah, I stated let System Z be a system s.t. Godel incompleteness doesn't apply, i.e. one in which you cannot formalize a sufficient amount of arithmetic. The crux of my question is should we care if $vdash_X$ Cons(X) for any System X. As if $vdash_X neg$Cons(X) then $vdash_X$ Cons(X) so it seems $vdash_X$ Cons(X) has no semantic content.
$endgroup$
– Keefer Rowan
Jan 23 at 16:33
2
2
$begingroup$
See Self-verifying theories and the post How to think about theories that prove their own inconsistency?
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:47
$begingroup$
See Self-verifying theories and the post How to think about theories that prove their own inconsistency?
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:47
2
2
$begingroup$
I agree that a proof of Con(T) from T or stronger wouldn’t necessarily be convincing to a skeptic. And also agree taking proof from $T$ as meaningful is implicitly assuming Con(T), or at least the consistency of the fragment you use. On the other hand I think “I believe PA is consistent because ZF proves it and I believe ZF is arithmetically sound” is reasonable, even if it misses the point a bit. More interesting are the proofs of Gentzen, Godel, and Friedman, from much more conservative assumptions, in some ways weaker than even PA, though of course by GIT they are not strictly weaker.
$endgroup$
– spaceisdarkgreen
Jan 23 at 17:32
$begingroup$
I agree that a proof of Con(T) from T or stronger wouldn’t necessarily be convincing to a skeptic. And also agree taking proof from $T$ as meaningful is implicitly assuming Con(T), or at least the consistency of the fragment you use. On the other hand I think “I believe PA is consistent because ZF proves it and I believe ZF is arithmetically sound” is reasonable, even if it misses the point a bit. More interesting are the proofs of Gentzen, Godel, and Friedman, from much more conservative assumptions, in some ways weaker than even PA, though of course by GIT they are not strictly weaker.
$endgroup$
– spaceisdarkgreen
Jan 23 at 17:32
1
1
$begingroup$
Could you please edit the post to include a more direct and succinct statement of the question? I'd like to think about an answer but I am not sure what you are asking.
$endgroup$
– Carl Mummert
Jan 24 at 19:23
$begingroup$
Could you please edit the post to include a more direct and succinct statement of the question? I'd like to think about an answer but I am not sure what you are asking.
$endgroup$
– Carl Mummert
Jan 24 at 19:23
|
show 3 more comments
1 Answer
1
active
oldest
votes
$begingroup$
You are correct in your explanation of why no proof of self-consistency can ever be trusted. If a proposed nice formal system $S$ (that interprets PA and has a proof verifier program) proves its own consistency, then the incompleteness theorems tell us that in fact it is not consistent. Even more so, $S$ itself knows this fact. This is completely contrary to what Hilbert expected.
Symbolically we can prove Godel's second incompleteness theorems expressed in provability logic:
$
defnn{mathbb{N}}
defcon{text{Con}}
defsound{text{Sound}}
$
- (GI*) If $S ⊢ con(S)$ then $S ⊢ 0=1$.
- (GI) $S ⊢ ⬜con(S)→⬜(0=1)$.
In general, $con(S)$ does not say that $S$ is consistent, but merely says that $S$ is arithmetically consistent, namely that $S$ does not prove $(0=1)$.
If $S$ proves $(0=1)$, then $S$ is useless because it proves every false arithmetical sentence. So for $S$ to be useful it must not prove $(0=1)$, in which case $con(S)$ is a true arithmetical sentence, and hence by (GI*) $S$ must not prove the true arithmetical sentence $con(S)$.
So it is not that $S ⊢ con(S)$ has no semantic content. It is a statement about finite strings, and if it is true then it tells us via (GI*) that $S ⊢ 0=1$. You must distinguish carefully between the meaningfulness of "$S ⊢ con(S)$" and the meaninglessness of asserting "$con(S)$" just because $S$ proves it (which is of course stupid even if the incompleteness theorems did not hold).
But your explanation of "we cannot bootstrap consistency proofs" is incorrect. You are essentially trying to assert:
We cannot take some exceedingly simple system $A$ that we believe is consistent and from that construct a stronger system $B$ such that $A ⊢ con(B)$, and then assert that $B$ is consistent.
This is erroneous; you need $A$ to be arithmetically sound (or at least $Σ_1$-sound) before you can go from "$A ⊢ con(B)$" to "$B$ is consistent"! So it is not enough to start from a consistent $A$. It is true that if $B$ interprets $A$, then $A$ cannot prove $con(B)$ by (GI*), but that fact does not permit you to make the above assertion.
It is not possible to replace "consistent" by "arithmetically sound" either, because arithmetical soundness is not itself an arithmetical property. So I think there is not much you can say about bootstrapping that requires invoking (GI*).
That said, there are things you can say based on either (GI*) or (GI). For example, either of them suffice to show that $⬜P→P$ cannot be an axiom for every $P$. Note the relation with Lob's theorems (L*) and (L). This shows that every useful nice formal system $S$ cannot have an internal self-proof-to-truth assumption. Perhaps this is a better way to understand the impact of incompleteness. Note that $S$ can still have the rule ( if $⊢ ⬜P$ then $⊢ P$ ). In fact, this rule is redundant if $S$ is $Σ_1$-sound.
More interestingly (as shown in the linked post), although $S$ proves $P∨¬P$ for every $P$, it may not prove $□P∨□¬P$, nor even $□P∨□¬P∨□¬(□P∨□¬P)$. And (as shown in the other post on that thread), $S$ cannot even have an internal self-consistency-implies-proof-to-truth assumption, namely that $S$ cannot always prove $¬□(0=1)∧□P→P$ without also proving $□(0=1)$ and rendering it all meaningless.
answered Feb 4 at 7:11
user21820user21820
39.4k543155
$endgroup$
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%2f3084683%2flegitimacy-of-consistency-proofs%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$
You are correct in your explanation of why no proof of self-consistency can ever be trusted. If a proposed nice formal system $S$ (that interprets PA and has a proof verifier program) proves its own consistency, then the incompleteness theorems tell us that in fact it is not consistent. Even more so, $S$ itself knows this fact. This is completely contrary to what Hilbert expected.
Symbolically we can prove Godel's second incompleteness theorems expressed in provability logic:
$
defnn{mathbb{N}}
defcon{text{Con}}
defsound{text{Sound}}
$
- (GI*) If $S ⊢ con(S)$ then $S ⊢ 0=1$.
- (GI) $S ⊢ ⬜con(S)→⬜(0=1)$.
In general, $con(S)$ does not say that $S$ is consistent, but merely says that $S$ is arithmetically consistent, namely that $S$ does not prove $(0=1)$.
If $S$ proves $(0=1)$, then $S$ is useless because it proves every false arithmetical sentence. So for $S$ to be useful it must not prove $(0=1)$, in which case $con(S)$ is a true arithmetical sentence, and hence by (GI*) $S$ must not prove the true arithmetical sentence $con(S)$.
So it is not that $S ⊢ con(S)$ has no semantic content. It is a statement about finite strings, and if it is true then it tells us via (GI*) that $S ⊢ 0=1$. You must distinguish carefully between the meaningfulness of "$S ⊢ con(S)$" and the meaninglessness of asserting "$con(S)$" just because $S$ proves it (which is of course stupid even if the incompleteness theorems did not hold).
But your explanation of "we cannot bootstrap consistency proofs" is incorrect. You are essentially trying to assert:
We cannot take some exceedingly simple system $A$ that we believe is consistent and from that construct a stronger system $B$ such that $A ⊢ con(B)$, and then assert that $B$ is consistent.
This is erroneous; you need $A$ to be arithmetically sound (or at least $Σ_1$-sound) before you can go from "$A ⊢ con(B)$" to "$B$ is consistent"! So it is not enough to start from a consistent $A$. It is true that if $B$ interprets $A$, then $A$ cannot prove $con(B)$ by (GI*), but that fact does not permit you to make the above assertion.
It is not possible to replace "consistent" by "arithmetically sound" either, because arithmetical soundness is not itself an arithmetical property. So I think there is not much you can say about bootstrapping that requires invoking (GI*).
That said, there are things you can say based on either (GI*) or (GI). For example, either of them suffice to show that $⬜P→P$ cannot be an axiom for every $P$. Note the relation with Lob's theorems (L*) and (L). This shows that every useful nice formal system $S$ cannot have an internal self-proof-to-truth assumption. Perhaps this is a better way to understand the impact of incompleteness. Note that $S$ can still have the rule ( if $⊢ ⬜P$ then $⊢ P$ ). In fact, this rule is redundant if $S$ is $Σ_1$-sound.
More interestingly (as shown in the linked post), although $S$ proves $P∨¬P$ for every $P$, it may not prove $□P∨□¬P$, nor even $□P∨□¬P∨□¬(□P∨□¬P)$. And (as shown in the other post on that thread), $S$ cannot even have an internal self-consistency-implies-proof-to-truth assumption, namely that $S$ cannot always prove $¬□(0=1)∧□P→P$ without also proving $□(0=1)$ and rendering it all meaningless.
answered Feb 4 at 7:11
user21820user21820
39.4k543155
$endgroup$
add a comment |
$begingroup$
You are correct in your explanation of why no proof of self-consistency can ever be trusted. If a proposed nice formal system $S$ (that interprets PA and has a proof verifier program) proves its own consistency, then the incompleteness theorems tell us that in fact it is not consistent. Even more so, $S$ itself knows this fact. This is completely contrary to what Hilbert expected.
Symbolically we can prove Godel's second incompleteness theorems expressed in provability logic:
$
defnn{mathbb{N}}
defcon{text{Con}}
defsound{text{Sound}}
$
- (GI*) If $S ⊢ con(S)$ then $S ⊢ 0=1$.
- (GI) $S ⊢ ⬜con(S)→⬜(0=1)$.
In general, $con(S)$ does not say that $S$ is consistent, but merely says that $S$ is arithmetically consistent, namely that $S$ does not prove $(0=1)$.
If $S$ proves $(0=1)$, then $S$ is useless because it proves every false arithmetical sentence. So for $S$ to be useful it must not prove $(0=1)$, in which case $con(S)$ is a true arithmetical sentence, and hence by (GI*) $S$ must not prove the true arithmetical sentence $con(S)$.
So it is not that $S ⊢ con(S)$ has no semantic content. It is a statement about finite strings, and if it is true then it tells us via (GI*) that $S ⊢ 0=1$. You must distinguish carefully between the meaningfulness of "$S ⊢ con(S)$" and the meaninglessness of asserting "$con(S)$" just because $S$ proves it (which is of course stupid even if the incompleteness theorems did not hold).
But your explanation of "we cannot bootstrap consistency proofs" is incorrect. You are essentially trying to assert:
We cannot take some exceedingly simple system $A$ that we believe is consistent and from that construct a stronger system $B$ such that $A ⊢ con(B)$, and then assert that $B$ is consistent.
This is erroneous; you need $A$ to be arithmetically sound (or at least $Σ_1$-sound) before you can go from "$A ⊢ con(B)$" to "$B$ is consistent"! So it is not enough to start from a consistent $A$. It is true that if $B$ interprets $A$, then $A$ cannot prove $con(B)$ by (GI*), but that fact does not permit you to make the above assertion.
It is not possible to replace "consistent" by "arithmetically sound" either, because arithmetical soundness is not itself an arithmetical property. So I think there is not much you can say about bootstrapping that requires invoking (GI*).
That said, there are things you can say based on either (GI*) or (GI). For example, either of them suffice to show that $⬜P→P$ cannot be an axiom for every $P$. Note the relation with Lob's theorems (L*) and (L). This shows that every useful nice formal system $S$ cannot have an internal self-proof-to-truth assumption. Perhaps this is a better way to understand the impact of incompleteness. Note that $S$ can still have the rule ( if $⊢ ⬜P$ then $⊢ P$ ). In fact, this rule is redundant if $S$ is $Σ_1$-sound.
More interestingly (as shown in the linked post), although $S$ proves $P∨¬P$ for every $P$, it may not prove $□P∨□¬P$, nor even $□P∨□¬P∨□¬(□P∨□¬P)$. And (as shown in the other post on that thread), $S$ cannot even have an internal self-consistency-implies-proof-to-truth assumption, namely that $S$ cannot always prove $¬□(0=1)∧□P→P$ without also proving $□(0=1)$ and rendering it all meaningless.
answered Feb 4 at 7:11
user21820user21820
39.4k543155
$endgroup$
add a comment |
$begingroup$
You are correct in your explanation of why no proof of self-consistency can ever be trusted. If a proposed nice formal system $S$ (that interprets PA and has a proof verifier program) proves its own consistency, then the incompleteness theorems tell us that in fact it is not consistent. Even more so, $S$ itself knows this fact. This is completely contrary to what Hilbert expected.
Symbolically we can prove Godel's second incompleteness theorems expressed in provability logic:
$
defnn{mathbb{N}}
defcon{text{Con}}
defsound{text{Sound}}
$
- (GI*) If $S ⊢ con(S)$ then $S ⊢ 0=1$.
- (GI) $S ⊢ ⬜con(S)→⬜(0=1)$.
In general, $con(S)$ does not say that $S$ is consistent, but merely says that $S$ is arithmetically consistent, namely that $S$ does not prove $(0=1)$.
If $S$ proves $(0=1)$, then $S$ is useless because it proves every false arithmetical sentence. So for $S$ to be useful it must not prove $(0=1)$, in which case $con(S)$ is a true arithmetical sentence, and hence by (GI*) $S$ must not prove the true arithmetical sentence $con(S)$.
So it is not that $S ⊢ con(S)$ has no semantic content. It is a statement about finite strings, and if it is true then it tells us via (GI*) that $S ⊢ 0=1$. You must distinguish carefully between the meaningfulness of "$S ⊢ con(S)$" and the meaninglessness of asserting "$con(S)$" just because $S$ proves it (which is of course stupid even if the incompleteness theorems did not hold).
But your explanation of "we cannot bootstrap consistency proofs" is incorrect. You are essentially trying to assert:
We cannot take some exceedingly simple system $A$ that we believe is consistent and from that construct a stronger system $B$ such that $A ⊢ con(B)$, and then assert that $B$ is consistent.
This is erroneous; you need $A$ to be arithmetically sound (or at least $Σ_1$-sound) before you can go from "$A ⊢ con(B)$" to "$B$ is consistent"! So it is not enough to start from a consistent $A$. It is true that if $B$ interprets $A$, then $A$ cannot prove $con(B)$ by (GI*), but that fact does not permit you to make the above assertion.
It is not possible to replace "consistent" by "arithmetically sound" either, because arithmetical soundness is not itself an arithmetical property. So I think there is not much you can say about bootstrapping that requires invoking (GI*).
That said, there are things you can say based on either (GI*) or (GI). For example, either of them suffice to show that $⬜P→P$ cannot be an axiom for every $P$. Note the relation with Lob's theorems (L*) and (L). This shows that every useful nice formal system $S$ cannot have an internal self-proof-to-truth assumption. Perhaps this is a better way to understand the impact of incompleteness. Note that $S$ can still have the rule ( if $⊢ ⬜P$ then $⊢ P$ ). In fact, this rule is redundant if $S$ is $Σ_1$-sound.
More interestingly (as shown in the linked post), although $S$ proves $P∨¬P$ for every $P$, it may not prove $□P∨□¬P$, nor even $□P∨□¬P∨□¬(□P∨□¬P)$. And (as shown in the other post on that thread), $S$ cannot even have an internal self-consistency-implies-proof-to-truth assumption, namely that $S$ cannot always prove $¬□(0=1)∧□P→P$ without also proving $□(0=1)$ and rendering it all meaningless.
answered Feb 4 at 7:11
user21820user21820
39.4k543155
$endgroup$
You are correct in your explanation of why no proof of self-consistency can ever be trusted. If a proposed nice formal system $S$ (that interprets PA and has a proof verifier program) proves its own consistency, then the incompleteness theorems tell us that in fact it is not consistent. Even more so, $S$ itself knows this fact. This is completely contrary to what Hilbert expected.
Symbolically we can prove Godel's second incompleteness theorems expressed in provability logic:
$
defnn{mathbb{N}}
defcon{text{Con}}
defsound{text{Sound}}
$
- (GI*) If $S ⊢ con(S)$ then $S ⊢ 0=1$.
- (GI) $S ⊢ ⬜con(S)→⬜(0=1)$.
In general, $con(S)$ does not say that $S$ is consistent, but merely says that $S$ is arithmetically consistent, namely that $S$ does not prove $(0=1)$.
If $S$ proves $(0=1)$, then $S$ is useless because it proves every false arithmetical sentence. So for $S$ to be useful it must not prove $(0=1)$, in which case $con(S)$ is a true arithmetical sentence, and hence by (GI*) $S$ must not prove the true arithmetical sentence $con(S)$.
So it is not that $S ⊢ con(S)$ has no semantic content. It is a statement about finite strings, and if it is true then it tells us via (GI*) that $S ⊢ 0=1$. You must distinguish carefully between the meaningfulness of "$S ⊢ con(S)$" and the meaninglessness of asserting "$con(S)$" just because $S$ proves it (which is of course stupid even if the incompleteness theorems did not hold).
But your explanation of "we cannot bootstrap consistency proofs" is incorrect. You are essentially trying to assert:
We cannot take some exceedingly simple system $A$ that we believe is consistent and from that construct a stronger system $B$ such that $A ⊢ con(B)$, and then assert that $B$ is consistent.
This is erroneous; you need $A$ to be arithmetically sound (or at least $Σ_1$-sound) before you can go from "$A ⊢ con(B)$" to "$B$ is consistent"! So it is not enough to start from a consistent $A$. It is true that if $B$ interprets $A$, then $A$ cannot prove $con(B)$ by (GI*), but that fact does not permit you to make the above assertion.
It is not possible to replace "consistent" by "arithmetically sound" either, because arithmetical soundness is not itself an arithmetical property. So I think there is not much you can say about bootstrapping that requires invoking (GI*).
That said, there are things you can say based on either (GI*) or (GI). For example, either of them suffice to show that $⬜P→P$ cannot be an axiom for every $P$. Note the relation with Lob's theorems (L*) and (L). This shows that every useful nice formal system $S$ cannot have an internal self-proof-to-truth assumption. Perhaps this is a better way to understand the impact of incompleteness. Note that $S$ can still have the rule ( if $⊢ ⬜P$ then $⊢ P$ ). In fact, this rule is redundant if $S$ is $Σ_1$-sound.
More interestingly (as shown in the linked post), although $S$ proves $P∨¬P$ for every $P$, it may not prove $□P∨□¬P$, nor even $□P∨□¬P∨□¬(□P∨□¬P)$. And (as shown in the other post on that thread), $S$ cannot even have an internal self-consistency-implies-proof-to-truth assumption, namely that $S$ cannot always prove $¬□(0=1)∧□P→P$ without also proving $□(0=1)$ and rendering it all meaningless.
answered Feb 4 at 7:11
user21820user21820
39.4k543155
answered Feb 4 at 7:11
user21820user21820
39.4k543155
answered Feb 4 at 7:11
user21820user21820
39.4k543155
answered Feb 4 at 7:11
user21820user21820
39.4k543155
39.4k543155
add a comment |
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%2f3084683%2flegitimacy-of-consistency-proofs%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$
If "System Z" is "suffiently strong", G's Theorem precludes that "there is some proof the consistency of System Z in System Z". The simplest translation of G's 2nd Incompl Th is "a consistent system cannot prove its own consistency".
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:28
$begingroup$
Yeah, I stated let System Z be a system s.t. Godel incompleteness doesn't apply, i.e. one in which you cannot formalize a sufficient amount of arithmetic. The crux of my question is should we care if $vdash_X$ Cons(X) for any System X. As if $vdash_X neg$Cons(X) then $vdash_X$ Cons(X) so it seems $vdash_X$ Cons(X) has no semantic content.
$endgroup$
– Keefer Rowan
Jan 23 at 16:33
2
$begingroup$
See Self-verifying theories and the post How to think about theories that prove their own inconsistency?
$endgroup$
– Mauro ALLEGRANZA
Jan 23 at 16:47
2
$begingroup$
I agree that a proof of Con(T) from T or stronger wouldn’t necessarily be convincing to a skeptic. And also agree taking proof from $T$ as meaningful is implicitly assuming Con(T), or at least the consistency of the fragment you use. On the other hand I think “I believe PA is consistent because ZF proves it and I believe ZF is arithmetically sound” is reasonable, even if it misses the point a bit. More interesting are the proofs of Gentzen, Godel, and Friedman, from much more conservative assumptions, in some ways weaker than even PA, though of course by GIT they are not strictly weaker.
$endgroup$
– spaceisdarkgreen
Jan 23 at 17:32
1
$begingroup$
Could you please edit the post to include a more direct and succinct statement of the question? I'd like to think about an answer but I am not sure what you are asking.
$endgroup$
– Carl Mummert
Jan 24 at 19:23