Circularity of LEM, principle of explosion, and $lnot lnot$ elimination











up vote
2
down vote

favorite
1












Consider the following proof of the principle of explosion using $lnot lnot$ elim:



|Assume $p land lnot p$



$quad$|$p$ (from $land$ elim)



$quad$|$lnot p$ (from $land$ elim)



$quad$|Assume $lnot q$



$quad$$quad$|$p$ (restatement)



$quad$|$lnot q to p$ (from $to$ intro)



$quad$|Assume $lnot q$



$quad$$quad$|$lnot p$ (restatement)



$quad$|$lnot q to lnot p$ (from $to$ intro)



$quad$|$lnot lnot q$ (from $lnot$ intro)



$quad$|$q$ (from $lnot lnot$ elim)



|$p land lnot p to q$ (from $to$ intro)



Consider also the proof of LEM using $lnot lnot$ elim:



|Assume $lnot(p lor lnot p)$



$quad$|$lnot(p lor lnot p)$ (restatement)



|$lnot(p lor lnot p) to lnot(p lor lnot p)$ (from $to$ intro)



|Assume $lnot(p lor lnot p)$



$quad$|Assume $p$



$quad$$quad$|$lnot(p lor lnot p)$ (restatement)



$quad$|$p to lnot(p lor lnot p)$ (from $to$ intro)



$quad$|Assume $p$



$quad$$quad$|$p lor lnot p$ (from $lor$ intro)



$quad$|$p to p lor lnot p$ (from $to$ intro)



$quad$|$lnot p$ (from $lnot$ intro)



$quad$|$p lor lnot p$ (from $lor$ intro)



|$lnot(p lor lnot p) to p lor lnot p$ (from $to$ intro)



|$lnot lnot (p lor lnot p)$ (from $lnot$ intro)



|$p lor lnot p$ (from $lnot lnot$ elim)



And a proof of $lnot lnot$ elim if we have LEM and the principle of explosion at our disposal:



|$p lor lnot p$ (from LEM)



|Assume $lnot lnot p$



$quad$|Assume $p$



$quad$$quad$| $p$ (restatement)



$quad$|Assume $lnot p$



$quad$$quad$|$lnot p$ (restatement)



$quad$$quad$|$lnot lnot p land lnot p$ (from $land$ intro)



$quad$$quad$|$bot$ ($lnot$ elim)



$quad$$quad$|$p$ (from $bot$ elim / the principle of explosion)



$quad$|$p$ (from $lor$ elim on LEM and the two previous assumption cases)



|$lnot lnot p to p$ (from $to$ intro)



My question



Am I reading this right? These rules appear circular and interdependent. If we are granted LEM and the principle of explosion, we can derive $lnot lnot$ elimination, but if we're granted $lnot lnot$ elimination, we can derive both LEM and the principle of explosion.



Is this correct or is there a way to derive these rules from some other common means?










share|cite|improve this question




















  • 2




    The finer details of the answer depend on the specific rules you are allowed to use in this formalism, however, yes, you appear to be reading this right: these rules can be derived from each other. In most formalisms which are set up for this discussion (i.e. classical logic is not "baked in", and it is a formalism for intuitionistic logic which can be made (more) classical by adding new rules), I would expect the principle of explosion to hold regardless, and LEM and $negneg$-elimination to be equivalent. Perhaps in this specific formalism the principle of explosion is not a given.
    – Mees de Vries
    Nov 19 at 15:23










  • @MeesdeVries I believe intuitionistic logic merely disallows LEM and $lnot lnot$ elimination but allows the principle of explosion (which is baked into its system without proof)
    – Brandon L
    Nov 19 at 15:30












  • In your proof you have used the principle : $(p to q) to ((p to lnot q) to lnot p)$ that is equivalent (in a system without $bot$) to $lnot$-intro : $(p to bot) vdash lnot p$
    – Mauro ALLEGRANZA
    Nov 19 at 15:56












  • @MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
    – Brandon L
    Nov 19 at 16:01












  • LEM and DN are equivalent and they are both not allowed in Intuitionsitic Logic; but this one use $bot to p$. Thus the first two are not equivalent to $bot to p$.
    – Mauro ALLEGRANZA
    Nov 19 at 16:16















