Consistency of PA from a Formalist Perspective
$begingroup$
In this lengthy thread there's people bickering back and forth about the consistency of PA (Peano Arithmetic) and misunderstandings abound. In reading it I came to an understanding I found useful, though I am not certain of the correctness of. If we take a formalist perspective on the situation and understand mathematical propositions as statements about what happens when we manipulate strings given certain rules, there are two ways of interpreting "the consistency of PA". That is
(a) we can say "PA is consistent" means that any finite series of the applications of logical rules to the axioms of PA will not result in a contradiction, and
(b) the statement "PA is consistent" is rendered as "Con(PA)" appropriately formalized in some formal system (e.g. $neg (0=1)$ in ZFC) and the question is about provability of "Con(PA)" in the given formal system.
It is my understanding (a) has not/cannot be demonstrated as any proofs done in any given formal system of the consistency of PA depend on the consistency of that formal system, which cannot be proved without resorting to a stronger system, and so on, but (b) has been demonstrated in various formal systems. It seems all disagreement as to whether "is PA consistent" is an open question is the result of one party referring to sense (a) and another referring to sense (b), where for sense (a) it is an open (and perhaps unanswerable) question while in sense (b), which is the usual meaning of an open question, it is definitively closed.
Does this analysis make sense? Am I missing anything important?
logic foundations incompleteness peano-axioms
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
$endgroup$
add a comment |
$begingroup$
In this lengthy thread there's people bickering back and forth about the consistency of PA (Peano Arithmetic) and misunderstandings abound. In reading it I came to an understanding I found useful, though I am not certain of the correctness of. If we take a formalist perspective on the situation and understand mathematical propositions as statements about what happens when we manipulate strings given certain rules, there are two ways of interpreting "the consistency of PA". That is
(a) we can say "PA is consistent" means that any finite series of the applications of logical rules to the axioms of PA will not result in a contradiction, and
(b) the statement "PA is consistent" is rendered as "Con(PA)" appropriately formalized in some formal system (e.g. $neg (0=1)$ in ZFC) and the question is about provability of "Con(PA)" in the given formal system.
It is my understanding (a) has not/cannot be demonstrated as any proofs done in any given formal system of the consistency of PA depend on the consistency of that formal system, which cannot be proved without resorting to a stronger system, and so on, but (b) has been demonstrated in various formal systems. It seems all disagreement as to whether "is PA consistent" is an open question is the result of one party referring to sense (a) and another referring to sense (b), where for sense (a) it is an open (and perhaps unanswerable) question while in sense (b), which is the usual meaning of an open question, it is definitively closed.
Does this analysis make sense? Am I missing anything important?
logic foundations incompleteness peano-axioms
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
$endgroup$
$begingroup$
Note for (b), if ¬CON(A) then A⊦CON(PA), also if CON(A), then for A⊦CON(PA) to be true, A need to be the stronger system.
$endgroup$
– Holo
Jan 23 at 10:01
$begingroup$
I have a related question at math.stackexchange.com/questions/3084683/…
$endgroup$
– Keefer Rowan
Jan 23 at 16:45
1
$begingroup$
Your analysis is OK, but I don't think it's a very fruitful topic for MSE for the same reasons as stated in David Roberts's comments on the MO question you link to.
$endgroup$
– Rob Arthan
Jan 23 at 21:38
add a comment |
$begingroup$
In this lengthy thread there's people bickering back and forth about the consistency of PA (Peano Arithmetic) and misunderstandings abound. In reading it I came to an understanding I found useful, though I am not certain of the correctness of. If we take a formalist perspective on the situation and understand mathematical propositions as statements about what happens when we manipulate strings given certain rules, there are two ways of interpreting "the consistency of PA". That is
(a) we can say "PA is consistent" means that any finite series of the applications of logical rules to the axioms of PA will not result in a contradiction, and
(b) the statement "PA is consistent" is rendered as "Con(PA)" appropriately formalized in some formal system (e.g. $neg (0=1)$ in ZFC) and the question is about provability of "Con(PA)" in the given formal system.
It is my understanding (a) has not/cannot be demonstrated as any proofs done in any given formal system of the consistency of PA depend on the consistency of that formal system, which cannot be proved without resorting to a stronger system, and so on, but (b) has been demonstrated in various formal systems. It seems all disagreement as to whether "is PA consistent" is an open question is the result of one party referring to sense (a) and another referring to sense (b), where for sense (a) it is an open (and perhaps unanswerable) question while in sense (b), which is the usual meaning of an open question, it is definitively closed.
Does this analysis make sense? Am I missing anything important?
logic foundations incompleteness peano-axioms
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
$endgroup$
In this lengthy thread there's people bickering back and forth about the consistency of PA (Peano Arithmetic) and misunderstandings abound. In reading it I came to an understanding I found useful, though I am not certain of the correctness of. If we take a formalist perspective on the situation and understand mathematical propositions as statements about what happens when we manipulate strings given certain rules, there are two ways of interpreting "the consistency of PA". That is
(a) we can say "PA is consistent" means that any finite series of the applications of logical rules to the axioms of PA will not result in a contradiction, and
(b) the statement "PA is consistent" is rendered as "Con(PA)" appropriately formalized in some formal system (e.g. $neg (0=1)$ in ZFC) and the question is about provability of "Con(PA)" in the given formal system.
It is my understanding (a) has not/cannot be demonstrated as any proofs done in any given formal system of the consistency of PA depend on the consistency of that formal system, which cannot be proved without resorting to a stronger system, and so on, but (b) has been demonstrated in various formal systems. It seems all disagreement as to whether "is PA consistent" is an open question is the result of one party referring to sense (a) and another referring to sense (b), where for sense (a) it is an open (and perhaps unanswerable) question while in sense (b), which is the usual meaning of an open question, it is definitively closed.
Does this analysis make sense? Am I missing anything important?
logic foundations incompleteness peano-axioms
logic foundations incompleteness peano-axioms
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
edited Jan 23 at 5:43
Ruggiero Rilievi
179112
179112
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
asked Jan 23 at 5:07
Keefer RowanKeefer Rowan
20510
20510
$begingroup$
Note for (b), if ¬CON(A) then A⊦CON(PA), also if CON(A), then for A⊦CON(PA) to be true, A need to be the stronger system.
$endgroup$
– Holo
Jan 23 at 10:01
$begingroup$
I have a related question at math.stackexchange.com/questions/3084683/…
$endgroup$
– Keefer Rowan
Jan 23 at 16:45
1
$begingroup$
Your analysis is OK, but I don't think it's a very fruitful topic for MSE for the same reasons as stated in David Roberts's comments on the MO question you link to.
$endgroup$
– Rob Arthan
Jan 23 at 21:38
add a comment |
$begingroup$
Note for (b), if ¬CON(A) then A⊦CON(PA), also if CON(A), then for A⊦CON(PA) to be true, A need to be the stronger system.
$endgroup$
– Holo
Jan 23 at 10:01
$begingroup$
I have a related question at math.stackexchange.com/questions/3084683/…
$endgroup$
– Keefer Rowan
Jan 23 at 16:45
1
$begingroup$
Your analysis is OK, but I don't think it's a very fruitful topic for MSE for the same reasons as stated in David Roberts's comments on the MO question you link to.
$endgroup$
– Rob Arthan
Jan 23 at 21:38
$begingroup$
Note for (b), if ¬CON(A) then A⊦CON(PA), also if CON(A), then for A⊦CON(PA) to be true, A need to be the stronger system.
$endgroup$
– Holo
Jan 23 at 10:01
$begingroup$
Note for (b), if ¬CON(A) then A⊦CON(PA), also if CON(A), then for A⊦CON(PA) to be true, A need to be the stronger system.
$endgroup$
– Holo
Jan 23 at 10:01
$begingroup$
I have a related question at math.stackexchange.com/questions/3084683/…
$endgroup$
– Keefer Rowan
Jan 23 at 16:45
$begingroup$
I have a related question at math.stackexchange.com/questions/3084683/…
$endgroup$
– Keefer Rowan
Jan 23 at 16:45
1
1
$begingroup$
Your analysis is OK, but I don't think it's a very fruitful topic for MSE for the same reasons as stated in David Roberts's comments on the MO question you link to.
$endgroup$
– Rob Arthan
Jan 23 at 21:38
$begingroup$
Your analysis is OK, but I don't think it's a very fruitful topic for MSE for the same reasons as stated in David Roberts's comments on the MO question you link to.
$endgroup$
– Rob Arthan
Jan 23 at 21:38
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Because we know the exact sentence $text{Con}(text{PA})$, we know that if (a) was false then (b) would also be false. Any counterexample to (a), if written down, would immediately lead to a counterexample to (b), that is, it would show $lnot text{Con}(text{PA})$.
The deeper issue in threads about "is PA consistent?" is whether that quoted question should be judged by the same standards as other mathematical knowledge, or whether there are somehow stronger standards that should be applied.
By normal mathematical standards of justification, the question "is PA consistent" is settled. But if we raise the burden of proof for that specific question high enough, we can make it impossible to settle.
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
$endgroup$
$begingroup$
While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont.
$endgroup$
– Keefer Rowan
Jan 24 at 19:36
$begingroup$
"contradiction?" is answerable. From a formalist perspective, we have a standard way of interpreting what it means for a given mathematical statement Y to be proven, that is: "In system X, there is a finite set of applications of logical rules to the axioms of System X that result in Y." Now if we ask the above question about the consistency of PA, it does not lend itself to being answered in the negative by some proof of a not provably consistent system. Perhaps then the above question about the consistency of PA is "unmathematical" in some sense.
$endgroup$
– Keefer Rowan
Jan 24 at 19:39
1
$begingroup$
When we ask whether a system proves Con(PA), as in (b), the question whether that system also proves ~Con(PA) is somewhat separate. But, as an example, it is not hard to find a system T so that T proves Con(PA) and ZFC proves T is consistent, which means that, by normal mathematical standards, we know "there is a consistent formal system T that proves Con(PA)". If that is what you take (b) to mean.
$endgroup$
– Carl Mummert
Jan 24 at 19:39
1
$begingroup$
On the other hand, because the consistency of formal systems that meet the hypotheses of the incompleteness theorems is never provable in those same systems, we will always need to appeal to some "stronger" system to prove the consistency of foundational theories. So if we look at natural foundational systems and we want to prove there is a consistent theory T that proves there is a consistent theory S that proves Con(PA), we can show that is true, but only in a system stronger than PA. We can make the chain of consistency proofs arbitrarily long.
$endgroup$
– Carl Mummert
Jan 24 at 19:42
$begingroup$
I agree with your comment, but, as I tried to make clear in my second comment you may not have seen yet, I am more concerned with "is there a finite set of applications of logical rules to the axioms of PA that lead to a contradiction?" to which (for what I think are fairly rational reasons) your above example of a proof of Cons(PA) is not a particularly satisfying resolution. Though certainly such a proof goes even beyond the standards of normal math. As such I am becoming more inclined to say my formation of the question is not mathematically answerable.
$endgroup$
– Keefer Rowan
Jan 24 at 19:43
|
show 2 more comments
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%2f3084104%2fconsistency-of-pa-from-a-formalist-perspective%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$
Because we know the exact sentence $text{Con}(text{PA})$, we know that if (a) was false then (b) would also be false. Any counterexample to (a), if written down, would immediately lead to a counterexample to (b), that is, it would show $lnot text{Con}(text{PA})$.
The deeper issue in threads about "is PA consistent?" is whether that quoted question should be judged by the same standards as other mathematical knowledge, or whether there are somehow stronger standards that should be applied.
By normal mathematical standards of justification, the question "is PA consistent" is settled. But if we raise the burden of proof for that specific question high enough, we can make it impossible to settle.
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
$endgroup$
$begingroup$
While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont.
$endgroup$
– Keefer Rowan
Jan 24 at 19:36
$begingroup$
"contradiction?" is answerable. From a formalist perspective, we have a standard way of interpreting what it means for a given mathematical statement Y to be proven, that is: "In system X, there is a finite set of applications of logical rules to the axioms of System X that result in Y." Now if we ask the above question about the consistency of PA, it does not lend itself to being answered in the negative by some proof of a not provably consistent system. Perhaps then the above question about the consistency of PA is "unmathematical" in some sense.
$endgroup$
– Keefer Rowan
Jan 24 at 19:39
1
$begingroup$
When we ask whether a system proves Con(PA), as in (b), the question whether that system also proves ~Con(PA) is somewhat separate. But, as an example, it is not hard to find a system T so that T proves Con(PA) and ZFC proves T is consistent, which means that, by normal mathematical standards, we know "there is a consistent formal system T that proves Con(PA)". If that is what you take (b) to mean.
$endgroup$
– Carl Mummert
Jan 24 at 19:39
1
$begingroup$
On the other hand, because the consistency of formal systems that meet the hypotheses of the incompleteness theorems is never provable in those same systems, we will always need to appeal to some "stronger" system to prove the consistency of foundational theories. So if we look at natural foundational systems and we want to prove there is a consistent theory T that proves there is a consistent theory S that proves Con(PA), we can show that is true, but only in a system stronger than PA. We can make the chain of consistency proofs arbitrarily long.
$endgroup$
– Carl Mummert
Jan 24 at 19:42
$begingroup$
I agree with your comment, but, as I tried to make clear in my second comment you may not have seen yet, I am more concerned with "is there a finite set of applications of logical rules to the axioms of PA that lead to a contradiction?" to which (for what I think are fairly rational reasons) your above example of a proof of Cons(PA) is not a particularly satisfying resolution. Though certainly such a proof goes even beyond the standards of normal math. As such I am becoming more inclined to say my formation of the question is not mathematically answerable.
$endgroup$
– Keefer Rowan
Jan 24 at 19:43
|
show 2 more comments
$begingroup$
Because we know the exact sentence $text{Con}(text{PA})$, we know that if (a) was false then (b) would also be false. Any counterexample to (a), if written down, would immediately lead to a counterexample to (b), that is, it would show $lnot text{Con}(text{PA})$.
The deeper issue in threads about "is PA consistent?" is whether that quoted question should be judged by the same standards as other mathematical knowledge, or whether there are somehow stronger standards that should be applied.
By normal mathematical standards of justification, the question "is PA consistent" is settled. But if we raise the burden of proof for that specific question high enough, we can make it impossible to settle.
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
$endgroup$
$begingroup$
While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont.
$endgroup$
– Keefer Rowan
Jan 24 at 19:36
$begingroup$
"contradiction?" is answerable. From a formalist perspective, we have a standard way of interpreting what it means for a given mathematical statement Y to be proven, that is: "In system X, there is a finite set of applications of logical rules to the axioms of System X that result in Y." Now if we ask the above question about the consistency of PA, it does not lend itself to being answered in the negative by some proof of a not provably consistent system. Perhaps then the above question about the consistency of PA is "unmathematical" in some sense.
$endgroup$
– Keefer Rowan
Jan 24 at 19:39
1
$begingroup$
When we ask whether a system proves Con(PA), as in (b), the question whether that system also proves ~Con(PA) is somewhat separate. But, as an example, it is not hard to find a system T so that T proves Con(PA) and ZFC proves T is consistent, which means that, by normal mathematical standards, we know "there is a consistent formal system T that proves Con(PA)". If that is what you take (b) to mean.
$endgroup$
– Carl Mummert
Jan 24 at 19:39
1
$begingroup$
On the other hand, because the consistency of formal systems that meet the hypotheses of the incompleteness theorems is never provable in those same systems, we will always need to appeal to some "stronger" system to prove the consistency of foundational theories. So if we look at natural foundational systems and we want to prove there is a consistent theory T that proves there is a consistent theory S that proves Con(PA), we can show that is true, but only in a system stronger than PA. We can make the chain of consistency proofs arbitrarily long.
$endgroup$
– Carl Mummert
Jan 24 at 19:42
$begingroup$
I agree with your comment, but, as I tried to make clear in my second comment you may not have seen yet, I am more concerned with "is there a finite set of applications of logical rules to the axioms of PA that lead to a contradiction?" to which (for what I think are fairly rational reasons) your above example of a proof of Cons(PA) is not a particularly satisfying resolution. Though certainly such a proof goes even beyond the standards of normal math. As such I am becoming more inclined to say my formation of the question is not mathematically answerable.
$endgroup$
– Keefer Rowan
Jan 24 at 19:43
|
show 2 more comments
$begingroup$
Because we know the exact sentence $text{Con}(text{PA})$, we know that if (a) was false then (b) would also be false. Any counterexample to (a), if written down, would immediately lead to a counterexample to (b), that is, it would show $lnot text{Con}(text{PA})$.
The deeper issue in threads about "is PA consistent?" is whether that quoted question should be judged by the same standards as other mathematical knowledge, or whether there are somehow stronger standards that should be applied.
By normal mathematical standards of justification, the question "is PA consistent" is settled. But if we raise the burden of proof for that specific question high enough, we can make it impossible to settle.
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
$endgroup$
Because we know the exact sentence $text{Con}(text{PA})$, we know that if (a) was false then (b) would also be false. Any counterexample to (a), if written down, would immediately lead to a counterexample to (b), that is, it would show $lnot text{Con}(text{PA})$.
The deeper issue in threads about "is PA consistent?" is whether that quoted question should be judged by the same standards as other mathematical knowledge, or whether there are somehow stronger standards that should be applied.
By normal mathematical standards of justification, the question "is PA consistent" is settled. But if we raise the burden of proof for that specific question high enough, we can make it impossible to settle.
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
edited Jan 24 at 19:24
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
answered Jan 24 at 19:16
Carl MummertCarl Mummert
67.2k7133251
67.2k7133251
$begingroup$
While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont.
$endgroup$
– Keefer Rowan
Jan 24 at 19:36
$begingroup$
"contradiction?" is answerable. From a formalist perspective, we have a standard way of interpreting what it means for a given mathematical statement Y to be proven, that is: "In system X, there is a finite set of applications of logical rules to the axioms of System X that result in Y." Now if we ask the above question about the consistency of PA, it does not lend itself to being answered in the negative by some proof of a not provably consistent system. Perhaps then the above question about the consistency of PA is "unmathematical" in some sense.
$endgroup$
– Keefer Rowan
Jan 24 at 19:39
1
$begingroup$
When we ask whether a system proves Con(PA), as in (b), the question whether that system also proves ~Con(PA) is somewhat separate. But, as an example, it is not hard to find a system T so that T proves Con(PA) and ZFC proves T is consistent, which means that, by normal mathematical standards, we know "there is a consistent formal system T that proves Con(PA)". If that is what you take (b) to mean.
$endgroup$
– Carl Mummert
Jan 24 at 19:39
1
$begingroup$
On the other hand, because the consistency of formal systems that meet the hypotheses of the incompleteness theorems is never provable in those same systems, we will always need to appeal to some "stronger" system to prove the consistency of foundational theories. So if we look at natural foundational systems and we want to prove there is a consistent theory T that proves there is a consistent theory S that proves Con(PA), we can show that is true, but only in a system stronger than PA. We can make the chain of consistency proofs arbitrarily long.
$endgroup$
– Carl Mummert
Jan 24 at 19:42
$begingroup$
I agree with your comment, but, as I tried to make clear in my second comment you may not have seen yet, I am more concerned with "is there a finite set of applications of logical rules to the axioms of PA that lead to a contradiction?" to which (for what I think are fairly rational reasons) your above example of a proof of Cons(PA) is not a particularly satisfying resolution. Though certainly such a proof goes even beyond the standards of normal math. As such I am becoming more inclined to say my formation of the question is not mathematically answerable.
$endgroup$
– Keefer Rowan
Jan 24 at 19:43
|
show 2 more comments
$begingroup$
While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont.
$endgroup$
– Keefer Rowan
Jan 24 at 19:36
$begingroup$
"contradiction?" is answerable. From a formalist perspective, we have a standard way of interpreting what it means for a given mathematical statement Y to be proven, that is: "In system X, there is a finite set of applications of logical rules to the axioms of System X that result in Y." Now if we ask the above question about the consistency of PA, it does not lend itself to being answered in the negative by some proof of a not provably consistent system. Perhaps then the above question about the consistency of PA is "unmathematical" in some sense.
$endgroup$
– Keefer Rowan
Jan 24 at 19:39
1
$begingroup$
When we ask whether a system proves Con(PA), as in (b), the question whether that system also proves ~Con(PA) is somewhat separate. But, as an example, it is not hard to find a system T so that T proves Con(PA) and ZFC proves T is consistent, which means that, by normal mathematical standards, we know "there is a consistent formal system T that proves Con(PA)". If that is what you take (b) to mean.
$endgroup$
– Carl Mummert
Jan 24 at 19:39
1
$begingroup$
On the other hand, because the consistency of formal systems that meet the hypotheses of the incompleteness theorems is never provable in those same systems, we will always need to appeal to some "stronger" system to prove the consistency of foundational theories. So if we look at natural foundational systems and we want to prove there is a consistent theory T that proves there is a consistent theory S that proves Con(PA), we can show that is true, but only in a system stronger than PA. We can make the chain of consistency proofs arbitrarily long.
$endgroup$
– Carl Mummert
Jan 24 at 19:42
$begingroup$
I agree with your comment, but, as I tried to make clear in my second comment you may not have seen yet, I am more concerned with "is there a finite set of applications of logical rules to the axioms of PA that lead to a contradiction?" to which (for what I think are fairly rational reasons) your above example of a proof of Cons(PA) is not a particularly satisfying resolution. Though certainly such a proof goes even beyond the standards of normal math. As such I am becoming more inclined to say my formation of the question is not mathematically answerable.
$endgroup$
– Keefer Rowan
Jan 24 at 19:43
$begingroup$
While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont.
$endgroup$
– Keefer Rowan
Jan 24 at 19:36
$begingroup$
While I agree that if (a) is false then (b) is false, but strangely enough even if (b) is true (by normal standards of truth, that Cons(PA) is provable in some System X), (a) could be false. That is because both systems could be inconsistent so, (a) could be false, that is there is some derivation of an inconsistency in PA, and Cons(PA) could be provable in System X, because if System X is inconsistent, then $neg$Cons(PA) and Cons(PA) are both provable. That is why I'm not sure if the question "is there a finite set of applications of logical rules to the axioms of PA that lead to a..." cont.
$endgroup$
– Keefer Rowan
Jan 24 at 19:36
$begingroup$
"contradiction?" is answerable. From a formalist perspective, we have a standard way of interpreting what it means for a given mathematical statement Y to be proven, that is: "In system X, there is a finite set of applications of logical rules to the axioms of System X that result in Y." Now if we ask the above question about the consistency of PA, it does not lend itself to being answered in the negative by some proof of a not provably consistent system. Perhaps then the above question about the consistency of PA is "unmathematical" in some sense.
$endgroup$
– Keefer Rowan
Jan 24 at 19:39
$begingroup$
"contradiction?" is answerable. From a formalist perspective, we have a standard way of interpreting what it means for a given mathematical statement Y to be proven, that is: "In system X, there is a finite set of applications of logical rules to the axioms of System X that result in Y." Now if we ask the above question about the consistency of PA, it does not lend itself to being answered in the negative by some proof of a not provably consistent system. Perhaps then the above question about the consistency of PA is "unmathematical" in some sense.
$endgroup$
– Keefer Rowan
Jan 24 at 19:39
1
1
$begingroup$
When we ask whether a system proves Con(PA), as in (b), the question whether that system also proves ~Con(PA) is somewhat separate. But, as an example, it is not hard to find a system T so that T proves Con(PA) and ZFC proves T is consistent, which means that, by normal mathematical standards, we know "there is a consistent formal system T that proves Con(PA)". If that is what you take (b) to mean.
$endgroup$
– Carl Mummert
Jan 24 at 19:39
$begingroup$
When we ask whether a system proves Con(PA), as in (b), the question whether that system also proves ~Con(PA) is somewhat separate. But, as an example, it is not hard to find a system T so that T proves Con(PA) and ZFC proves T is consistent, which means that, by normal mathematical standards, we know "there is a consistent formal system T that proves Con(PA)". If that is what you take (b) to mean.
$endgroup$
– Carl Mummert
Jan 24 at 19:39
1
1
$begingroup$
On the other hand, because the consistency of formal systems that meet the hypotheses of the incompleteness theorems is never provable in those same systems, we will always need to appeal to some "stronger" system to prove the consistency of foundational theories. So if we look at natural foundational systems and we want to prove there is a consistent theory T that proves there is a consistent theory S that proves Con(PA), we can show that is true, but only in a system stronger than PA. We can make the chain of consistency proofs arbitrarily long.
$endgroup$
– Carl Mummert
Jan 24 at 19:42
$begingroup$
On the other hand, because the consistency of formal systems that meet the hypotheses of the incompleteness theorems is never provable in those same systems, we will always need to appeal to some "stronger" system to prove the consistency of foundational theories. So if we look at natural foundational systems and we want to prove there is a consistent theory T that proves there is a consistent theory S that proves Con(PA), we can show that is true, but only in a system stronger than PA. We can make the chain of consistency proofs arbitrarily long.
$endgroup$
– Carl Mummert
Jan 24 at 19:42
$begingroup$
I agree with your comment, but, as I tried to make clear in my second comment you may not have seen yet, I am more concerned with "is there a finite set of applications of logical rules to the axioms of PA that lead to a contradiction?" to which (for what I think are fairly rational reasons) your above example of a proof of Cons(PA) is not a particularly satisfying resolution. Though certainly such a proof goes even beyond the standards of normal math. As such I am becoming more inclined to say my formation of the question is not mathematically answerable.
$endgroup$
– Keefer Rowan
Jan 24 at 19:43
$begingroup$
I agree with your comment, but, as I tried to make clear in my second comment you may not have seen yet, I am more concerned with "is there a finite set of applications of logical rules to the axioms of PA that lead to a contradiction?" to which (for what I think are fairly rational reasons) your above example of a proof of Cons(PA) is not a particularly satisfying resolution. Though certainly such a proof goes even beyond the standards of normal math. As such I am becoming more inclined to say my formation of the question is not mathematically answerable.
$endgroup$
– Keefer Rowan
Jan 24 at 19:43
|
show 2 more comments
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%2f3084104%2fconsistency-of-pa-from-a-formalist-perspective%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$
Note for (b), if ¬CON(A) then A⊦CON(PA), also if CON(A), then for A⊦CON(PA) to be true, A need to be the stronger system.
$endgroup$
– Holo
Jan 23 at 10:01
$begingroup$
I have a related question at math.stackexchange.com/questions/3084683/…
$endgroup$
– Keefer Rowan
Jan 23 at 16:45
1
$begingroup$
Your analysis is OK, but I don't think it's a very fruitful topic for MSE for the same reasons as stated in David Roberts's comments on the MO question you link to.
$endgroup$
– Rob Arthan
Jan 23 at 21:38