“Contradiction” in Constructive Mathematics
$begingroup$
I’m watching this video on Constructive Mathematics Five Stages of Accepting Constructive Mathematics, and Andrej Bauer makes the following claim:
Mathematicians call two different things “Proof by Contradiction”. One is assume not p, blah blah blah contradiction. Therefore p. The other is assume p, blah blah blah contradiction. Therefore not p. The first is not constructively valid, but the second is. The second is how you prove negation.
I’m confused why the latter is constructively valid. Aren’t the two statements dual to each other in some sense, even constructively speaking? Perhaps I’m confused about proving negation.
soft-question constructive-mathematics
$endgroup$
add a comment |
$begingroup$
I’m watching this video on Constructive Mathematics Five Stages of Accepting Constructive Mathematics, and Andrej Bauer makes the following claim:
Mathematicians call two different things “Proof by Contradiction”. One is assume not p, blah blah blah contradiction. Therefore p. The other is assume p, blah blah blah contradiction. Therefore not p. The first is not constructively valid, but the second is. The second is how you prove negation.
I’m confused why the latter is constructively valid. Aren’t the two statements dual to each other in some sense, even constructively speaking? Perhaps I’m confused about proving negation.
soft-question constructive-mathematics
$endgroup$
1
$begingroup$
Note that saying 'assume $neg p$, blah blah, contradiction' is still a fine argument - but what it proves is $neg neg p$, and in constructive mathematics you can't infer $p$ from $neg neg p$.
$endgroup$
– Steven Stadnicki
1 hour ago
add a comment |
$begingroup$
I’m watching this video on Constructive Mathematics Five Stages of Accepting Constructive Mathematics, and Andrej Bauer makes the following claim:
Mathematicians call two different things “Proof by Contradiction”. One is assume not p, blah blah blah contradiction. Therefore p. The other is assume p, blah blah blah contradiction. Therefore not p. The first is not constructively valid, but the second is. The second is how you prove negation.
I’m confused why the latter is constructively valid. Aren’t the two statements dual to each other in some sense, even constructively speaking? Perhaps I’m confused about proving negation.
soft-question constructive-mathematics
$endgroup$
I’m watching this video on Constructive Mathematics Five Stages of Accepting Constructive Mathematics, and Andrej Bauer makes the following claim:
Mathematicians call two different things “Proof by Contradiction”. One is assume not p, blah blah blah contradiction. Therefore p. The other is assume p, blah blah blah contradiction. Therefore not p. The first is not constructively valid, but the second is. The second is how you prove negation.
I’m confused why the latter is constructively valid. Aren’t the two statements dual to each other in some sense, even constructively speaking? Perhaps I’m confused about proving negation.
soft-question constructive-mathematics
soft-question constructive-mathematics
asked 2 hours ago
user458276user458276
39929
39929
1
$begingroup$
Note that saying 'assume $neg p$, blah blah, contradiction' is still a fine argument - but what it proves is $neg neg p$, and in constructive mathematics you can't infer $p$ from $neg neg p$.
$endgroup$
– Steven Stadnicki
1 hour ago
add a comment |
1
$begingroup$
Note that saying 'assume $neg p$, blah blah, contradiction' is still a fine argument - but what it proves is $neg neg p$, and in constructive mathematics you can't infer $p$ from $neg neg p$.
$endgroup$
– Steven Stadnicki
1 hour ago
1
1
$begingroup$
Note that saying 'assume $neg p$, blah blah, contradiction' is still a fine argument - but what it proves is $neg neg p$, and in constructive mathematics you can't infer $p$ from $neg neg p$.
$endgroup$
– Steven Stadnicki
1 hour ago
$begingroup$
Note that saying 'assume $neg p$, blah blah, contradiction' is still a fine argument - but what it proves is $neg neg p$, and in constructive mathematics you can't infer $p$ from $neg neg p$.
$endgroup$
– Steven Stadnicki
1 hour ago
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
One rule is negation-introduction; that is "If we derive a contradiction under an assumption, then we may infer that the premises entail the negation of the assumption." This is a "Proof of Negation". $$begin{split}Gamma, p&vdash bot\hlineGamma&vdashlnot pend{split}tag {1, $lnot$i}$$
Well, what if we derive a contradiction when we assume a negation? Applying this rule we would infer that the premises entail the negation of that negation; ie a 'double negation'. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdashlnotlnot pend{split}tag 2$$
This is all intuitionistically valid. The difference between intuitionistic (contructive) and classical logic is the rule of double-negation-elimination (DNE), is only admissible under the later; it says "if we can derive a double negation of a proposition we may infer that we can derive the proposition." $$begin{split}Gamma &vdash lnotlnot p\hlineGamma&vdash pend{split}tag {3, DNE}$$
Putting (2) and (3) together and we have "Proof by Reduction to Absurdity", and this is why it is not intuitionistically valid. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdash pend{split}tag{4, RAA}$$
$endgroup$
add a comment |
$begingroup$
The second is how you prove negation.
When you are proving "not $A$", you are proving "if $A$, then contradiction", because this is literally how "not $A$" is defined in constructive logic.
When you are proving "$A$", it does not suffice to prove "if not $A$, then contradiction", because $A$ is not defined this way (that would be circular!) and there is no general rule that tells you that "if not $A$, then contradiction" implies $A$. There are situations when this does hold (for example, if $A$ is computable -- i.e., there exists a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$), but these are theorems that have to be proven rather than consequences of a general axiom like TND. (For example, when $A$ is computable -- i.e., when you know a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$ -- you can prove $A$ by proving "if not $A$, then contradiction" -- but the reason why this works is simply that you can distinguish cases based upon whether $a = operatorname{True}$ or $a = operatorname{False}$. So, on the level of axioms, you are not using TND, but rather emulating a "proof by contradiction" by inducting (= distinguishing cases) upon a boolean. If you don't know such a boolean $a$, then this trick does not work.)
Yes, these situations are dual in a sense, but "dual" does not mean "equally true" in mathematics. Even in classical mathematics. For example, a basis of a vector space may have any cardinality, but a basis of a dual of a vector space may not :)
$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%2f3104606%2fcontradiction-in-constructive-mathematics%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
One rule is negation-introduction; that is "If we derive a contradiction under an assumption, then we may infer that the premises entail the negation of the assumption." This is a "Proof of Negation". $$begin{split}Gamma, p&vdash bot\hlineGamma&vdashlnot pend{split}tag {1, $lnot$i}$$
Well, what if we derive a contradiction when we assume a negation? Applying this rule we would infer that the premises entail the negation of that negation; ie a 'double negation'. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdashlnotlnot pend{split}tag 2$$
This is all intuitionistically valid. The difference between intuitionistic (contructive) and classical logic is the rule of double-negation-elimination (DNE), is only admissible under the later; it says "if we can derive a double negation of a proposition we may infer that we can derive the proposition." $$begin{split}Gamma &vdash lnotlnot p\hlineGamma&vdash pend{split}tag {3, DNE}$$
Putting (2) and (3) together and we have "Proof by Reduction to Absurdity", and this is why it is not intuitionistically valid. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdash pend{split}tag{4, RAA}$$
$endgroup$
add a comment |
$begingroup$
One rule is negation-introduction; that is "If we derive a contradiction under an assumption, then we may infer that the premises entail the negation of the assumption." This is a "Proof of Negation". $$begin{split}Gamma, p&vdash bot\hlineGamma&vdashlnot pend{split}tag {1, $lnot$i}$$
Well, what if we derive a contradiction when we assume a negation? Applying this rule we would infer that the premises entail the negation of that negation; ie a 'double negation'. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdashlnotlnot pend{split}tag 2$$
This is all intuitionistically valid. The difference between intuitionistic (contructive) and classical logic is the rule of double-negation-elimination (DNE), is only admissible under the later; it says "if we can derive a double negation of a proposition we may infer that we can derive the proposition." $$begin{split}Gamma &vdash lnotlnot p\hlineGamma&vdash pend{split}tag {3, DNE}$$
Putting (2) and (3) together and we have "Proof by Reduction to Absurdity", and this is why it is not intuitionistically valid. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdash pend{split}tag{4, RAA}$$
$endgroup$
add a comment |
$begingroup$
One rule is negation-introduction; that is "If we derive a contradiction under an assumption, then we may infer that the premises entail the negation of the assumption." This is a "Proof of Negation". $$begin{split}Gamma, p&vdash bot\hlineGamma&vdashlnot pend{split}tag {1, $lnot$i}$$
Well, what if we derive a contradiction when we assume a negation? Applying this rule we would infer that the premises entail the negation of that negation; ie a 'double negation'. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdashlnotlnot pend{split}tag 2$$
This is all intuitionistically valid. The difference between intuitionistic (contructive) and classical logic is the rule of double-negation-elimination (DNE), is only admissible under the later; it says "if we can derive a double negation of a proposition we may infer that we can derive the proposition." $$begin{split}Gamma &vdash lnotlnot p\hlineGamma&vdash pend{split}tag {3, DNE}$$
Putting (2) and (3) together and we have "Proof by Reduction to Absurdity", and this is why it is not intuitionistically valid. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdash pend{split}tag{4, RAA}$$
$endgroup$
One rule is negation-introduction; that is "If we derive a contradiction under an assumption, then we may infer that the premises entail the negation of the assumption." This is a "Proof of Negation". $$begin{split}Gamma, p&vdash bot\hlineGamma&vdashlnot pend{split}tag {1, $lnot$i}$$
Well, what if we derive a contradiction when we assume a negation? Applying this rule we would infer that the premises entail the negation of that negation; ie a 'double negation'. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdashlnotlnot pend{split}tag 2$$
This is all intuitionistically valid. The difference between intuitionistic (contructive) and classical logic is the rule of double-negation-elimination (DNE), is only admissible under the later; it says "if we can derive a double negation of a proposition we may infer that we can derive the proposition." $$begin{split}Gamma &vdash lnotlnot p\hlineGamma&vdash pend{split}tag {3, DNE}$$
Putting (2) and (3) together and we have "Proof by Reduction to Absurdity", and this is why it is not intuitionistically valid. $$begin{split}Gamma, lnot p&vdash bot\hlineGamma&vdash pend{split}tag{4, RAA}$$
answered 1 hour ago
Graham KempGraham Kemp
85.6k43378
85.6k43378
add a comment |
add a comment |
$begingroup$
The second is how you prove negation.
When you are proving "not $A$", you are proving "if $A$, then contradiction", because this is literally how "not $A$" is defined in constructive logic.
When you are proving "$A$", it does not suffice to prove "if not $A$, then contradiction", because $A$ is not defined this way (that would be circular!) and there is no general rule that tells you that "if not $A$, then contradiction" implies $A$. There are situations when this does hold (for example, if $A$ is computable -- i.e., there exists a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$), but these are theorems that have to be proven rather than consequences of a general axiom like TND. (For example, when $A$ is computable -- i.e., when you know a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$ -- you can prove $A$ by proving "if not $A$, then contradiction" -- but the reason why this works is simply that you can distinguish cases based upon whether $a = operatorname{True}$ or $a = operatorname{False}$. So, on the level of axioms, you are not using TND, but rather emulating a "proof by contradiction" by inducting (= distinguishing cases) upon a boolean. If you don't know such a boolean $a$, then this trick does not work.)
Yes, these situations are dual in a sense, but "dual" does not mean "equally true" in mathematics. Even in classical mathematics. For example, a basis of a vector space may have any cardinality, but a basis of a dual of a vector space may not :)
$endgroup$
add a comment |
$begingroup$
The second is how you prove negation.
When you are proving "not $A$", you are proving "if $A$, then contradiction", because this is literally how "not $A$" is defined in constructive logic.
When you are proving "$A$", it does not suffice to prove "if not $A$, then contradiction", because $A$ is not defined this way (that would be circular!) and there is no general rule that tells you that "if not $A$, then contradiction" implies $A$. There are situations when this does hold (for example, if $A$ is computable -- i.e., there exists a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$), but these are theorems that have to be proven rather than consequences of a general axiom like TND. (For example, when $A$ is computable -- i.e., when you know a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$ -- you can prove $A$ by proving "if not $A$, then contradiction" -- but the reason why this works is simply that you can distinguish cases based upon whether $a = operatorname{True}$ or $a = operatorname{False}$. So, on the level of axioms, you are not using TND, but rather emulating a "proof by contradiction" by inducting (= distinguishing cases) upon a boolean. If you don't know such a boolean $a$, then this trick does not work.)
Yes, these situations are dual in a sense, but "dual" does not mean "equally true" in mathematics. Even in classical mathematics. For example, a basis of a vector space may have any cardinality, but a basis of a dual of a vector space may not :)
$endgroup$
add a comment |
$begingroup$
The second is how you prove negation.
When you are proving "not $A$", you are proving "if $A$, then contradiction", because this is literally how "not $A$" is defined in constructive logic.
When you are proving "$A$", it does not suffice to prove "if not $A$, then contradiction", because $A$ is not defined this way (that would be circular!) and there is no general rule that tells you that "if not $A$, then contradiction" implies $A$. There are situations when this does hold (for example, if $A$ is computable -- i.e., there exists a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$), but these are theorems that have to be proven rather than consequences of a general axiom like TND. (For example, when $A$ is computable -- i.e., when you know a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$ -- you can prove $A$ by proving "if not $A$, then contradiction" -- but the reason why this works is simply that you can distinguish cases based upon whether $a = operatorname{True}$ or $a = operatorname{False}$. So, on the level of axioms, you are not using TND, but rather emulating a "proof by contradiction" by inducting (= distinguishing cases) upon a boolean. If you don't know such a boolean $a$, then this trick does not work.)
Yes, these situations are dual in a sense, but "dual" does not mean "equally true" in mathematics. Even in classical mathematics. For example, a basis of a vector space may have any cardinality, but a basis of a dual of a vector space may not :)
$endgroup$
The second is how you prove negation.
When you are proving "not $A$", you are proving "if $A$, then contradiction", because this is literally how "not $A$" is defined in constructive logic.
When you are proving "$A$", it does not suffice to prove "if not $A$, then contradiction", because $A$ is not defined this way (that would be circular!) and there is no general rule that tells you that "if not $A$, then contradiction" implies $A$. There are situations when this does hold (for example, if $A$ is computable -- i.e., there exists a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$), but these are theorems that have to be proven rather than consequences of a general axiom like TND. (For example, when $A$ is computable -- i.e., when you know a boolean $a in left{operatorname{True}, operatorname{False}right}$ such that $A Longleftrightarrow left(a = operatorname{True} right)$ -- you can prove $A$ by proving "if not $A$, then contradiction" -- but the reason why this works is simply that you can distinguish cases based upon whether $a = operatorname{True}$ or $a = operatorname{False}$. So, on the level of axioms, you are not using TND, but rather emulating a "proof by contradiction" by inducting (= distinguishing cases) upon a boolean. If you don't know such a boolean $a$, then this trick does not work.)
Yes, these situations are dual in a sense, but "dual" does not mean "equally true" in mathematics. Even in classical mathematics. For example, a basis of a vector space may have any cardinality, but a basis of a dual of a vector space may not :)
edited 1 hour ago
answered 1 hour ago
darij grinbergdarij grinberg
10.9k33163
10.9k33163
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%2f3104606%2fcontradiction-in-constructive-mathematics%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
1
$begingroup$
Note that saying 'assume $neg p$, blah blah, contradiction' is still a fine argument - but what it proves is $neg neg p$, and in constructive mathematics you can't infer $p$ from $neg neg p$.
$endgroup$
– Steven Stadnicki
1 hour ago