up vote
2
down vote

favorite
1












Consider the following proof of the principle of explosion using $lnot lnot$ elim:



|Assume $p land lnot p$



$quad$|$p$ (from $land$ elim)



$quad$|$lnot p$ (from $land$ elim)



$quad$|Assume $lnot q$



$quad$$quad$|$p$ (restatement)



$quad$|$lnot q to p$ (from $to$ intro)



$quad$|Assume $lnot q$



$quad$$quad$|$lnot p$ (restatement)



$quad$|$lnot q to lnot p$ (from $to$ intro)



$quad$|$lnot lnot q$ (from $lnot$ intro)



$quad$|$q$ (from $lnot lnot$ elim)



|$p land lnot p to q$ (from $to$ intro)



Consider also the proof of LEM using $lnot lnot$ elim:



|Assume $lnot(p lor lnot p)$



$quad$|$lnot(p lor lnot p)$ (restatement)



|$lnot(p lor lnot p) to lnot(p lor lnot p)$ (from $to$ intro)



|Assume $lnot(p lor lnot p)$



$quad$|Assume $p$



$quad$$quad$|$lnot(p lor lnot p)$ (restatement)



$quad$|$p to lnot(p lor lnot p)$ (from $to$ intro)



$quad$|Assume $p$



$quad$$quad$|$p lor lnot p$ (from $lor$ intro)



$quad$|$p to p lor lnot p$ (from $to$ intro)



$quad$|$lnot p$ (from $lnot$ intro)



$quad$|$p lor lnot p$ (from $lor$ intro)



|$lnot(p lor lnot p) to p lor lnot p$ (from $to$ intro)



|$lnot lnot (p lor lnot p)$ (from $lnot$ intro)



|$p lor lnot p$ (from $lnot lnot$ elim)



And a proof of $lnot lnot$ elim if we have LEM and the principle of explosion at our disposal:



|$p lor lnot p$ (from LEM)



|Assume $lnot lnot p$



$quad$|Assume $p$



$quad$$quad$| $p$ (restatement)



$quad$|Assume $lnot p$



$quad$$quad$|$lnot p$ (restatement)



$quad$$quad$|$lnot lnot p land lnot p$ (from $land$ intro)



$quad$$quad$|$bot$ ($lnot$ elim)



$quad$$quad$|$p$ (from $bot$ elim / the principle of explosion)



$quad$|$p$ (from $lor$ elim on LEM and the two previous assumption cases)



|$lnot lnot p to p$ (from $to$ intro)



My question



Am I reading this right? These rules appear circular and interdependent. If we are granted LEM and the principle of explosion, we can derive $lnot lnot$ elimination, but if we're granted $lnot lnot$ elimination, we can derive both LEM and the principle of explosion.



Is this correct or is there a way to derive these rules from some other common means?










share|cite|improve this question




















  • 2




    The finer details of the answer depend on the specific rules you are allowed to use in this formalism, however, yes, you appear to be reading this right: these rules can be derived from each other. In most formalisms which are set up for this discussion (i.e. classical logic is not "baked in", and it is a formalism for intuitionistic logic which can be made (more) classical by adding new rules), I would expect the principle of explosion to hold regardless, and LEM and $negneg$-elimination to be equivalent. Perhaps in this specific formalism the principle of explosion is not a given.
    – Mees de Vries
    Nov 19 at 15:23










  • @MeesdeVries I believe intuitionistic logic merely disallows LEM and $lnot lnot$ elimination but allows the principle of explosion (which is baked into its system without proof)
    – Brandon L
    Nov 19 at 15:30












  • In your proof you have used the principle : $(p to q) to ((p to lnot q) to lnot p)$ that is equivalent (in a system without $bot$) to $lnot$-intro : $(p to bot) vdash lnot p$
    – Mauro ALLEGRANZA
    Nov 19 at 15:56












  • @MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
    – Brandon L
    Nov 19 at 16:01












  • LEM and DN are equivalent and they are both not allowed in Intuitionsitic Logic; but this one use $bot to p$. Thus the first two are not equivalent to $bot to p$.
    – Mauro ALLEGRANZA
    Nov 19 at 16:16













