Mixing
Why, logically, is proof by contradiction valid?
How does proof by contradiction work logically?
Normally in a proof we might have a true premise leading to a true conclusion, i.e. it is true that $T rightarrow T$.
But then how does proof by contradiction work? We assume the premise is false and then the goal is to what, show $F rightarrow F$? Or $F rightarrow T$? (both of which are true?)
Like what exactly is the logical mechanism underneath all this that lets proofs work as well as proof by contradiction?
logic proof-writing definition boolean-algebra
asked Mar 22 '18 at 23:37
user525966
1,994921
|
show 3 more comments
How does proof by contradiction work logically?
Normally in a proof we might have a true premise leading to a true conclusion, i.e. it is true that $T rightarrow T$.
But then how does proof by contradiction work? We assume the premise is false and then the goal is to what, show $F rightarrow F$? Or $F rightarrow T$? (both of which are true?)
Like what exactly is the logical mechanism underneath all this that lets proofs work as well as proof by contradiction?
logic proof-writing definition boolean-algebra
asked Mar 22 '18 at 23:37
user525966
1,994921
8
Either a theorem is true or it is false. Truth by contradiction eliminates one of those alternatives.
– David G. Stork
Mar 22 '18 at 23:40
4
No, we assume the premise is true and if it leads to false it means the premise is false and the opposite of false is true.
– Vasya
Mar 22 '18 at 23:42
Possible duplicate: math.stackexchange.com/questions/2431003/…
– user477343
Mar 23 '18 at 0:20
2
"Works logically" depends on the proof system you are using.
– Graham Kemp
Mar 23 '18 at 0:36
I think the struggle to accept this type of proof isn't so much the system of logic, but a quirk of its application. In J. P. Serre's words "A proof by contradiction is the only proof where when you make a mistake it helps you."
– Algeboy
Mar 23 '18 at 2:55
|
show 3 more comments
How does proof by contradiction work logically?
Normally in a proof we might have a true premise leading to a true conclusion, i.e. it is true that $T rightarrow T$.
But then how does proof by contradiction work? We assume the premise is false and then the goal is to what, show $F rightarrow F$? Or $F rightarrow T$? (both of which are true?)
Like what exactly is the logical mechanism underneath all this that lets proofs work as well as proof by contradiction?
logic proof-writing definition boolean-algebra
asked Mar 22 '18 at 23:37
user525966
1,994921
How does proof by contradiction work logically?
Normally in a proof we might have a true premise leading to a true conclusion, i.e. it is true that $T rightarrow T$.
But then how does proof by contradiction work? We assume the premise is false and then the goal is to what, show $F rightarrow F$? Or $F rightarrow T$? (both of which are true?)
Like what exactly is the logical mechanism underneath all this that lets proofs work as well as proof by contradiction?
logic proof-writing definition boolean-algebra
logic proof-writing definition boolean-algebra
asked Mar 22 '18 at 23:37
user525966
1,994921
asked Mar 22 '18 at 23:37
user525966
1,994921
asked Mar 22 '18 at 23:37
user525966
1,994921
asked Mar 22 '18 at 23:37
user525966
1,994921
asked Mar 22 '18 at 23:37
user525966
1,994921
1,994921
8
Either a theorem is true or it is false. Truth by contradiction eliminates one of those alternatives.
– David G. Stork
Mar 22 '18 at 23:40
4
No, we assume the premise is true and if it leads to false it means the premise is false and the opposite of false is true.
– Vasya
Mar 22 '18 at 23:42
Possible duplicate: math.stackexchange.com/questions/2431003/…
– user477343
Mar 23 '18 at 0:20
2
"Works logically" depends on the proof system you are using.
– Graham Kemp
Mar 23 '18 at 0:36
I think the struggle to accept this type of proof isn't so much the system of logic, but a quirk of its application. In J. P. Serre's words "A proof by contradiction is the only proof where when you make a mistake it helps you."
– Algeboy
Mar 23 '18 at 2:55
|
show 3 more comments
8
Either a theorem is true or it is false. Truth by contradiction eliminates one of those alternatives.
– David G. Stork
Mar 22 '18 at 23:40
4
No, we assume the premise is true and if it leads to false it means the premise is false and the opposite of false is true.
– Vasya
Mar 22 '18 at 23:42
Possible duplicate: math.stackexchange.com/questions/2431003/…
– user477343
Mar 23 '18 at 0:20
2
"Works logically" depends on the proof system you are using.
– Graham Kemp
Mar 23 '18 at 0:36
I think the struggle to accept this type of proof isn't so much the system of logic, but a quirk of its application. In J. P. Serre's words "A proof by contradiction is the only proof where when you make a mistake it helps you."
– Algeboy
Mar 23 '18 at 2:55
8
8
Either a theorem is true or it is false. Truth by contradiction eliminates one of those alternatives.
– David G. Stork
Mar 22 '18 at 23:40
Either a theorem is true or it is false. Truth by contradiction eliminates one of those alternatives.
– David G. Stork
Mar 22 '18 at 23:40
4
4
No, we assume the premise is true and if it leads to false it means the premise is false and the opposite of false is true.
– Vasya
Mar 22 '18 at 23:42
No, we assume the premise is true and if it leads to false it means the premise is false and the opposite of false is true.
– Vasya
Mar 22 '18 at 23:42
Possible duplicate: math.stackexchange.com/questions/2431003/…
– user477343
Mar 23 '18 at 0:20
Possible duplicate: math.stackexchange.com/questions/2431003/…
– user477343
Mar 23 '18 at 0:20
2
2
"Works logically" depends on the proof system you are using.
– Graham Kemp
Mar 23 '18 at 0:36
"Works logically" depends on the proof system you are using.
– Graham Kemp
Mar 23 '18 at 0:36
I think the struggle to accept this type of proof isn't so much the system of logic, but a quirk of its application. In J. P. Serre's words "A proof by contradiction is the only proof where when you make a mistake it helps you."
– Algeboy
Mar 23 '18 at 2:55
I think the struggle to accept this type of proof isn't so much the system of logic, but a quirk of its application. In J. P. Serre's words "A proof by contradiction is the only proof where when you make a mistake it helps you."
– Algeboy
Mar 23 '18 at 2:55
|
show 3 more comments
4 Answers
4
active
oldest
votes
Yes, well, a proof by contradiction involves two rules of inference.
$$begin{split}text{Negation introduction}quad&quad (rimplies q) text{ and } (rimplies neg q), text{ infers } neg r\text{Double Negation elimination:}quad &quad negneg ptext{ infers } pend{split}$$
(1) the "Negation introduction" rule of inference argues that if something implies a contradiction then it must be false, since we usually assert that contradictions are not true and so cannot be infered by true things.
This is acceptable in both intuitionistic and classical logic systems. Although there are other systems (such as minimal logic) which do not accept this.
($deffalse{mathsf F}deftrue{mathsf T}$Semantically, this is because $false to false$ is true while $truetofalse$ is false. This leads some systems to define negation as $neg phi ~equiv~ phitomathsf F$ .)
(2) the "Double negation elimination" rule is that if the negation of a premise is false, then the premise must be true. This is not accepted in intuitionistic logic, but it is in classical logic.
(3) Combining these rules give the schema for a proof by contradiction: assume a negation of a predicate, demonstrate that infers a contradiction, thereby deducing that the predicate is true.
$$begin{split}text{Proof by Contradiction}quad&quad (neg p implies q) text{ and }(neg pimplies neg q) text{, infers }pend{split}$$
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
What is ⊢? Or ϕ? Why fractions?
– user525966
Mar 23 '18 at 1:18
The turnstyle, $vdash$, stands for "derivable". $phi, p, q, r$ are predicates. The proof tree displays the form of the rule. $neg r$ is infered when $q$ and $neg q$ are both derivable from $r$. $$dfrac{rvdash qquad rvdash neg q}{vdash neg r}{small negmathsf I}$$
– Graham Kemp
Mar 23 '18 at 2:01
What is the extra not-line thing on the far right?
– user525966
Mar 23 '18 at 2:08
1
Is this saying "When $q$ is provable from $r$, and $lnot q$ is also provable from $r$, then we conclude that $lnot r$ is provable from these premises"?
– user525966
Mar 23 '18 at 2:09
Maybe I should reedit.
– Graham Kemp
Mar 23 '18 at 2:19
|
show 4 more comments
Many of the issues I described here are on display in this Q&A.
First, let's be clear about what we're talking about. There are two rules that are often called "proof by contradiction". The first, negation introduction, can be written like $cfrac{varphivdashbot}{vdashnegvarphi}$ which can be read as "if we can derive that $varphi$ entails falsity, then we can derive $negvarphi$". We could also write this as an axiom: $(varphiRightarrowbot)Rightarrownegvarphi$. For some reason, this is how Bram28 has taken your statement, but I don't think you have an issue with this. You'd say, "well clearly if assuming $varphi$ leads to a contradiction then $varphi$ must have been false and thus $negvarphi$ is true". There's another rule, more appropriately called "proof by contradiction", that can be written $cfrac{negvarphivdashbot}{vdashvarphi}$ or as an axiom $(negvarphiRightarrowbot)Rightarrowvarphi$. These seems to be what you are taking issue with. Seeing as this latter rule has been rejected by many mathematicians (constructivists of various sorts), you wouldn't be completely crazy to question it. (In weak defense of Bram28, you'd probably accept "by substituting $negpsi$ into the above, by the same argument we can show that $negpsi$ is false so $psi$ is true", but the rule only shows that $negnegpsi$ is true. The rule allowing you to go from $negnegpsi$ to $psi$ is, in fact, equivalent to proof by contradiction.)
To be even more clear about what we're talking about we need to distinguish syntax from semantics. If we're talking about "rules of inference" or "proofs", we are usually thinking syntactically. That is, we're thinking about symbols on a page and rules for manipulating those collections of symbols into other collections of symbols or rules about what constitutes "correct" arrangements of the symbols, i.e. a proof. (More informal renditions will be sentences in a natural language that follow "rules of reason", but the idea is still that the form of the argument is what makes it valid.) Semantics, on the other hand, interprets those symbols as mathematical objects and then we say a formula (i.e. arrangement of symbols) is "true" if it is interpreted into a mathematical object satisfying some given property. For example, we say a formula of classical propositional logic is "true" if its interpretation as a Boolean function is the constantly $1$ function.
So, we have two possible readings of your question: 1) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ derivable? 2) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ "true"?
For (1), one very unsatisfying answer is that it is often taken as given, i.e. it is derivable by definition of the logic. A slightly more satisfying answer is the following. Given a constructive logic where that rule isn't derivable but most other "usual" rules are, we can show that if for all formulas $varphi$, $vdashvarphilornegvarphi$ is derivable, then we can derive the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ (and vice versa). Another way of saying this is that $varphilornegvarphi$ is provably equivalent to $(negvarphiRightarrowbot)Rightarrowvarphi$. It is also provably equivalent to $negnegvarphiRightarrowvarphi$. The axiom $varphilornegvarphi$ is often described as "everything is either true or false". This isn't quite what it means, but this idea of everything being "either true or false" is often considered intuitively obvious. However, there is no question of whether $varphi$ is "true" or "false" in the above. We have rules for building proofs from other proofs, and that's all there is to this perspective.
For (2), if you use the "truth table" semantics of classical propositional logic, then you simply calculate. You simply need to show that $(negvarphiRightarrowbot)Rightarrowvarphi$ when interpreted is the constantly $1$ function when both $0$ and $1$ are substituted in the interpretation of the formula. You can easily show this. In these semantics, "proof by contradiction" is simply "true". To question this requires questioning the semantics. One thing is to question whether there are only two truth values, $0$ and $1$. Why not three or an infinite number of them? This leads to multi-valued logics. Alternatively, we could keep the truth values the same, but interpret formulas as something other than Boolean functions. For example, we could say they are Boolean functions but we only allow monotonic ones, or we could say that they are total Boolean relations. Making these changes requires adapting the notion of "true". For the latter example, we may say a formula is "true" if it is interpreted as a relation which relates all Boolean inputs to $1$. Being a relation and not just a function, though, this does not stop it from also relating some or all of the inputs to $0$, i.e. something can be both "true" and "false".
Changing the semantics affects which rules and axioms are sound. A rule or axiom is sound with respect to a given semantics, if its interpretation is "true" in that semantics. $(negvarphiRightarrowbot)Rightarrowvarphi$ is sound with respect to "truth tables" but not with respect to many other possible semantics.
To summarize, if you're working with respect to "truth table" semantics, then "proof by contradiction" is simply "true", that is when interpreted it is interpreted as a constantly "true" Boolean function, and this can be easily calculated. In this case, all of your "logical assumptions" are built into the notion of "truth table" semantics. With respect to semantics, "proof" is irrelevant. Proof is a syntactic concept. Your discussion about "assuming the premise is false" is (slightly mangled) proof-theoretic talk. With a semantic approach, there is no "assuming the premise is true/false", either the formula interprets as "true" (i.e. a constantly $1$ function) or it doesn't. (You can have meta-logical assumptions that some formula is "true", but this is happening outside of the logic. Ultimately the coin of the mathematical realm is the more syntactic notion of proof and semantics just pushes proof to the meta-logic.)
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
So,for proof by contradiction, law of excluded middle(LEM) is the "connecting link" between the syntax(proof process) and the binary-logic-truth-table(BLTT) semantics. Because the syntactics "just happens to" support the defining property of BLTT semantics(i.e.LEM) 'syntactically' i.e. derivable** AND the interpretation(achieved via axioms/rule i.e. syntactics) in BLTT semantics is "true",this makes syntactics sound,and things work out. 1 Was syntactical property of LEM accidentally or deliberately added to syntactics?Perhaps it is a loop then! 2 **So truth has syntactic constraints?
– Ajax
Nov 21 '18 at 9:31
LEM is not the "defining property" of truth table semantics. The intuitive idea that "everything is either true or false" idea is a major motivation for truth table semantics. As I alluded to in the answer, LEM does not say that everything is either true or false. Consider ${0,1}^2$ with operations defined component-wise. This semantics validates LEM, but $(0,1)$ is neither true, $(1,1)$, nor false, $(0,0)$.
– Derek Elkins
Nov 21 '18 at 21:02
As an axiom (schema), LEM is simply part of a definition of a proof system for classical propositional logic. If you have the rules of intuitionistic propositional logic and you add LEM, you can derive proof by contradiction. This doesn't require any semantics to even be defined, so LEM certainly isn't a "connecting link" between syntax and semantics.
– Derek Elkins
Nov 21 '18 at 21:02
I don't get why are you able to derive the syntax formula which clearly tells the story of what LEM is? More importantly why is your (derived) formula (1) telling me about LEM? Why is syntax indicating what it is talking about?
– Ajax
Nov 21 '18 at 21:45
add a comment |
It works as follows:
Say you have some set of statements $Gamma$, and we want to infer $neg phi$, and we do this by a proof by contradiction.
Thus, we assume $phi$, and show that that leads to a contradiction.
This means that $Gamma$, together with $phi$ logically implies a contradiction, i.e.
$$Gamma cup phi vDash bot$$
and that means that is impossible to set all of the statements in $Gamma cup phi$ to true. But that then also means that if all statements in $Gamma$ are true, $phi$ will have to be false, i.e. $neg phi$ will have to be true. And thus we have
$$Gamma vDash neg phi$$
Thus, in effect, we have proven $neg phi$
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
What is ϕ? Or ⊨?
– user525966
Mar 23 '18 at 1:26
add a comment |
It is because the proposition $(neg P Rightarrow (Q wedge neg Q)) Rightarrow P$ is a tautology, meaning it is always true no matter the truth values of $P$ and $Q$.
The tautology is saying "If the opposite of $P$ implies something impossible, then $P$."
answered Mar 23 '18 at 0:09
diligar
496212
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%2f2704096%2fwhy-logically-is-proof-by-contradiction-valid%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
4 Answers
4
active
oldest
votes
4 Answers
4
active
oldest
votes
active
oldest
votes
active
oldest
votes
Yes, well, a proof by contradiction involves two rules of inference.
$$begin{split}text{Negation introduction}quad&quad (rimplies q) text{ and } (rimplies neg q), text{ infers } neg r\text{Double Negation elimination:}quad &quad negneg ptext{ infers } pend{split}$$
(1) the "Negation introduction" rule of inference argues that if something implies a contradiction then it must be false, since we usually assert that contradictions are not true and so cannot be infered by true things.
This is acceptable in both intuitionistic and classical logic systems. Although there are other systems (such as minimal logic) which do not accept this.
($deffalse{mathsf F}deftrue{mathsf T}$Semantically, this is because $false to false$ is true while $truetofalse$ is false. This leads some systems to define negation as $neg phi ~equiv~ phitomathsf F$ .)
(2) the "Double negation elimination" rule is that if the negation of a premise is false, then the premise must be true. This is not accepted in intuitionistic logic, but it is in classical logic.
(3) Combining these rules give the schema for a proof by contradiction: assume a negation of a predicate, demonstrate that infers a contradiction, thereby deducing that the predicate is true.
$$begin{split}text{Proof by Contradiction}quad&quad (neg p implies q) text{ and }(neg pimplies neg q) text{, infers }pend{split}$$
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
What is ⊢? Or ϕ? Why fractions?
– user525966
Mar 23 '18 at 1:18
The turnstyle, $vdash$, stands for "derivable". $phi, p, q, r$ are predicates. The proof tree displays the form of the rule. $neg r$ is infered when $q$ and $neg q$ are both derivable from $r$. $$dfrac{rvdash qquad rvdash neg q}{vdash neg r}{small negmathsf I}$$
– Graham Kemp
Mar 23 '18 at 2:01
What is the extra not-line thing on the far right?
– user525966
Mar 23 '18 at 2:08
1
Is this saying "When $q$ is provable from $r$, and $lnot q$ is also provable from $r$, then we conclude that $lnot r$ is provable from these premises"?
– user525966
Mar 23 '18 at 2:09
Maybe I should reedit.
– Graham Kemp
Mar 23 '18 at 2:19
|
show 4 more comments
Yes, well, a proof by contradiction involves two rules of inference.
$$begin{split}text{Negation introduction}quad&quad (rimplies q) text{ and } (rimplies neg q), text{ infers } neg r\text{Double Negation elimination:}quad &quad negneg ptext{ infers } pend{split}$$
(1) the "Negation introduction" rule of inference argues that if something implies a contradiction then it must be false, since we usually assert that contradictions are not true and so cannot be infered by true things.
This is acceptable in both intuitionistic and classical logic systems. Although there are other systems (such as minimal logic) which do not accept this.
($deffalse{mathsf F}deftrue{mathsf T}$Semantically, this is because $false to false$ is true while $truetofalse$ is false. This leads some systems to define negation as $neg phi ~equiv~ phitomathsf F$ .)
(2) the "Double negation elimination" rule is that if the negation of a premise is false, then the premise must be true. This is not accepted in intuitionistic logic, but it is in classical logic.
(3) Combining these rules give the schema for a proof by contradiction: assume a negation of a predicate, demonstrate that infers a contradiction, thereby deducing that the predicate is true.
$$begin{split}text{Proof by Contradiction}quad&quad (neg p implies q) text{ and }(neg pimplies neg q) text{, infers }pend{split}$$
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
What is ⊢? Or ϕ? Why fractions?
– user525966
Mar 23 '18 at 1:18
The turnstyle, $vdash$, stands for "derivable". $phi, p, q, r$ are predicates. The proof tree displays the form of the rule. $neg r$ is infered when $q$ and $neg q$ are both derivable from $r$. $$dfrac{rvdash qquad rvdash neg q}{vdash neg r}{small negmathsf I}$$
– Graham Kemp
Mar 23 '18 at 2:01
What is the extra not-line thing on the far right?
– user525966
Mar 23 '18 at 2:08
1
Is this saying "When $q$ is provable from $r$, and $lnot q$ is also provable from $r$, then we conclude that $lnot r$ is provable from these premises"?
– user525966
Mar 23 '18 at 2:09
Maybe I should reedit.
– Graham Kemp
Mar 23 '18 at 2:19
|
show 4 more comments
Yes, well, a proof by contradiction involves two rules of inference.
$$begin{split}text{Negation introduction}quad&quad (rimplies q) text{ and } (rimplies neg q), text{ infers } neg r\text{Double Negation elimination:}quad &quad negneg ptext{ infers } pend{split}$$
(1) the "Negation introduction" rule of inference argues that if something implies a contradiction then it must be false, since we usually assert that contradictions are not true and so cannot be infered by true things.
This is acceptable in both intuitionistic and classical logic systems. Although there are other systems (such as minimal logic) which do not accept this.
($deffalse{mathsf F}deftrue{mathsf T}$Semantically, this is because $false to false$ is true while $truetofalse$ is false. This leads some systems to define negation as $neg phi ~equiv~ phitomathsf F$ .)
(2) the "Double negation elimination" rule is that if the negation of a premise is false, then the premise must be true. This is not accepted in intuitionistic logic, but it is in classical logic.
(3) Combining these rules give the schema for a proof by contradiction: assume a negation of a predicate, demonstrate that infers a contradiction, thereby deducing that the predicate is true.
$$begin{split}text{Proof by Contradiction}quad&quad (neg p implies q) text{ and }(neg pimplies neg q) text{, infers }pend{split}$$
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
Yes, well, a proof by contradiction involves two rules of inference.
$$begin{split}text{Negation introduction}quad&quad (rimplies q) text{ and } (rimplies neg q), text{ infers } neg r\text{Double Negation elimination:}quad &quad negneg ptext{ infers } pend{split}$$
(1) the "Negation introduction" rule of inference argues that if something implies a contradiction then it must be false, since we usually assert that contradictions are not true and so cannot be infered by true things.
This is acceptable in both intuitionistic and classical logic systems. Although there are other systems (such as minimal logic) which do not accept this.
($deffalse{mathsf F}deftrue{mathsf T}$Semantically, this is because $false to false$ is true while $truetofalse$ is false. This leads some systems to define negation as $neg phi ~equiv~ phitomathsf F$ .)
(2) the "Double negation elimination" rule is that if the negation of a premise is false, then the premise must be true. This is not accepted in intuitionistic logic, but it is in classical logic.
(3) Combining these rules give the schema for a proof by contradiction: assume a negation of a predicate, demonstrate that infers a contradiction, thereby deducing that the predicate is true.
$$begin{split}text{Proof by Contradiction}quad&quad (neg p implies q) text{ and }(neg pimplies neg q) text{, infers }pend{split}$$
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
edited Mar 23 '18 at 6:52
Greek - Area 51 Proposal
3,158669103
3,158669103
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
answered Mar 23 '18 at 0:31
Graham Kemp
84.7k43378
84.7k43378
What is ⊢? Or ϕ? Why fractions?
– user525966
Mar 23 '18 at 1:18
The turnstyle, $vdash$, stands for "derivable". $phi, p, q, r$ are predicates. The proof tree displays the form of the rule. $neg r$ is infered when $q$ and $neg q$ are both derivable from $r$. $$dfrac{rvdash qquad rvdash neg q}{vdash neg r}{small negmathsf I}$$
– Graham Kemp
Mar 23 '18 at 2:01
What is the extra not-line thing on the far right?
– user525966
Mar 23 '18 at 2:08
1
Is this saying "When $q$ is provable from $r$, and $lnot q$ is also provable from $r$, then we conclude that $lnot r$ is provable from these premises"?
– user525966
Mar 23 '18 at 2:09
Maybe I should reedit.
– Graham Kemp
Mar 23 '18 at 2:19
|
show 4 more comments
What is ⊢? Or ϕ? Why fractions?
– user525966
Mar 23 '18 at 1:18
The turnstyle, $vdash$, stands for "derivable". $phi, p, q, r$ are predicates. The proof tree displays the form of the rule. $neg r$ is infered when $q$ and $neg q$ are both derivable from $r$. $$dfrac{rvdash qquad rvdash neg q}{vdash neg r}{small negmathsf I}$$
– Graham Kemp
Mar 23 '18 at 2:01
What is the extra not-line thing on the far right?
– user525966
Mar 23 '18 at 2:08
1
Is this saying "When $q$ is provable from $r$, and $lnot q$ is also provable from $r$, then we conclude that $lnot r$ is provable from these premises"?
– user525966
Mar 23 '18 at 2:09
Maybe I should reedit.
– Graham Kemp
Mar 23 '18 at 2:19
What is ⊢? Or ϕ? Why fractions?
– user525966
Mar 23 '18 at 1:18
What is ⊢? Or ϕ? Why fractions?
– user525966
Mar 23 '18 at 1:18
The turnstyle, $vdash$, stands for "derivable". $phi, p, q, r$ are predicates. The proof tree displays the form of the rule. $neg r$ is infered when $q$ and $neg q$ are both derivable from $r$. $$dfrac{rvdash qquad rvdash neg q}{vdash neg r}{small negmathsf I}$$
– Graham Kemp
Mar 23 '18 at 2:01
The turnstyle, $vdash$, stands for "derivable". $phi, p, q, r$ are predicates. The proof tree displays the form of the rule. $neg r$ is infered when $q$ and $neg q$ are both derivable from $r$. $$dfrac{rvdash qquad rvdash neg q}{vdash neg r}{small negmathsf I}$$
– Graham Kemp
Mar 23 '18 at 2:01
What is the extra not-line thing on the far right?
– user525966
Mar 23 '18 at 2:08
What is the extra not-line thing on the far right?
– user525966
Mar 23 '18 at 2:08
1
1
Is this saying "When $q$ is provable from $r$, and $lnot q$ is also provable from $r$, then we conclude that $lnot r$ is provable from these premises"?
– user525966
Mar 23 '18 at 2:09
Is this saying "When $q$ is provable from $r$, and $lnot q$ is also provable from $r$, then we conclude that $lnot r$ is provable from these premises"?
– user525966
Mar 23 '18 at 2:09
Maybe I should reedit.
– Graham Kemp
Mar 23 '18 at 2:19
Maybe I should reedit.
– Graham Kemp
Mar 23 '18 at 2:19
|
show 4 more comments
Many of the issues I described here are on display in this Q&A.
First, let's be clear about what we're talking about. There are two rules that are often called "proof by contradiction". The first, negation introduction, can be written like $cfrac{varphivdashbot}{vdashnegvarphi}$ which can be read as "if we can derive that $varphi$ entails falsity, then we can derive $negvarphi$". We could also write this as an axiom: $(varphiRightarrowbot)Rightarrownegvarphi$. For some reason, this is how Bram28 has taken your statement, but I don't think you have an issue with this. You'd say, "well clearly if assuming $varphi$ leads to a contradiction then $varphi$ must have been false and thus $negvarphi$ is true". There's another rule, more appropriately called "proof by contradiction", that can be written $cfrac{negvarphivdashbot}{vdashvarphi}$ or as an axiom $(negvarphiRightarrowbot)Rightarrowvarphi$. These seems to be what you are taking issue with. Seeing as this latter rule has been rejected by many mathematicians (constructivists of various sorts), you wouldn't be completely crazy to question it. (In weak defense of Bram28, you'd probably accept "by substituting $negpsi$ into the above, by the same argument we can show that $negpsi$ is false so $psi$ is true", but the rule only shows that $negnegpsi$ is true. The rule allowing you to go from $negnegpsi$ to $psi$ is, in fact, equivalent to proof by contradiction.)
To be even more clear about what we're talking about we need to distinguish syntax from semantics. If we're talking about "rules of inference" or "proofs", we are usually thinking syntactically. That is, we're thinking about symbols on a page and rules for manipulating those collections of symbols into other collections of symbols or rules about what constitutes "correct" arrangements of the symbols, i.e. a proof. (More informal renditions will be sentences in a natural language that follow "rules of reason", but the idea is still that the form of the argument is what makes it valid.) Semantics, on the other hand, interprets those symbols as mathematical objects and then we say a formula (i.e. arrangement of symbols) is "true" if it is interpreted into a mathematical object satisfying some given property. For example, we say a formula of classical propositional logic is "true" if its interpretation as a Boolean function is the constantly $1$ function.
So, we have two possible readings of your question: 1) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ derivable? 2) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ "true"?
For (1), one very unsatisfying answer is that it is often taken as given, i.e. it is derivable by definition of the logic. A slightly more satisfying answer is the following. Given a constructive logic where that rule isn't derivable but most other "usual" rules are, we can show that if for all formulas $varphi$, $vdashvarphilornegvarphi$ is derivable, then we can derive the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ (and vice versa). Another way of saying this is that $varphilornegvarphi$ is provably equivalent to $(negvarphiRightarrowbot)Rightarrowvarphi$. It is also provably equivalent to $negnegvarphiRightarrowvarphi$. The axiom $varphilornegvarphi$ is often described as "everything is either true or false". This isn't quite what it means, but this idea of everything being "either true or false" is often considered intuitively obvious. However, there is no question of whether $varphi$ is "true" or "false" in the above. We have rules for building proofs from other proofs, and that's all there is to this perspective.
For (2), if you use the "truth table" semantics of classical propositional logic, then you simply calculate. You simply need to show that $(negvarphiRightarrowbot)Rightarrowvarphi$ when interpreted is the constantly $1$ function when both $0$ and $1$ are substituted in the interpretation of the formula. You can easily show this. In these semantics, "proof by contradiction" is simply "true". To question this requires questioning the semantics. One thing is to question whether there are only two truth values, $0$ and $1$. Why not three or an infinite number of them? This leads to multi-valued logics. Alternatively, we could keep the truth values the same, but interpret formulas as something other than Boolean functions. For example, we could say they are Boolean functions but we only allow monotonic ones, or we could say that they are total Boolean relations. Making these changes requires adapting the notion of "true". For the latter example, we may say a formula is "true" if it is interpreted as a relation which relates all Boolean inputs to $1$. Being a relation and not just a function, though, this does not stop it from also relating some or all of the inputs to $0$, i.e. something can be both "true" and "false".
Changing the semantics affects which rules and axioms are sound. A rule or axiom is sound with respect to a given semantics, if its interpretation is "true" in that semantics. $(negvarphiRightarrowbot)Rightarrowvarphi$ is sound with respect to "truth tables" but not with respect to many other possible semantics.
To summarize, if you're working with respect to "truth table" semantics, then "proof by contradiction" is simply "true", that is when interpreted it is interpreted as a constantly "true" Boolean function, and this can be easily calculated. In this case, all of your "logical assumptions" are built into the notion of "truth table" semantics. With respect to semantics, "proof" is irrelevant. Proof is a syntactic concept. Your discussion about "assuming the premise is false" is (slightly mangled) proof-theoretic talk. With a semantic approach, there is no "assuming the premise is true/false", either the formula interprets as "true" (i.e. a constantly $1$ function) or it doesn't. (You can have meta-logical assumptions that some formula is "true", but this is happening outside of the logic. Ultimately the coin of the mathematical realm is the more syntactic notion of proof and semantics just pushes proof to the meta-logic.)
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
So,for proof by contradiction, law of excluded middle(LEM) is the "connecting link" between the syntax(proof process) and the binary-logic-truth-table(BLTT) semantics. Because the syntactics "just happens to" support the defining property of BLTT semantics(i.e.LEM) 'syntactically' i.e. derivable** AND the interpretation(achieved via axioms/rule i.e. syntactics) in BLTT semantics is "true",this makes syntactics sound,and things work out. 1 Was syntactical property of LEM accidentally or deliberately added to syntactics?Perhaps it is a loop then! 2 **So truth has syntactic constraints?
– Ajax
Nov 21 '18 at 9:31
LEM is not the "defining property" of truth table semantics. The intuitive idea that "everything is either true or false" idea is a major motivation for truth table semantics. As I alluded to in the answer, LEM does not say that everything is either true or false. Consider ${0,1}^2$ with operations defined component-wise. This semantics validates LEM, but $(0,1)$ is neither true, $(1,1)$, nor false, $(0,0)$.
– Derek Elkins
Nov 21 '18 at 21:02
As an axiom (schema), LEM is simply part of a definition of a proof system for classical propositional logic. If you have the rules of intuitionistic propositional logic and you add LEM, you can derive proof by contradiction. This doesn't require any semantics to even be defined, so LEM certainly isn't a "connecting link" between syntax and semantics.
– Derek Elkins
Nov 21 '18 at 21:02
I don't get why are you able to derive the syntax formula which clearly tells the story of what LEM is? More importantly why is your (derived) formula (1) telling me about LEM? Why is syntax indicating what it is talking about?
– Ajax
Nov 21 '18 at 21:45
add a comment |
Many of the issues I described here are on display in this Q&A.
First, let's be clear about what we're talking about. There are two rules that are often called "proof by contradiction". The first, negation introduction, can be written like $cfrac{varphivdashbot}{vdashnegvarphi}$ which can be read as "if we can derive that $varphi$ entails falsity, then we can derive $negvarphi$". We could also write this as an axiom: $(varphiRightarrowbot)Rightarrownegvarphi$. For some reason, this is how Bram28 has taken your statement, but I don't think you have an issue with this. You'd say, "well clearly if assuming $varphi$ leads to a contradiction then $varphi$ must have been false and thus $negvarphi$ is true". There's another rule, more appropriately called "proof by contradiction", that can be written $cfrac{negvarphivdashbot}{vdashvarphi}$ or as an axiom $(negvarphiRightarrowbot)Rightarrowvarphi$. These seems to be what you are taking issue with. Seeing as this latter rule has been rejected by many mathematicians (constructivists of various sorts), you wouldn't be completely crazy to question it. (In weak defense of Bram28, you'd probably accept "by substituting $negpsi$ into the above, by the same argument we can show that $negpsi$ is false so $psi$ is true", but the rule only shows that $negnegpsi$ is true. The rule allowing you to go from $negnegpsi$ to $psi$ is, in fact, equivalent to proof by contradiction.)
To be even more clear about what we're talking about we need to distinguish syntax from semantics. If we're talking about "rules of inference" or "proofs", we are usually thinking syntactically. That is, we're thinking about symbols on a page and rules for manipulating those collections of symbols into other collections of symbols or rules about what constitutes "correct" arrangements of the symbols, i.e. a proof. (More informal renditions will be sentences in a natural language that follow "rules of reason", but the idea is still that the form of the argument is what makes it valid.) Semantics, on the other hand, interprets those symbols as mathematical objects and then we say a formula (i.e. arrangement of symbols) is "true" if it is interpreted into a mathematical object satisfying some given property. For example, we say a formula of classical propositional logic is "true" if its interpretation as a Boolean function is the constantly $1$ function.
So, we have two possible readings of your question: 1) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ derivable? 2) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ "true"?
For (1), one very unsatisfying answer is that it is often taken as given, i.e. it is derivable by definition of the logic. A slightly more satisfying answer is the following. Given a constructive logic where that rule isn't derivable but most other "usual" rules are, we can show that if for all formulas $varphi$, $vdashvarphilornegvarphi$ is derivable, then we can derive the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ (and vice versa). Another way of saying this is that $varphilornegvarphi$ is provably equivalent to $(negvarphiRightarrowbot)Rightarrowvarphi$. It is also provably equivalent to $negnegvarphiRightarrowvarphi$. The axiom $varphilornegvarphi$ is often described as "everything is either true or false". This isn't quite what it means, but this idea of everything being "either true or false" is often considered intuitively obvious. However, there is no question of whether $varphi$ is "true" or "false" in the above. We have rules for building proofs from other proofs, and that's all there is to this perspective.
For (2), if you use the "truth table" semantics of classical propositional logic, then you simply calculate. You simply need to show that $(negvarphiRightarrowbot)Rightarrowvarphi$ when interpreted is the constantly $1$ function when both $0$ and $1$ are substituted in the interpretation of the formula. You can easily show this. In these semantics, "proof by contradiction" is simply "true". To question this requires questioning the semantics. One thing is to question whether there are only two truth values, $0$ and $1$. Why not three or an infinite number of them? This leads to multi-valued logics. Alternatively, we could keep the truth values the same, but interpret formulas as something other than Boolean functions. For example, we could say they are Boolean functions but we only allow monotonic ones, or we could say that they are total Boolean relations. Making these changes requires adapting the notion of "true". For the latter example, we may say a formula is "true" if it is interpreted as a relation which relates all Boolean inputs to $1$. Being a relation and not just a function, though, this does not stop it from also relating some or all of the inputs to $0$, i.e. something can be both "true" and "false".
Changing the semantics affects which rules and axioms are sound. A rule or axiom is sound with respect to a given semantics, if its interpretation is "true" in that semantics. $(negvarphiRightarrowbot)Rightarrowvarphi$ is sound with respect to "truth tables" but not with respect to many other possible semantics.
To summarize, if you're working with respect to "truth table" semantics, then "proof by contradiction" is simply "true", that is when interpreted it is interpreted as a constantly "true" Boolean function, and this can be easily calculated. In this case, all of your "logical assumptions" are built into the notion of "truth table" semantics. With respect to semantics, "proof" is irrelevant. Proof is a syntactic concept. Your discussion about "assuming the premise is false" is (slightly mangled) proof-theoretic talk. With a semantic approach, there is no "assuming the premise is true/false", either the formula interprets as "true" (i.e. a constantly $1$ function) or it doesn't. (You can have meta-logical assumptions that some formula is "true", but this is happening outside of the logic. Ultimately the coin of the mathematical realm is the more syntactic notion of proof and semantics just pushes proof to the meta-logic.)
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
So,for proof by contradiction, law of excluded middle(LEM) is the "connecting link" between the syntax(proof process) and the binary-logic-truth-table(BLTT) semantics. Because the syntactics "just happens to" support the defining property of BLTT semantics(i.e.LEM) 'syntactically' i.e. derivable** AND the interpretation(achieved via axioms/rule i.e. syntactics) in BLTT semantics is "true",this makes syntactics sound,and things work out. 1 Was syntactical property of LEM accidentally or deliberately added to syntactics?Perhaps it is a loop then! 2 **So truth has syntactic constraints?
– Ajax
Nov 21 '18 at 9:31
LEM is not the "defining property" of truth table semantics. The intuitive idea that "everything is either true or false" idea is a major motivation for truth table semantics. As I alluded to in the answer, LEM does not say that everything is either true or false. Consider ${0,1}^2$ with operations defined component-wise. This semantics validates LEM, but $(0,1)$ is neither true, $(1,1)$, nor false, $(0,0)$.
– Derek Elkins
Nov 21 '18 at 21:02
As an axiom (schema), LEM is simply part of a definition of a proof system for classical propositional logic. If you have the rules of intuitionistic propositional logic and you add LEM, you can derive proof by contradiction. This doesn't require any semantics to even be defined, so LEM certainly isn't a "connecting link" between syntax and semantics.
– Derek Elkins
Nov 21 '18 at 21:02
I don't get why are you able to derive the syntax formula which clearly tells the story of what LEM is? More importantly why is your (derived) formula (1) telling me about LEM? Why is syntax indicating what it is talking about?
– Ajax
Nov 21 '18 at 21:45
add a comment |
Many of the issues I described here are on display in this Q&A.
First, let's be clear about what we're talking about. There are two rules that are often called "proof by contradiction". The first, negation introduction, can be written like $cfrac{varphivdashbot}{vdashnegvarphi}$ which can be read as "if we can derive that $varphi$ entails falsity, then we can derive $negvarphi$". We could also write this as an axiom: $(varphiRightarrowbot)Rightarrownegvarphi$. For some reason, this is how Bram28 has taken your statement, but I don't think you have an issue with this. You'd say, "well clearly if assuming $varphi$ leads to a contradiction then $varphi$ must have been false and thus $negvarphi$ is true". There's another rule, more appropriately called "proof by contradiction", that can be written $cfrac{negvarphivdashbot}{vdashvarphi}$ or as an axiom $(negvarphiRightarrowbot)Rightarrowvarphi$. These seems to be what you are taking issue with. Seeing as this latter rule has been rejected by many mathematicians (constructivists of various sorts), you wouldn't be completely crazy to question it. (In weak defense of Bram28, you'd probably accept "by substituting $negpsi$ into the above, by the same argument we can show that $negpsi$ is false so $psi$ is true", but the rule only shows that $negnegpsi$ is true. The rule allowing you to go from $negnegpsi$ to $psi$ is, in fact, equivalent to proof by contradiction.)
To be even more clear about what we're talking about we need to distinguish syntax from semantics. If we're talking about "rules of inference" or "proofs", we are usually thinking syntactically. That is, we're thinking about symbols on a page and rules for manipulating those collections of symbols into other collections of symbols or rules about what constitutes "correct" arrangements of the symbols, i.e. a proof. (More informal renditions will be sentences in a natural language that follow "rules of reason", but the idea is still that the form of the argument is what makes it valid.) Semantics, on the other hand, interprets those symbols as mathematical objects and then we say a formula (i.e. arrangement of symbols) is "true" if it is interpreted into a mathematical object satisfying some given property. For example, we say a formula of classical propositional logic is "true" if its interpretation as a Boolean function is the constantly $1$ function.
So, we have two possible readings of your question: 1) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ derivable? 2) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ "true"?
For (1), one very unsatisfying answer is that it is often taken as given, i.e. it is derivable by definition of the logic. A slightly more satisfying answer is the following. Given a constructive logic where that rule isn't derivable but most other "usual" rules are, we can show that if for all formulas $varphi$, $vdashvarphilornegvarphi$ is derivable, then we can derive the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ (and vice versa). Another way of saying this is that $varphilornegvarphi$ is provably equivalent to $(negvarphiRightarrowbot)Rightarrowvarphi$. It is also provably equivalent to $negnegvarphiRightarrowvarphi$. The axiom $varphilornegvarphi$ is often described as "everything is either true or false". This isn't quite what it means, but this idea of everything being "either true or false" is often considered intuitively obvious. However, there is no question of whether $varphi$ is "true" or "false" in the above. We have rules for building proofs from other proofs, and that's all there is to this perspective.
For (2), if you use the "truth table" semantics of classical propositional logic, then you simply calculate. You simply need to show that $(negvarphiRightarrowbot)Rightarrowvarphi$ when interpreted is the constantly $1$ function when both $0$ and $1$ are substituted in the interpretation of the formula. You can easily show this. In these semantics, "proof by contradiction" is simply "true". To question this requires questioning the semantics. One thing is to question whether there are only two truth values, $0$ and $1$. Why not three or an infinite number of them? This leads to multi-valued logics. Alternatively, we could keep the truth values the same, but interpret formulas as something other than Boolean functions. For example, we could say they are Boolean functions but we only allow monotonic ones, or we could say that they are total Boolean relations. Making these changes requires adapting the notion of "true". For the latter example, we may say a formula is "true" if it is interpreted as a relation which relates all Boolean inputs to $1$. Being a relation and not just a function, though, this does not stop it from also relating some or all of the inputs to $0$, i.e. something can be both "true" and "false".
Changing the semantics affects which rules and axioms are sound. A rule or axiom is sound with respect to a given semantics, if its interpretation is "true" in that semantics. $(negvarphiRightarrowbot)Rightarrowvarphi$ is sound with respect to "truth tables" but not with respect to many other possible semantics.
To summarize, if you're working with respect to "truth table" semantics, then "proof by contradiction" is simply "true", that is when interpreted it is interpreted as a constantly "true" Boolean function, and this can be easily calculated. In this case, all of your "logical assumptions" are built into the notion of "truth table" semantics. With respect to semantics, "proof" is irrelevant. Proof is a syntactic concept. Your discussion about "assuming the premise is false" is (slightly mangled) proof-theoretic talk. With a semantic approach, there is no "assuming the premise is true/false", either the formula interprets as "true" (i.e. a constantly $1$ function) or it doesn't. (You can have meta-logical assumptions that some formula is "true", but this is happening outside of the logic. Ultimately the coin of the mathematical realm is the more syntactic notion of proof and semantics just pushes proof to the meta-logic.)
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
Many of the issues I described here are on display in this Q&A.
First, let's be clear about what we're talking about. There are two rules that are often called "proof by contradiction". The first, negation introduction, can be written like $cfrac{varphivdashbot}{vdashnegvarphi}$ which can be read as "if we can derive that $varphi$ entails falsity, then we can derive $negvarphi$". We could also write this as an axiom: $(varphiRightarrowbot)Rightarrownegvarphi$. For some reason, this is how Bram28 has taken your statement, but I don't think you have an issue with this. You'd say, "well clearly if assuming $varphi$ leads to a contradiction then $varphi$ must have been false and thus $negvarphi$ is true". There's another rule, more appropriately called "proof by contradiction", that can be written $cfrac{negvarphivdashbot}{vdashvarphi}$ or as an axiom $(negvarphiRightarrowbot)Rightarrowvarphi$. These seems to be what you are taking issue with. Seeing as this latter rule has been rejected by many mathematicians (constructivists of various sorts), you wouldn't be completely crazy to question it. (In weak defense of Bram28, you'd probably accept "by substituting $negpsi$ into the above, by the same argument we can show that $negpsi$ is false so $psi$ is true", but the rule only shows that $negnegpsi$ is true. The rule allowing you to go from $negnegpsi$ to $psi$ is, in fact, equivalent to proof by contradiction.)
To be even more clear about what we're talking about we need to distinguish syntax from semantics. If we're talking about "rules of inference" or "proofs", we are usually thinking syntactically. That is, we're thinking about symbols on a page and rules for manipulating those collections of symbols into other collections of symbols or rules about what constitutes "correct" arrangements of the symbols, i.e. a proof. (More informal renditions will be sentences in a natural language that follow "rules of reason", but the idea is still that the form of the argument is what makes it valid.) Semantics, on the other hand, interprets those symbols as mathematical objects and then we say a formula (i.e. arrangement of symbols) is "true" if it is interpreted into a mathematical object satisfying some given property. For example, we say a formula of classical propositional logic is "true" if its interpretation as a Boolean function is the constantly $1$ function.
So, we have two possible readings of your question: 1) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ derivable? 2) Why is the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ "true"?
For (1), one very unsatisfying answer is that it is often taken as given, i.e. it is derivable by definition of the logic. A slightly more satisfying answer is the following. Given a constructive logic where that rule isn't derivable but most other "usual" rules are, we can show that if for all formulas $varphi$, $vdashvarphilornegvarphi$ is derivable, then we can derive the rule $cfrac{negvarphivdashbot}{vdashvarphi}$ (and vice versa). Another way of saying this is that $varphilornegvarphi$ is provably equivalent to $(negvarphiRightarrowbot)Rightarrowvarphi$. It is also provably equivalent to $negnegvarphiRightarrowvarphi$. The axiom $varphilornegvarphi$ is often described as "everything is either true or false". This isn't quite what it means, but this idea of everything being "either true or false" is often considered intuitively obvious. However, there is no question of whether $varphi$ is "true" or "false" in the above. We have rules for building proofs from other proofs, and that's all there is to this perspective.
For (2), if you use the "truth table" semantics of classical propositional logic, then you simply calculate. You simply need to show that $(negvarphiRightarrowbot)Rightarrowvarphi$ when interpreted is the constantly $1$ function when both $0$ and $1$ are substituted in the interpretation of the formula. You can easily show this. In these semantics, "proof by contradiction" is simply "true". To question this requires questioning the semantics. One thing is to question whether there are only two truth values, $0$ and $1$. Why not three or an infinite number of them? This leads to multi-valued logics. Alternatively, we could keep the truth values the same, but interpret formulas as something other than Boolean functions. For example, we could say they are Boolean functions but we only allow monotonic ones, or we could say that they are total Boolean relations. Making these changes requires adapting the notion of "true". For the latter example, we may say a formula is "true" if it is interpreted as a relation which relates all Boolean inputs to $1$. Being a relation and not just a function, though, this does not stop it from also relating some or all of the inputs to $0$, i.e. something can be both "true" and "false".
Changing the semantics affects which rules and axioms are sound. A rule or axiom is sound with respect to a given semantics, if its interpretation is "true" in that semantics. $(negvarphiRightarrowbot)Rightarrowvarphi$ is sound with respect to "truth tables" but not with respect to many other possible semantics.
To summarize, if you're working with respect to "truth table" semantics, then "proof by contradiction" is simply "true", that is when interpreted it is interpreted as a constantly "true" Boolean function, and this can be easily calculated. In this case, all of your "logical assumptions" are built into the notion of "truth table" semantics. With respect to semantics, "proof" is irrelevant. Proof is a syntactic concept. Your discussion about "assuming the premise is false" is (slightly mangled) proof-theoretic talk. With a semantic approach, there is no "assuming the premise is true/false", either the formula interprets as "true" (i.e. a constantly $1$ function) or it doesn't. (You can have meta-logical assumptions that some formula is "true", but this is happening outside of the logic. Ultimately the coin of the mathematical realm is the more syntactic notion of proof and semantics just pushes proof to the meta-logic.)
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
answered Mar 23 '18 at 1:41
Derek Elkins
16.2k11337
16.2k11337
So,for proof by contradiction, law of excluded middle(LEM) is the "connecting link" between the syntax(proof process) and the binary-logic-truth-table(BLTT) semantics. Because the syntactics "just happens to" support the defining property of BLTT semantics(i.e.LEM) 'syntactically' i.e. derivable** AND the interpretation(achieved via axioms/rule i.e. syntactics) in BLTT semantics is "true",this makes syntactics sound,and things work out. 1 Was syntactical property of LEM accidentally or deliberately added to syntactics?Perhaps it is a loop then! 2 **So truth has syntactic constraints?
– Ajax
Nov 21 '18 at 9:31
LEM is not the "defining property" of truth table semantics. The intuitive idea that "everything is either true or false" idea is a major motivation for truth table semantics. As I alluded to in the answer, LEM does not say that everything is either true or false. Consider ${0,1}^2$ with operations defined component-wise. This semantics validates LEM, but $(0,1)$ is neither true, $(1,1)$, nor false, $(0,0)$.
– Derek Elkins
Nov 21 '18 at 21:02
As an axiom (schema), LEM is simply part of a definition of a proof system for classical propositional logic. If you have the rules of intuitionistic propositional logic and you add LEM, you can derive proof by contradiction. This doesn't require any semantics to even be defined, so LEM certainly isn't a "connecting link" between syntax and semantics.
– Derek Elkins
Nov 21 '18 at 21:02
I don't get why are you able to derive the syntax formula which clearly tells the story of what LEM is? More importantly why is your (derived) formula (1) telling me about LEM? Why is syntax indicating what it is talking about?
– Ajax
Nov 21 '18 at 21:45
add a comment |
So,for proof by contradiction, law of excluded middle(LEM) is the "connecting link" between the syntax(proof process) and the binary-logic-truth-table(BLTT) semantics. Because the syntactics "just happens to" support the defining property of BLTT semantics(i.e.LEM) 'syntactically' i.e. derivable** AND the interpretation(achieved via axioms/rule i.e. syntactics) in BLTT semantics is "true",this makes syntactics sound,and things work out. 1 Was syntactical property of LEM accidentally or deliberately added to syntactics?Perhaps it is a loop then! 2 **So truth has syntactic constraints?
– Ajax
Nov 21 '18 at 9:31
LEM is not the "defining property" of truth table semantics. The intuitive idea that "everything is either true or false" idea is a major motivation for truth table semantics. As I alluded to in the answer, LEM does not say that everything is either true or false. Consider ${0,1}^2$ with operations defined component-wise. This semantics validates LEM, but $(0,1)$ is neither true, $(1,1)$, nor false, $(0,0)$.
– Derek Elkins
Nov 21 '18 at 21:02
As an axiom (schema), LEM is simply part of a definition of a proof system for classical propositional logic. If you have the rules of intuitionistic propositional logic and you add LEM, you can derive proof by contradiction. This doesn't require any semantics to even be defined, so LEM certainly isn't a "connecting link" between syntax and semantics.
– Derek Elkins
Nov 21 '18 at 21:02
I don't get why are you able to derive the syntax formula which clearly tells the story of what LEM is? More importantly why is your (derived) formula (1) telling me about LEM? Why is syntax indicating what it is talking about?
– Ajax
Nov 21 '18 at 21:45
So,for proof by contradiction, law of excluded middle(LEM) is the "connecting link" between the syntax(proof process) and the binary-logic-truth-table(BLTT) semantics. Because the syntactics "just happens to" support the defining property of BLTT semantics(i.e.LEM) 'syntactically' i.e. derivable** AND the interpretation(achieved via axioms/rule i.e. syntactics) in BLTT semantics is "true",this makes syntactics sound,and things work out. 1 Was syntactical property of LEM accidentally or deliberately added to syntactics?Perhaps it is a loop then! 2 **So truth has syntactic constraints?
– Ajax
Nov 21 '18 at 9:31
So,for proof by contradiction, law of excluded middle(LEM) is the "connecting link" between the syntax(proof process) and the binary-logic-truth-table(BLTT) semantics. Because the syntactics "just happens to" support the defining property of BLTT semantics(i.e.LEM) 'syntactically' i.e. derivable** AND the interpretation(achieved via axioms/rule i.e. syntactics) in BLTT semantics is "true",this makes syntactics sound,and things work out. 1 Was syntactical property of LEM accidentally or deliberately added to syntactics?Perhaps it is a loop then! 2 **So truth has syntactic constraints?
– Ajax
Nov 21 '18 at 9:31
LEM is not the "defining property" of truth table semantics. The intuitive idea that "everything is either true or false" idea is a major motivation for truth table semantics. As I alluded to in the answer, LEM does not say that everything is either true or false. Consider ${0,1}^2$ with operations defined component-wise. This semantics validates LEM, but $(0,1)$ is neither true, $(1,1)$, nor false, $(0,0)$.
– Derek Elkins
Nov 21 '18 at 21:02
LEM is not the "defining property" of truth table semantics. The intuitive idea that "everything is either true or false" idea is a major motivation for truth table semantics. As I alluded to in the answer, LEM does not say that everything is either true or false. Consider ${0,1}^2$ with operations defined component-wise. This semantics validates LEM, but $(0,1)$ is neither true, $(1,1)$, nor false, $(0,0)$.
– Derek Elkins
Nov 21 '18 at 21:02
As an axiom (schema), LEM is simply part of a definition of a proof system for classical propositional logic. If you have the rules of intuitionistic propositional logic and you add LEM, you can derive proof by contradiction. This doesn't require any semantics to even be defined, so LEM certainly isn't a "connecting link" between syntax and semantics.
– Derek Elkins
Nov 21 '18 at 21:02
As an axiom (schema), LEM is simply part of a definition of a proof system for classical propositional logic. If you have the rules of intuitionistic propositional logic and you add LEM, you can derive proof by contradiction. This doesn't require any semantics to even be defined, so LEM certainly isn't a "connecting link" between syntax and semantics.
– Derek Elkins
Nov 21 '18 at 21:02
I don't get why are you able to derive the syntax formula which clearly tells the story of what LEM is? More importantly why is your (derived) formula (1) telling me about LEM? Why is syntax indicating what it is talking about?
– Ajax
Nov 21 '18 at 21:45
I don't get why are you able to derive the syntax formula which clearly tells the story of what LEM is? More importantly why is your (derived) formula (1) telling me about LEM? Why is syntax indicating what it is talking about?
– Ajax
Nov 21 '18 at 21:45
add a comment |
It works as follows:
Say you have some set of statements $Gamma$, and we want to infer $neg phi$, and we do this by a proof by contradiction.
Thus, we assume $phi$, and show that that leads to a contradiction.
This means that $Gamma$, together with $phi$ logically implies a contradiction, i.e.
$$Gamma cup phi vDash bot$$
and that means that is impossible to set all of the statements in $Gamma cup phi$ to true. But that then also means that if all statements in $Gamma$ are true, $phi$ will have to be false, i.e. $neg phi$ will have to be true. And thus we have
$$Gamma vDash neg phi$$
Thus, in effect, we have proven $neg phi$
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
What is ϕ? Or ⊨?
– user525966
Mar 23 '18 at 1:26
add a comment |
It works as follows:
Say you have some set of statements $Gamma$, and we want to infer $neg phi$, and we do this by a proof by contradiction.
Thus, we assume $phi$, and show that that leads to a contradiction.
This means that $Gamma$, together with $phi$ logically implies a contradiction, i.e.
$$Gamma cup phi vDash bot$$
and that means that is impossible to set all of the statements in $Gamma cup phi$ to true. But that then also means that if all statements in $Gamma$ are true, $phi$ will have to be false, i.e. $neg phi$ will have to be true. And thus we have
$$Gamma vDash neg phi$$
Thus, in effect, we have proven $neg phi$
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
What is ϕ? Or ⊨?
– user525966
Mar 23 '18 at 1:26
add a comment |
It works as follows:
Say you have some set of statements $Gamma$, and we want to infer $neg phi$, and we do this by a proof by contradiction.
Thus, we assume $phi$, and show that that leads to a contradiction.
This means that $Gamma$, together with $phi$ logically implies a contradiction, i.e.
$$Gamma cup phi vDash bot$$
and that means that is impossible to set all of the statements in $Gamma cup phi$ to true. But that then also means that if all statements in $Gamma$ are true, $phi$ will have to be false, i.e. $neg phi$ will have to be true. And thus we have
$$Gamma vDash neg phi$$
Thus, in effect, we have proven $neg phi$
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
It works as follows:
Say you have some set of statements $Gamma$, and we want to infer $neg phi$, and we do this by a proof by contradiction.
Thus, we assume $phi$, and show that that leads to a contradiction.
This means that $Gamma$, together with $phi$ logically implies a contradiction, i.e.
$$Gamma cup phi vDash bot$$
and that means that is impossible to set all of the statements in $Gamma cup phi$ to true. But that then also means that if all statements in $Gamma$ are true, $phi$ will have to be false, i.e. $neg phi$ will have to be true. And thus we have
$$Gamma vDash neg phi$$
Thus, in effect, we have proven $neg phi$
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
answered Mar 22 '18 at 23:58
Bram28
60.3k44590
60.3k44590
What is ϕ? Or ⊨?
– user525966
Mar 23 '18 at 1:26
add a comment |
What is ϕ? Or ⊨?
– user525966
Mar 23 '18 at 1:26
What is ϕ? Or ⊨?
– user525966
Mar 23 '18 at 1:26
What is ϕ? Or ⊨?
– user525966
Mar 23 '18 at 1:26
add a comment |
It is because the proposition $(neg P Rightarrow (Q wedge neg Q)) Rightarrow P$ is a tautology, meaning it is always true no matter the truth values of $P$ and $Q$.
The tautology is saying "If the opposite of $P$ implies something impossible, then $P$."
answered Mar 23 '18 at 0:09
diligar
496212
add a comment |
It is because the proposition $(neg P Rightarrow (Q wedge neg Q)) Rightarrow P$ is a tautology, meaning it is always true no matter the truth values of $P$ and $Q$.
The tautology is saying "If the opposite of $P$ implies something impossible, then $P$."
answered Mar 23 '18 at 0:09
diligar
496212
add a comment |
It is because the proposition $(neg P Rightarrow (Q wedge neg Q)) Rightarrow P$ is a tautology, meaning it is always true no matter the truth values of $P$ and $Q$.
The tautology is saying "If the opposite of $P$ implies something impossible, then $P$."
answered Mar 23 '18 at 0:09
diligar
496212
It is because the proposition $(neg P Rightarrow (Q wedge neg Q)) Rightarrow P$ is a tautology, meaning it is always true no matter the truth values of $P$ and $Q$.
The tautology is saying "If the opposite of $P$ implies something impossible, then $P$."
answered Mar 23 '18 at 0:09
diligar
496212
answered Mar 23 '18 at 0:09
diligar
496212
answered Mar 23 '18 at 0:09
diligar
496212
answered Mar 23 '18 at 0:09
diligar
496212
496212
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.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- 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.
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%2f2704096%2fwhy-logically-is-proof-by-contradiction-valid%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
8
Either a theorem is true or it is false. Truth by contradiction eliminates one of those alternatives.
– David G. Stork
Mar 22 '18 at 23:40
4
No, we assume the premise is true and if it leads to false it means the premise is false and the opposite of false is true.
– Vasya
Mar 22 '18 at 23:42
Possible duplicate: math.stackexchange.com/questions/2431003/…
– user477343
Mar 23 '18 at 0:20
2
"Works logically" depends on the proof system you are using.
– Graham Kemp
Mar 23 '18 at 0:36
I think the struggle to accept this type of proof isn't so much the system of logic, but a quirk of its application. In J. P. Serre's words "A proof by contradiction is the only proof where when you make a mistake it helps you."
– Algeboy
Mar 23 '18 at 2:55