Mixing
Circularity of LEM, principle of explosion, and $lnot lnot$ elimination
up vote
2
down vote
favorite
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
asked yesterday
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
|
show 5 more comments
up vote
2
down vote
favorite
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
asked yesterday
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
yesterday
@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
yesterday
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
yesterday
@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
yesterday
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
yesterday
|
show 5 more comments
up vote
2
down vote
favorite
up vote
2
down vote
favorite
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
asked yesterday
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
logic proof-explanation propositional-calculus
asked yesterday
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked yesterday
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited yesterday
asked yesterday
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked yesterday
Brandon L
184
asked yesterday
Brandon L
184
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
yesterday
@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
yesterday
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
yesterday
@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
yesterday
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
yesterday
|
show 5 more comments
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
yesterday
@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
yesterday
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
yesterday
@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
yesterday
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
yesterday
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
yesterday
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
yesterday
@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
yesterday
@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
yesterday
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
yesterday
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
yesterday
@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
yesterday
@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
yesterday
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
yesterday
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
yesterday
|
show 5 more comments
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).
answered yesterday
Peter Smith
40.1k339118
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
yesterday
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
yesterday
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
yesterday
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
yesterday
See logicmatters.net/2017/09/30/…
– Peter Smith
yesterday
|
show 6 more comments
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).
answered yesterday
Peter Smith
40.1k339118
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
yesterday
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
yesterday
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
yesterday
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
yesterday
See logicmatters.net/2017/09/30/…
– Peter Smith
yesterday
|
show 6 more comments
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).
answered yesterday
Peter Smith
40.1k339118
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
yesterday
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
yesterday
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
yesterday
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
yesterday
See logicmatters.net/2017/09/30/…
– Peter Smith
yesterday
|
show 6 more comments
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).
answered yesterday
Peter Smith
40.1k339118
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).
answered yesterday
Peter Smith
40.1k339118
answered yesterday
Peter Smith
40.1k339118
answered yesterday
Peter Smith
40.1k339118
answered yesterday
Peter Smith
40.1k339118
40.1k339118
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
yesterday
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
yesterday
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
yesterday
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
yesterday
See logicmatters.net/2017/09/30/…
– Peter Smith
yesterday
|
show 6 more comments
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
yesterday
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
yesterday
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
yesterday
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
yesterday
See logicmatters.net/2017/09/30/…
– Peter Smith
yesterday
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
yesterday
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
yesterday
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
yesterday
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
yesterday
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
yesterday
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
yesterday
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
yesterday
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
yesterday
See logicmatters.net/2017/09/30/…
– Peter Smith
yesterday
See logicmatters.net/2017/09/30/…
– Peter Smith
yesterday
|
show 6 more comments
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
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%2f3005053%2fcircularity-of-lem-principle-of-explosion-and-lnot-lnot-elimination%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
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
yesterday
@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
yesterday
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
yesterday
@MauroALLEGRANZA I agree, but how is this relevant to the question? Principle of explosion is $bot to p$
– Brandon L
yesterday
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
yesterday