up vote
2
down vote

favorite
1









up vote
2
down vote

favorite
1






1





Consider the following proof of the principle of explosion using $lnot lnot$ elim:



|Assume $p land lnot p$



$quad$|$p$ (from $land$ elim)



$quad$|$lnot p$ (from $land$ elim)



$quad$|Assume $lnot q$



$quad$$quad$|$p$ (restatement)



$quad$|$lnot q to p$ (from $to$ intro)



$quad$|Assume $lnot q$



$quad$$quad$|$lnot p$ (restatement)



$quad$|$lnot q to lnot p$ (from $to$ intro)



$quad$|$lnot lnot q$ (from $lnot$ intro)



$quad$|$q$ (from $lnot lnot$ elim)



|$p land lnot p to q$ (from $to$ intro)



Consider also the proof of LEM using $lnot lnot$ elim:



|Assume $lnot(p lor lnot p)$



$quad$|$lnot(p lor lnot p)$ (restatement)



|$lnot(p lor lnot p) to lnot(p lor lnot p)$ (from $to$ intro)



|Assume $lnot(p lor lnot p)$



$quad$|Assume $p$



$quad$$quad$|$lnot(p lor lnot p)$ (restatement)



$quad$|$p to lnot(p lor lnot p)$ (from $to$ intro)



$quad$|Assume $p$



$quad$$quad$|$p lor lnot p$ (from $lor$ intro)



$quad$|$p to p lor lnot p$ (from $to$ intro)



$quad$|$lnot p$ (from $lnot$ intro)



$quad$|$p lor lnot p$ (from $lor$ intro)



|$lnot(p lor lnot p) to p lor lnot p$ (from $to$ intro)



|$lnot lnot (p lor lnot p)$ (from $lnot$ intro)



|$p lor lnot p$ (from $lnot lnot$ elim)



And a proof of $lnot lnot$ elim if we have LEM and the principle of explosion at our disposal:



|$p lor lnot p$ (from LEM)



|Assume $lnot lnot p$



$quad$|Assume $p$



$quad$$quad$| $p$ (restatement)



$quad$|Assume $lnot p$



$quad$$quad$|$lnot p$ (restatement)



$quad$$quad$|$lnot lnot p land lnot p$ (from $land$ intro)



$quad$$quad$|$bot$ ($lnot$ elim)



$quad$$quad$|$p$ (from $bot$ elim / the principle of explosion)



$quad$|$p$ (from $lor$ elim on LEM and the two previous assumption cases)



|$lnot lnot p to p$ (from $to$ intro)



My question



Am I reading this right? These rules appear circular and interdependent. If we are granted LEM and the principle of explosion, we can derive $lnot lnot$ elimination, but if we're granted $lnot lnot$ elimination, we can derive both LEM and the principle of explosion.



Is this correct or is there a way to derive these rules from some other common means?










share|cite|improve this question















Consider the following proof of the principle of explosion using $lnot lnot$ elim:



|Assume $p land lnot p$



$quad$|$p$ (from $land$ elim)



$quad$|$lnot p$ (from $land$ elim)



$quad$|Assume $lnot q$



$quad$$quad$|$p$ (restatement)



$quad$|$lnot q to p$ (from $to$ intro)



$quad$|Assume $lnot q$



$quad$$quad$|$lnot p$ (restatement)



$quad$|$lnot q to lnot p$ (from $to$ intro)



$quad$|$lnot lnot q$ (from $lnot$ intro)



$quad$|$q$ (from $lnot lnot$ elim)



|$p land lnot p to q$ (from $to$ intro)



Consider also the proof of LEM using $lnot lnot$ elim:



|Assume $lnot(p lor lnot p)$



$quad$|$lnot(p lor lnot p)$ (restatement)



|$lnot(p lor lnot p) to lnot(p lor lnot p)$ (from $to$ intro)



|Assume $lnot(p lor lnot p)$



$quad$|Assume $p$



$quad$$quad$|$lnot(p lor lnot p)$ (restatement)



$quad$|$p to lnot(p lor lnot p)$ (from $to$ intro)



$quad$|Assume $p$



$quad$$quad$|$p lor lnot p$ (from $lor$ intro)



$quad$|$p to p lor lnot p$ (from $to$ intro)



$quad$|$lnot p$ (from $lnot$ intro)



$quad$|$p lor lnot p$ (from $lor$ intro)



|$lnot(p lor lnot p) to p lor lnot p$ (from $to$ intro)



|$lnot lnot (p lor lnot p)$ (from $lnot$ intro)



|$p lor lnot p$ (from $lnot lnot$ elim)



And a proof of $lnot lnot$ elim if we have LEM and the principle of explosion at our disposal:



|$p lor lnot p$ (from LEM)



|Assume $lnot lnot p$



$quad$|Assume $p$



$quad$$quad$| $p$ (restatement)



$quad$|Assume $lnot p$



$quad$$quad$|$lnot p$ (restatement)



$quad$$quad$|$lnot lnot p land lnot p$ (from $land$ intro)



$quad$$quad$|$bot$ ($lnot$ elim)



$quad$$quad$|$p$ (from $bot$ elim / the principle of explosion)



$quad$|$p$ (from $lor$ elim on LEM and the two previous assumption cases)



|$lnot lnot p to p$ (from $to$ intro)



My question



Am I reading this right? These rules appear circular and interdependent. If we are granted LEM and the principle of explosion, we can derive $lnot lnot$ elimination, but if we're granted $lnot lnot$ elimination, we can derive both LEM and the principle of explosion.



Is this correct or is there a way to derive these rules from some other common means?







logic proof-explanation propositional-calculus






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited Nov 19 at 15:25

























asked Nov 19 at 15:18









Brandon L

184




184








  • 2




    The finer details of the answer depend on the specific rules you are allowed to use in this formalism, however, yes, you appear to be reading this right: these rules can be derived from each other. In most formalisms which are set up for this discussion (i.e. classical logic is not "baked in", and it is a formalism for intuitionistic logic which can be made (more) classical by adding new rules), I would expect the principle of explosion to hold regardless, and LEM and $negneg$-elimination to be equivalent. Perhaps in this specific formalism the principle of explosion is not a given.
    – Mees de Vries
    Nov 19 at 15:23










  • @MeesdeVries I believe intuitionistic logic merely disallows LEM and $lnot lnot$ elimination but allows the principle of explosion (which is baked into its system without proof)
    – Brandon L
    Nov 19 at 15:30












  • In your proof you have used the principle : $(p to q) to ((p to lnot q) to lnot p)$ that is equivalent (in a system without $bot$) to $lnot$-intro : $(p to bot) vdash lnot p$
    – Mauro ALLEGRANZA
    Nov 19 at 15:56












  • @MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
    – Brandon L
    Nov 19 at 16:01












  • LEM and DN are equivalent and they are both not allowed in Intuitionsitic Logic; but this one use $bot to p$. Thus the first two are not equivalent to $bot to p$.
    – Mauro ALLEGRANZA
    Nov 19 at 16:16














  • 2




    The finer details of the answer depend on the specific rules you are allowed to use in this formalism, however, yes, you appear to be reading this right: these rules can be derived from each other. In most formalisms which are set up for this discussion (i.e. classical logic is not "baked in", and it is a formalism for intuitionistic logic which can be made (more) classical by adding new rules), I would expect the principle of explosion to hold regardless, and LEM and $negneg$-elimination to be equivalent. Perhaps in this specific formalism the principle of explosion is not a given.
    – Mees de Vries
    Nov 19 at 15:23










  • @MeesdeVries I believe intuitionistic logic merely disallows LEM and $lnot lnot$ elimination but allows the principle of explosion (which is baked into its system without proof)
    – Brandon L
    Nov 19 at 15:30












  • In your proof you have used the principle : $(p to q) to ((p to lnot q) to lnot p)$ that is equivalent (in a system without $bot$) to $lnot$-intro : $(p to bot) vdash lnot p$
    – Mauro ALLEGRANZA
    Nov 19 at 15:56












  • @MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
    – Brandon L
    Nov 19 at 16:01












  • LEM and DN are equivalent and they are both not allowed in Intuitionsitic Logic; but this one use $bot to p$. Thus the first two are not equivalent to $bot to p$.
    – Mauro ALLEGRANZA
    Nov 19 at 16:16








2




2




The finer details of the answer depend on the specific rules you are allowed to use in this formalism, however, yes, you appear to be reading this right: these rules can be derived from each other. In most formalisms which are set up for this discussion (i.e. classical logic is not "baked in", and it is a formalism for intuitionistic logic which can be made (more) classical by adding new rules), I would expect the principle of explosion to hold regardless, and LEM and $negneg$-elimination to be equivalent. Perhaps in this specific formalism the principle of explosion is not a given.
– Mees de Vries
Nov 19 at 15:23




The finer details of the answer depend on the specific rules you are allowed to use in this formalism, however, yes, you appear to be reading this right: these rules can be derived from each other. In most formalisms which are set up for this discussion (i.e. classical logic is not "baked in", and it is a formalism for intuitionistic logic which can be made (more) classical by adding new rules), I would expect the principle of explosion to hold regardless, and LEM and $negneg$-elimination to be equivalent. Perhaps in this specific formalism the principle of explosion is not a given.
– Mees de Vries
Nov 19 at 15:23












@MeesdeVries I believe intuitionistic logic merely disallows LEM and $lnot lnot$ elimination but allows the principle of explosion (which is baked into its system without proof)
– Brandon L
Nov 19 at 15:30






@MeesdeVries I believe intuitionistic logic merely disallows LEM and $lnot lnot$ elimination but allows the principle of explosion (which is baked into its system without proof)
– Brandon L
Nov 19 at 15:30














In your proof you have used the principle : $(p to q) to ((p to lnot q) to lnot p)$ that is equivalent (in a system without $bot$) to $lnot$-intro : $(p to bot) vdash lnot p$
– Mauro ALLEGRANZA
Nov 19 at 15:56






In your proof you have used the principle : $(p to q) to ((p to lnot q) to lnot p)$ that is equivalent (in a system without $bot$) to $lnot$-intro : $(p to bot) vdash lnot p$
– Mauro ALLEGRANZA
Nov 19 at 15:56














@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
Nov 19 at 16:01






@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
Nov 19 at 16:01














LEM and DN are equivalent and they are both not allowed in Intuitionsitic Logic; but this one use $bot to p$. Thus the first two are not equivalent to $bot to p$.
– Mauro ALLEGRANZA
Nov 19 at 16:16




LEM and DN are equivalent and they are both not allowed in Intuitionsitic Logic; but this one use $bot to p$. Thus the first two are not equivalent to $bot to p$.
– Mauro ALLEGRANZA
Nov 19 at 16:16










1 Answer
1






active

oldest

votes

















up vote
3
down vote













You can have a logical system with double-negation elimination and without explosion.



And you can have logical system where excluded middle and double-negation elimination are provably equivalent without the use of explosion.



The classical version of Neil Tennant's Core Logic (a sort of relevant logic) is a case in point.



Which just goes to show that the rules are not interdependent in quite the way you claim. What's happening is that you are smuggling in other albeit standard assumptions (e.g. about the correct formulation of the or-elimination rule).



Of course, in a standard classical framework, things fit together rather as you say (indeed explosion can be a derived rule).






share|cite|improve this answer





















  • I don't really understand this answer at all. If our system has double negation elimination and no explosion, how is that enforced if I can re-derive explosion with double negation elimination?
    – Brandon L
    Nov 19 at 15:49












  • And how are the rules not interdependent simply due to things like or elimination? As far as I can tell that's an entirely standard rule in virtually all systems, $p lor q, (p vdash r), (q vdash r) vdash r$. In what way is this "smuggling" non-interdependence?
    – Brandon L
    Nov 19 at 15:51












  • On or-elimination, an alternative rule is from $alpha lor beta$ and a proof from $alpha$ to one of $gamma$ or $bot$ and a proof from $beta$ to one of $gamma$ or $bot$, derive $bot$ if both subproofs end in $bot$ or else $gamma$. This is arguably a more intuitive rule ("if one disjunct leads to absurdity, go with the other!"), and gives us a proof of $negneg p$ from $p$, assuming excluded middle, without explosion.
    – Peter Smith
    Nov 19 at 16:02












  • I don't understand what you mean by that -- can you provide an example using this rule? I'm not sure what "a proof from α to γ or ⊥" means or "if one disjunct leads to absurdity, go with the other!" or how this is nevertheless done without explosion.
    – Brandon L
    Nov 19 at 16:05












  • See logicmatters.net/2017/09/30/…
    – Peter Smith
    Nov 19 at 16:07











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',
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
});


}
});














draft saved

draft discarded


















StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3005053%2fcircularity-of-lem-principle-of-explosion-and-lnot-lnot-elimination%23new-answer', 'question_page');
}
);

Post as a guest















Required, but never shown

























1 Answer
1






active

oldest

votes








1 Answer
1






active

oldest

votes









active

oldest

votes






active

oldest

votes








up vote
3
down vote













You can have a logical system with double-negation elimination and without explosion.



And you can have logical system where excluded middle and double-negation elimination are provably equivalent without the use of explosion.



The classical version of Neil Tennant's Core Logic (a sort of relevant logic) is a case in point.



Which just goes to show that the rules are not interdependent in quite the way you claim. What's happening is that you are smuggling in other albeit standard assumptions (e.g. about the correct formulation of the or-elimination rule).



Of course, in a standard classical framework, things fit together rather as you say (indeed explosion can be a derived rule).






share|cite|improve this answer





















  • I don't really understand this answer at all. If our system has double negation elimination and no explosion, how is that enforced if I can re-derive explosion with double negation elimination?
    – Brandon L
    Nov 19 at 15:49












  • And how are the rules not interdependent simply due to things like or elimination? As far as I can tell that's an entirely standard rule in virtually all systems, $p lor q, (p vdash r), (q vdash r) vdash r$. In what way is this "smuggling" non-interdependence?
    – Brandon L
    Nov 19 at 15:51












  • On or-elimination, an alternative rule is from $alpha lor beta$ and a proof from $alpha$ to one of $gamma$ or $bot$ and a proof from $beta$ to one of $gamma$ or $bot$, derive $bot$ if both subproofs end in $bot$ or else $gamma$. This is arguably a more intuitive rule ("if one disjunct leads to absurdity, go with the other!"), and gives us a proof of $negneg p$ from $p$, assuming excluded middle, without explosion.
    – Peter Smith
    Nov 19 at 16:02












  • I don't understand what you mean by that -- can you provide an example using this rule? I'm not sure what "a proof from α to γ or ⊥" means or "if one disjunct leads to absurdity, go with the other!" or how this is nevertheless done without explosion.
    – Brandon L
    Nov 19 at 16:05












  • See logicmatters.net/2017/09/30/…
    – Peter Smith
    Nov 19 at 16:07















up vote
3
down vote













You can have a logical system with double-negation elimination and without explosion.



And you can have logical system where excluded middle and double-negation elimination are provably equivalent without the use of explosion.



The classical version of Neil Tennant's Core Logic (a sort of relevant logic) is a case in point.



Which just goes to show that the rules are not interdependent in quite the way you claim. What's happening is that you are smuggling in other albeit standard assumptions (e.g. about the correct formulation of the or-elimination rule).



Of course, in a standard classical framework, things fit together rather as you say (indeed explosion can be a derived rule).






share|cite|improve this answer





















  • I don't really understand this answer at all. If our system has double negation elimination and no explosion, how is that enforced if I can re-derive explosion with double negation elimination?
    – Brandon L
    Nov 19 at 15:49












  • And how are the rules not interdependent simply due to things like or elimination? As far as I can tell that's an entirely standard rule in virtually all systems, $p lor q, (p vdash r), (q vdash r) vdash r$. In what way is this "smuggling" non-interdependence?
    – Brandon L
    Nov 19 at 15:51












  • On or-elimination, an alternative rule is from $alpha lor beta$ and a proof from $alpha$ to one of $gamma$ or $bot$ and a proof from $beta$ to one of $gamma$ or $bot$, derive $bot$ if both subproofs end in $bot$ or else $gamma$. This is arguably a more intuitive rule ("if one disjunct leads to absurdity, go with the other!"), and gives us a proof of $negneg p$ from $p$, assuming excluded middle, without explosion.
    – Peter Smith
    Nov 19 at 16:02












  • I don't understand what you mean by that -- can you provide an example using this rule? I'm not sure what "a proof from α to γ or ⊥" means or "if one disjunct leads to absurdity, go with the other!" or how this is nevertheless done without explosion.
    – Brandon L
    Nov 19 at 16:05












  • See logicmatters.net/2017/09/30/…
    – Peter Smith
    Nov 19 at 16:07













up vote
3
down vote










up vote
3
down vote









You can have a logical system with double-negation elimination and without explosion.



And you can have logical system where excluded middle and double-negation elimination are provably equivalent without the use of explosion.



The classical version of Neil Tennant's Core Logic (a sort of relevant logic) is a case in point.



Which just goes to show that the rules are not interdependent in quite the way you claim. What's happening is that you are smuggling in other albeit standard assumptions (e.g. about the correct formulation of the or-elimination rule).



Of course, in a standard classical framework, things fit together rather as you say (indeed explosion can be a derived rule).






share|cite|improve this answer












You can have a logical system with double-negation elimination and without explosion.



And you can have logical system where excluded middle and double-negation elimination are provably equivalent without the use of explosion.



The classical version of Neil Tennant's Core Logic (a sort of relevant logic) is a case in point.



Which just goes to show that the rules are not interdependent in quite the way you claim. What's happening is that you are smuggling in other albeit standard assumptions (e.g. about the correct formulation of the or-elimination rule).



Of course, in a standard classical framework, things fit together rather as you say (indeed explosion can be a derived rule).







share|cite|improve this answer












share|cite|improve this answer



share|cite|improve this answer










answered Nov 19 at 15:39









Peter Smith

40.4k339118




40.4k339118












  • I don't really understand this answer at all. If our system has double negation elimination and no explosion, how is that enforced if I can re-derive explosion with double negation elimination?
    – Brandon L
    Nov 19 at 15:49












  • And how are the rules not interdependent simply due to things like or elimination? As far as I can tell that's an entirely standard rule in virtually all systems, $p lor q, (p vdash r), (q vdash r) vdash r$. In what way is this "smuggling" non-interdependence?
    – Brandon L
    Nov 19 at 15:51












  • On or-elimination, an alternative rule is from $alpha lor beta$ and a proof from $alpha$ to one of $gamma$ or $bot$ and a proof from $beta$ to one of $gamma$ or $bot$, derive $bot$ if both subproofs end in $bot$ or else $gamma$. This is arguably a more intuitive rule ("if one disjunct leads to absurdity, go with the other!"), and gives us a proof of $negneg p$ from $p$, assuming excluded middle, without explosion.
    – Peter Smith
    Nov 19 at 16:02












  • I don't understand what you mean by that -- can you provide an example using this rule? I'm not sure what "a proof from α to γ or ⊥" means or "if one disjunct leads to absurdity, go with the other!" or how this is nevertheless done without explosion.
    – Brandon L
    Nov 19 at 16:05












  • See logicmatters.net/2017/09/30/…
    – Peter Smith
    Nov 19 at 16:07


















  • I don't really understand this answer at all. If our system has double negation elimination and no explosion, how is that enforced if I can re-derive explosion with double negation elimination?
    – Brandon L
    Nov 19 at 15:49












  • And how are the rules not interdependent simply due to things like or elimination? As far as I can tell that's an entirely standard rule in virtually all systems, $p lor q, (p vdash r), (q vdash r) vdash r$. In what way is this "smuggling" non-interdependence?
    – Brandon L
    Nov 19 at 15:51












  • On or-elimination, an alternative rule is from $alpha lor beta$ and a proof from $alpha$ to one of $gamma$ or $bot$ and a proof from $beta$ to one of $gamma$ or $bot$, derive $bot$ if both subproofs end in $bot$ or else $gamma$. This is arguably a more intuitive rule ("if one disjunct leads to absurdity, go with the other!"), and gives us a proof of $negneg p$ from $p$, assuming excluded middle, without explosion.
    – Peter Smith
    Nov 19 at 16:02












  • I don't understand what you mean by that -- can you provide an example using this rule? I'm not sure what "a proof from α to γ or ⊥" means or "if one disjunct leads to absurdity, go with the other!" or how this is nevertheless done without explosion.
    – Brandon L
    Nov 19 at 16:05












  • See logicmatters.net/2017/09/30/…
    – Peter Smith
    Nov 19 at 16:07
















I don't really understand this answer at all. If our system has double negation elimination and no explosion, how is that enforced if I can re-derive explosion with double negation elimination?
– Brandon L
Nov 19 at 15:49






I don't really understand this answer at all. If our system has double negation elimination and no explosion, how is that enforced if I can re-derive explosion with double negation elimination?
– Brandon L
Nov 19 at 15:49














And how are the rules not interdependent simply due to things like or elimination? As far as I can tell that's an entirely standard rule in virtually all systems, $p lor q, (p vdash r), (q vdash r) vdash r$. In what way is this "smuggling" non-interdependence?
– Brandon L
Nov 19 at 15:51






And how are the rules not interdependent simply due to things like or elimination? As far as I can tell that's an entirely standard rule in virtually all systems, $p lor q, (p vdash r), (q vdash r) vdash r$. In what way is this "smuggling" non-interdependence?
– Brandon L
Nov 19 at 15:51














On or-elimination, an alternative rule is from $alpha lor beta$ and a proof from $alpha$ to one of $gamma$ or $bot$ and a proof from $beta$ to one of $gamma$ or $bot$, derive $bot$ if both subproofs end in $bot$ or else $gamma$. This is arguably a more intuitive rule ("if one disjunct leads to absurdity, go with the other!"), and gives us a proof of $negneg p$ from $p$, assuming excluded middle, without explosion.
– Peter Smith
Nov 19 at 16:02






On or-elimination, an alternative rule is from $alpha lor beta$ and a proof from $alpha$ to one of $gamma$ or $bot$ and a proof from $beta$ to one of $gamma$ or $bot$, derive $bot$ if both subproofs end in $bot$ or else $gamma$. This is arguably a more intuitive rule ("if one disjunct leads to absurdity, go with the other!"), and gives us a proof of $negneg p$ from $p$, assuming excluded middle, without explosion.
– Peter Smith
Nov 19 at 16:02














I don't understand what you mean by that -- can you provide an example using this rule? I'm not sure what "a proof from α to γ or ⊥" means or "if one disjunct leads to absurdity, go with the other!" or how this is nevertheless done without explosion.
– Brandon L
Nov 19 at 16:05






I don't understand what you mean by that -- can you provide an example using this rule? I'm not sure what "a proof from α to γ or ⊥" means or "if one disjunct leads to absurdity, go with the other!" or how this is nevertheless done without explosion.
– Brandon L
Nov 19 at 16:05














See logicmatters.net/2017/09/30/…
– Peter Smith
Nov 19 at 16:07




See logicmatters.net/2017/09/30/…
– Peter Smith
Nov 19 at 16:07


















draft saved

draft discarded




















































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.




draft saved


draft discarded














StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3005053%2fcircularity-of-lem-principle-of-explosion-and-lnot-lnot-elimination%23new-answer', 'question_page');
}
);

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







Popular posts from this blog

Plaza Victoria

Puebla de Zaragoza

Musa