Mixing
Why is the principle of explosion accepted in constructive mathematics?
Clash Royale CLAN TAG#URR8PPP
up vote
5
down vote
favorite
I think something is wrong with the principle of explosion, because according to it, if I know $Pwedge lnot P$, I can deduce $Q$ though I don't know anything about $Q$.
Is it really constructive to decide whether $Q$ is true by only seeing $P$ unrelated to $Q$? If $Pwedge lnot P$ holds, how do I construct a reason for $Q$ ?
logic foundations constructive-mathematics
asked 7 hours ago
marimo
1345
add a comment |Â
up vote
5
down vote
favorite
I think something is wrong with the principle of explosion, because according to it, if I know $Pwedge lnot P$, I can deduce $Q$ though I don't know anything about $Q$.
Is it really constructive to decide whether $Q$ is true by only seeing $P$ unrelated to $Q$? If $Pwedge lnot P$ holds, how do I construct a reason for $Q$ ?
logic foundations constructive-mathematics
asked 7 hours ago
marimo
1345
3
You don't know $Q$ is true, you know $(P land lnot P) to Q$ which is a much weaker statement. It in fact contains zero knowledge because you won't be able to prove $(P land lnot P)$.
– DanielV
7 hours ago
add a comment |Â
up vote
5
down vote
favorite
up vote
5
down vote
favorite
I think something is wrong with the principle of explosion, because according to it, if I know $Pwedge lnot P$, I can deduce $Q$ though I don't know anything about $Q$.
Is it really constructive to decide whether $Q$ is true by only seeing $P$ unrelated to $Q$? If $Pwedge lnot P$ holds, how do I construct a reason for $Q$ ?
logic foundations constructive-mathematics
asked 7 hours ago
marimo
1345
I think something is wrong with the principle of explosion, because according to it, if I know $Pwedge lnot P$, I can deduce $Q$ though I don't know anything about $Q$.
Is it really constructive to decide whether $Q$ is true by only seeing $P$ unrelated to $Q$? If $Pwedge lnot P$ holds, how do I construct a reason for $Q$ ?
logic foundations constructive-mathematics
logic foundations constructive-mathematics
asked 7 hours ago
marimo
1345
asked 7 hours ago
marimo
1345
asked 7 hours ago
marimo
1345
asked 7 hours ago
marimo
1345
asked 7 hours ago
marimo
1345
1345
3
You don't know $Q$ is true, you know $(P land lnot P) to Q$ which is a much weaker statement. It in fact contains zero knowledge because you won't be able to prove $(P land lnot P)$.
– DanielV
7 hours ago
add a comment |Â
3
You don't know $Q$ is true, you know $(P land lnot P) to Q$ which is a much weaker statement. It in fact contains zero knowledge because you won't be able to prove $(P land lnot P)$.
– DanielV
7 hours ago
3
3
You don't know $Q$ is true, you know $(P land lnot P) to Q$ which is a much weaker statement. It in fact contains zero knowledge because you won't be able to prove $(P land lnot P)$.
– DanielV
7 hours ago
You don't know $Q$ is true, you know $(P land lnot P) to Q$ which is a much weaker statement. It in fact contains zero knowledge because you won't be able to prove $(P land lnot P)$.
– DanielV
7 hours ago
add a comment |Â
3 Answers
3
active
oldest
votes
up vote
5
down vote
As correctly pointed out by @DanielV, the principle of explosion (aka ex falso quodlibet) just says that $(P land lnot P) to Q$ holds for any formula $Q$ (possibly unrelated to $P$).
It does not mean that $Q$ holds, but only that if $P land lnot P$ held then $Q$ (which could be anything) would hold; as in a consistent system $P land lnot P$ never holds, from the principle of explosion we cannot infer whether $Q$ holds or not.
So, the principle of explosion does not contradict constructivity, this is the reason why it is accepted in a constructive setting such as intuitionistic logic. The principle of explosion just says that if a theory contains a single inconsistency, such a theory is trivial—that is, it can prove everything.
Therefore, according to the principle of explosion, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem.
An informal justification of the principle of explosion is the following: if $P$ and its negation $lnot P$ are both assumed, then $P$ holds, from which it follows that at least one of the claims $P$ and some other (arbitrary) claim $Q$ holds. However, as we know that either $P$ or $Q$ holds, and also that $P$ does not hold (that is, $lnot P$ holds) we can conclude that $Q$ holds.
This argument is constructive, in that it is valid in classical logic as well as in intuitionistic logic.
There are logics that reject the principle of explosion: paraconsistent logics and in particular minimal logic. Such logics make it possible to distinguish between inconsistent theories and to reason with them. The idea is that it ought to be possible to reason with inconsistent information in a controlled and discriminating way, which is precluded by the principle of explosion.
For more information, see here, here and here.
answered 5 hours ago
Taroccoesbrocco
3,84951433
add a comment |Â
up vote
4
down vote
In the BHK interpretation of constructive logic, a proposition is "true" when you provide a witness for it. You get different notions of constructive logic by defining "witness" in different ways. For example, you could say a witness is a Turing machine that will compute the relevant evidence. For our purposes, let's say for each proposition we assign a set of witnesses. We don't do this arbitrarily though. For an proposition variable, we may assign a set of witnesses arbitrarily, but, in particular, for $Ato B$, we assign as the set of witnesses the function space between the set of witnesses of $A$ and the set of witnesses of $B$. All this is to say, that for this example, a witness of an implication is a (set-theoretic) function from a set of witnesses of $A$ to a set of witnesses for $B$. We also assign the empty set of witnesses to $bot$, the nullary connective for falsity corresponding to a contradiction1.
For the particular notion of "witness" just described, the principle of explosion is "true" constructively because it is witnessed. In particular, it is witnessed by the empty function. For most of the other common choices for the notion of "witness", there is some analogue of the empty function. One take on generalizing the BHK interpretation, in the case of Intuitionistic Propositional Logic (IPL), is saying that we have a Heyting category of witnesses and the BHK interpretation is a Heyting functor from the (thin) syntactic Heyting category describing IPL to that Heyting category of witnesses. Heyting categories have initial objects which represent $bot$ and the unique arrow from an initial object to any other object is the generalization of the empty function. Whenever our category of witnesses has an initial object (that's well-behaved in a certain sense and we also have some other "structural" stuff), then we can interpret the $bot$ connective. Having the $bot$ connective means having the principle of explosion in the form $botvdashvarphi$ for all $varphi$.
Of course, we could just drop $bot$ and weaken the requirement that the category of witnesses be Heyting and that we have a Heyting functor to not include the initial object stuff. That's a completely reasonable thing to do and will lead to a paraconsistent logic such as minimal logic. It's not so much "do we support the principle of explosion" as "do we have (something equivalent to) the $bot$ connective". However, dropping $bot$ means we need a different story for negation, $neg$, or dropping we need to drop negation entirely. For intuitionistic logics, negation is usually defined as $negvarphiequivvarphitobot$.
1 I strongly recommend providing $bot$ as a primitive connective (for logics where contradictions make sense). Always talking about $Plandneg P$ is tedious and kind of hacky. Why do I need to arbitrarily choose some irrelevant proposition $P$ just to talk about a fundamental concept like contradiction?
answered 5 hours ago
Derek Elkins
15.4k11035
add a comment |Â
up vote
3
down vote
Here's one way to look at it. Suppose we're working in a natural deduction system with a $lor$-elimination rule that goes
$$ fracGammavdash Plor Q qquad Gamma, Pvdash R qquad Gamma, Qvdash RGammavdash R $$
This allows us to prove things by case analysis once we have proved a $lor$ that tells us we have to be in one of the cases.
Now, what is the fundamental thing knowing $neg P$ tells us? Arguably it is that in the above rule we won't need to carry out the $Gamma, Pvdash R$ part of the proof because $P$ cannot actually happen.
We could achieve that by having a bunch of specialized $lor$-elimination rules such as
$$ fracGammavdash Plor Q qquad Gamma, Pvdash A qquad Gammavdashneg A qquad Gamma, Qvdash RGammavdash R $$
but it is simpler to wrap all the variants up in a single rule that says:
If you find yourself in a branch of a proof where two contradictory things appear to hold, it means that proof branch was not actually necessary, and you can cancel it completely by pretending you've already proved whatever you were aiming for in that branch.
That's basically what the principle of explosion does.
It is constructively acceptible because intuitively there are only two ways it's ever possible to use it:
Either your initial assumptions in the proof are impossible to satisfy. Then we don't really care if we conclude nonsense. What we do care is that if our assumptions hold then the conclusion will also hold. Otherwise we're happy with garbage-in, garbage-out.
Or you have introduced an additional temporary assumption somewhere in the proof tree which creates the contradiction. For example, the $Gamma,Pvdash R$ premise in our $lor$-elimination rule does that. Then we can justify the use of explosion by arguing that the branch that the explosion happened in was not actually necessary because the conditions it would be relevant in cannot happen.
If the additional assumption came from an introduction rule such as $to$-introduction, the argument that "this branch is not needed" is not as immediately convincing. However, in that case we can argue that we're still "constructively safe", because then our conclusion of that introduction rule is something that involves $to$. And the only way we can use that result is by using it in modus ponens (aka $to$-elimination). At that time someone will be claiming they can prove the antecedent of the $to$, but we know that is not actually realistic because the assumption leads to a contradiction! So this tells us that the proof branch where the modus ponens is found will itself be an unneeded branch, so constructively we don't need to worry about shenanigans there. It will never be executed.
The story for $neg$-introduction is similar to that for $to$-introduction; then the principle of explosion itself is the relevant elimination rule.
answered 1 hour ago
Henning Makholm
231k16297529
add a comment |Â
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
5
down vote
As correctly pointed out by @DanielV, the principle of explosion (aka ex falso quodlibet) just says that $(P land lnot P) to Q$ holds for any formula $Q$ (possibly unrelated to $P$).
It does not mean that $Q$ holds, but only that if $P land lnot P$ held then $Q$ (which could be anything) would hold; as in a consistent system $P land lnot P$ never holds, from the principle of explosion we cannot infer whether $Q$ holds or not.
So, the principle of explosion does not contradict constructivity, this is the reason why it is accepted in a constructive setting such as intuitionistic logic. The principle of explosion just says that if a theory contains a single inconsistency, such a theory is trivial—that is, it can prove everything.
Therefore, according to the principle of explosion, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem.
An informal justification of the principle of explosion is the following: if $P$ and its negation $lnot P$ are both assumed, then $P$ holds, from which it follows that at least one of the claims $P$ and some other (arbitrary) claim $Q$ holds. However, as we know that either $P$ or $Q$ holds, and also that $P$ does not hold (that is, $lnot P$ holds) we can conclude that $Q$ holds.
This argument is constructive, in that it is valid in classical logic as well as in intuitionistic logic.
There are logics that reject the principle of explosion: paraconsistent logics and in particular minimal logic. Such logics make it possible to distinguish between inconsistent theories and to reason with them. The idea is that it ought to be possible to reason with inconsistent information in a controlled and discriminating way, which is precluded by the principle of explosion.
For more information, see here, here and here.
answered 5 hours ago
Taroccoesbrocco
3,84951433
add a comment |Â
up vote
5
down vote
As correctly pointed out by @DanielV, the principle of explosion (aka ex falso quodlibet) just says that $(P land lnot P) to Q$ holds for any formula $Q$ (possibly unrelated to $P$).
It does not mean that $Q$ holds, but only that if $P land lnot P$ held then $Q$ (which could be anything) would hold; as in a consistent system $P land lnot P$ never holds, from the principle of explosion we cannot infer whether $Q$ holds or not.
So, the principle of explosion does not contradict constructivity, this is the reason why it is accepted in a constructive setting such as intuitionistic logic. The principle of explosion just says that if a theory contains a single inconsistency, such a theory is trivial—that is, it can prove everything.
Therefore, according to the principle of explosion, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem.
An informal justification of the principle of explosion is the following: if $P$ and its negation $lnot P$ are both assumed, then $P$ holds, from which it follows that at least one of the claims $P$ and some other (arbitrary) claim $Q$ holds. However, as we know that either $P$ or $Q$ holds, and also that $P$ does not hold (that is, $lnot P$ holds) we can conclude that $Q$ holds.
This argument is constructive, in that it is valid in classical logic as well as in intuitionistic logic.
There are logics that reject the principle of explosion: paraconsistent logics and in particular minimal logic. Such logics make it possible to distinguish between inconsistent theories and to reason with them. The idea is that it ought to be possible to reason with inconsistent information in a controlled and discriminating way, which is precluded by the principle of explosion.
For more information, see here, here and here.
answered 5 hours ago
Taroccoesbrocco
3,84951433
add a comment |Â
up vote
5
down vote
up vote
5
down vote
As correctly pointed out by @DanielV, the principle of explosion (aka ex falso quodlibet) just says that $(P land lnot P) to Q$ holds for any formula $Q$ (possibly unrelated to $P$).
It does not mean that $Q$ holds, but only that if $P land lnot P$ held then $Q$ (which could be anything) would hold; as in a consistent system $P land lnot P$ never holds, from the principle of explosion we cannot infer whether $Q$ holds or not.
So, the principle of explosion does not contradict constructivity, this is the reason why it is accepted in a constructive setting such as intuitionistic logic. The principle of explosion just says that if a theory contains a single inconsistency, such a theory is trivial—that is, it can prove everything.
Therefore, according to the principle of explosion, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem.
An informal justification of the principle of explosion is the following: if $P$ and its negation $lnot P$ are both assumed, then $P$ holds, from which it follows that at least one of the claims $P$ and some other (arbitrary) claim $Q$ holds. However, as we know that either $P$ or $Q$ holds, and also that $P$ does not hold (that is, $lnot P$ holds) we can conclude that $Q$ holds.
This argument is constructive, in that it is valid in classical logic as well as in intuitionistic logic.
There are logics that reject the principle of explosion: paraconsistent logics and in particular minimal logic. Such logics make it possible to distinguish between inconsistent theories and to reason with them. The idea is that it ought to be possible to reason with inconsistent information in a controlled and discriminating way, which is precluded by the principle of explosion.
For more information, see here, here and here.
answered 5 hours ago
Taroccoesbrocco
3,84951433
As correctly pointed out by @DanielV, the principle of explosion (aka ex falso quodlibet) just says that $(P land lnot P) to Q$ holds for any formula $Q$ (possibly unrelated to $P$).
It does not mean that $Q$ holds, but only that if $P land lnot P$ held then $Q$ (which could be anything) would hold; as in a consistent system $P land lnot P$ never holds, from the principle of explosion we cannot infer whether $Q$ holds or not.
So, the principle of explosion does not contradict constructivity, this is the reason why it is accepted in a constructive setting such as intuitionistic logic. The principle of explosion just says that if a theory contains a single inconsistency, such a theory is trivial—that is, it can prove everything.
Therefore, according to the principle of explosion, there is only one inconsistent theory: the trivial theory that has every sentence as a theorem.
An informal justification of the principle of explosion is the following: if $P$ and its negation $lnot P$ are both assumed, then $P$ holds, from which it follows that at least one of the claims $P$ and some other (arbitrary) claim $Q$ holds. However, as we know that either $P$ or $Q$ holds, and also that $P$ does not hold (that is, $lnot P$ holds) we can conclude that $Q$ holds.
This argument is constructive, in that it is valid in classical logic as well as in intuitionistic logic.
There are logics that reject the principle of explosion: paraconsistent logics and in particular minimal logic. Such logics make it possible to distinguish between inconsistent theories and to reason with them. The idea is that it ought to be possible to reason with inconsistent information in a controlled and discriminating way, which is precluded by the principle of explosion.
For more information, see here, here and here.
answered 5 hours ago
Taroccoesbrocco
3,84951433
edited 1 hour ago
answered 5 hours ago
Taroccoesbrocco
3,84951433
answered 5 hours ago
Taroccoesbrocco
3,84951433
answered 5 hours ago
Taroccoesbrocco
3,84951433
3,84951433
add a comment |Â
add a comment |Â
up vote
4
down vote
In the BHK interpretation of constructive logic, a proposition is "true" when you provide a witness for it. You get different notions of constructive logic by defining "witness" in different ways. For example, you could say a witness is a Turing machine that will compute the relevant evidence. For our purposes, let's say for each proposition we assign a set of witnesses. We don't do this arbitrarily though. For an proposition variable, we may assign a set of witnesses arbitrarily, but, in particular, for $Ato B$, we assign as the set of witnesses the function space between the set of witnesses of $A$ and the set of witnesses of $B$. All this is to say, that for this example, a witness of an implication is a (set-theoretic) function from a set of witnesses of $A$ to a set of witnesses for $B$. We also assign the empty set of witnesses to $bot$, the nullary connective for falsity corresponding to a contradiction1.
For the particular notion of "witness" just described, the principle of explosion is "true" constructively because it is witnessed. In particular, it is witnessed by the empty function. For most of the other common choices for the notion of "witness", there is some analogue of the empty function. One take on generalizing the BHK interpretation, in the case of Intuitionistic Propositional Logic (IPL), is saying that we have a Heyting category of witnesses and the BHK interpretation is a Heyting functor from the (thin) syntactic Heyting category describing IPL to that Heyting category of witnesses. Heyting categories have initial objects which represent $bot$ and the unique arrow from an initial object to any other object is the generalization of the empty function. Whenever our category of witnesses has an initial object (that's well-behaved in a certain sense and we also have some other "structural" stuff), then we can interpret the $bot$ connective. Having the $bot$ connective means having the principle of explosion in the form $botvdashvarphi$ for all $varphi$.
Of course, we could just drop $bot$ and weaken the requirement that the category of witnesses be Heyting and that we have a Heyting functor to not include the initial object stuff. That's a completely reasonable thing to do and will lead to a paraconsistent logic such as minimal logic. It's not so much "do we support the principle of explosion" as "do we have (something equivalent to) the $bot$ connective". However, dropping $bot$ means we need a different story for negation, $neg$, or dropping we need to drop negation entirely. For intuitionistic logics, negation is usually defined as $negvarphiequivvarphitobot$.
1 I strongly recommend providing $bot$ as a primitive connective (for logics where contradictions make sense). Always talking about $Plandneg P$ is tedious and kind of hacky. Why do I need to arbitrarily choose some irrelevant proposition $P$ just to talk about a fundamental concept like contradiction?
answered 5 hours ago
Derek Elkins
15.4k11035
add a comment |Â
up vote
4
down vote
In the BHK interpretation of constructive logic, a proposition is "true" when you provide a witness for it. You get different notions of constructive logic by defining "witness" in different ways. For example, you could say a witness is a Turing machine that will compute the relevant evidence. For our purposes, let's say for each proposition we assign a set of witnesses. We don't do this arbitrarily though. For an proposition variable, we may assign a set of witnesses arbitrarily, but, in particular, for $Ato B$, we assign as the set of witnesses the function space between the set of witnesses of $A$ and the set of witnesses of $B$. All this is to say, that for this example, a witness of an implication is a (set-theoretic) function from a set of witnesses of $A$ to a set of witnesses for $B$. We also assign the empty set of witnesses to $bot$, the nullary connective for falsity corresponding to a contradiction1.
For the particular notion of "witness" just described, the principle of explosion is "true" constructively because it is witnessed. In particular, it is witnessed by the empty function. For most of the other common choices for the notion of "witness", there is some analogue of the empty function. One take on generalizing the BHK interpretation, in the case of Intuitionistic Propositional Logic (IPL), is saying that we have a Heyting category of witnesses and the BHK interpretation is a Heyting functor from the (thin) syntactic Heyting category describing IPL to that Heyting category of witnesses. Heyting categories have initial objects which represent $bot$ and the unique arrow from an initial object to any other object is the generalization of the empty function. Whenever our category of witnesses has an initial object (that's well-behaved in a certain sense and we also have some other "structural" stuff), then we can interpret the $bot$ connective. Having the $bot$ connective means having the principle of explosion in the form $botvdashvarphi$ for all $varphi$.
Of course, we could just drop $bot$ and weaken the requirement that the category of witnesses be Heyting and that we have a Heyting functor to not include the initial object stuff. That's a completely reasonable thing to do and will lead to a paraconsistent logic such as minimal logic. It's not so much "do we support the principle of explosion" as "do we have (something equivalent to) the $bot$ connective". However, dropping $bot$ means we need a different story for negation, $neg$, or dropping we need to drop negation entirely. For intuitionistic logics, negation is usually defined as $negvarphiequivvarphitobot$.
1 I strongly recommend providing $bot$ as a primitive connective (for logics where contradictions make sense). Always talking about $Plandneg P$ is tedious and kind of hacky. Why do I need to arbitrarily choose some irrelevant proposition $P$ just to talk about a fundamental concept like contradiction?
answered 5 hours ago
Derek Elkins
15.4k11035
add a comment |Â
up vote
4
down vote
up vote
4
down vote
In the BHK interpretation of constructive logic, a proposition is "true" when you provide a witness for it. You get different notions of constructive logic by defining "witness" in different ways. For example, you could say a witness is a Turing machine that will compute the relevant evidence. For our purposes, let's say for each proposition we assign a set of witnesses. We don't do this arbitrarily though. For an proposition variable, we may assign a set of witnesses arbitrarily, but, in particular, for $Ato B$, we assign as the set of witnesses the function space between the set of witnesses of $A$ and the set of witnesses of $B$. All this is to say, that for this example, a witness of an implication is a (set-theoretic) function from a set of witnesses of $A$ to a set of witnesses for $B$. We also assign the empty set of witnesses to $bot$, the nullary connective for falsity corresponding to a contradiction1.
For the particular notion of "witness" just described, the principle of explosion is "true" constructively because it is witnessed. In particular, it is witnessed by the empty function. For most of the other common choices for the notion of "witness", there is some analogue of the empty function. One take on generalizing the BHK interpretation, in the case of Intuitionistic Propositional Logic (IPL), is saying that we have a Heyting category of witnesses and the BHK interpretation is a Heyting functor from the (thin) syntactic Heyting category describing IPL to that Heyting category of witnesses. Heyting categories have initial objects which represent $bot$ and the unique arrow from an initial object to any other object is the generalization of the empty function. Whenever our category of witnesses has an initial object (that's well-behaved in a certain sense and we also have some other "structural" stuff), then we can interpret the $bot$ connective. Having the $bot$ connective means having the principle of explosion in the form $botvdashvarphi$ for all $varphi$.
Of course, we could just drop $bot$ and weaken the requirement that the category of witnesses be Heyting and that we have a Heyting functor to not include the initial object stuff. That's a completely reasonable thing to do and will lead to a paraconsistent logic such as minimal logic. It's not so much "do we support the principle of explosion" as "do we have (something equivalent to) the $bot$ connective". However, dropping $bot$ means we need a different story for negation, $neg$, or dropping we need to drop negation entirely. For intuitionistic logics, negation is usually defined as $negvarphiequivvarphitobot$.
1 I strongly recommend providing $bot$ as a primitive connective (for logics where contradictions make sense). Always talking about $Plandneg P$ is tedious and kind of hacky. Why do I need to arbitrarily choose some irrelevant proposition $P$ just to talk about a fundamental concept like contradiction?
answered 5 hours ago
Derek Elkins
15.4k11035
In the BHK interpretation of constructive logic, a proposition is "true" when you provide a witness for it. You get different notions of constructive logic by defining "witness" in different ways. For example, you could say a witness is a Turing machine that will compute the relevant evidence. For our purposes, let's say for each proposition we assign a set of witnesses. We don't do this arbitrarily though. For an proposition variable, we may assign a set of witnesses arbitrarily, but, in particular, for $Ato B$, we assign as the set of witnesses the function space between the set of witnesses of $A$ and the set of witnesses of $B$. All this is to say, that for this example, a witness of an implication is a (set-theoretic) function from a set of witnesses of $A$ to a set of witnesses for $B$. We also assign the empty set of witnesses to $bot$, the nullary connective for falsity corresponding to a contradiction1.
For the particular notion of "witness" just described, the principle of explosion is "true" constructively because it is witnessed. In particular, it is witnessed by the empty function. For most of the other common choices for the notion of "witness", there is some analogue of the empty function. One take on generalizing the BHK interpretation, in the case of Intuitionistic Propositional Logic (IPL), is saying that we have a Heyting category of witnesses and the BHK interpretation is a Heyting functor from the (thin) syntactic Heyting category describing IPL to that Heyting category of witnesses. Heyting categories have initial objects which represent $bot$ and the unique arrow from an initial object to any other object is the generalization of the empty function. Whenever our category of witnesses has an initial object (that's well-behaved in a certain sense and we also have some other "structural" stuff), then we can interpret the $bot$ connective. Having the $bot$ connective means having the principle of explosion in the form $botvdashvarphi$ for all $varphi$.
Of course, we could just drop $bot$ and weaken the requirement that the category of witnesses be Heyting and that we have a Heyting functor to not include the initial object stuff. That's a completely reasonable thing to do and will lead to a paraconsistent logic such as minimal logic. It's not so much "do we support the principle of explosion" as "do we have (something equivalent to) the $bot$ connective". However, dropping $bot$ means we need a different story for negation, $neg$, or dropping we need to drop negation entirely. For intuitionistic logics, negation is usually defined as $negvarphiequivvarphitobot$.
1 I strongly recommend providing $bot$ as a primitive connective (for logics where contradictions make sense). Always talking about $Plandneg P$ is tedious and kind of hacky. Why do I need to arbitrarily choose some irrelevant proposition $P$ just to talk about a fundamental concept like contradiction?
answered 5 hours ago
Derek Elkins
15.4k11035
answered 5 hours ago
Derek Elkins
15.4k11035
answered 5 hours ago
Derek Elkins
15.4k11035
answered 5 hours ago
Derek Elkins
15.4k11035
15.4k11035
add a comment |Â
add a comment |Â
up vote
3
down vote
Here's one way to look at it. Suppose we're working in a natural deduction system with a $lor$-elimination rule that goes
$$ fracGammavdash Plor Q qquad Gamma, Pvdash R qquad Gamma, Qvdash RGammavdash R $$
This allows us to prove things by case analysis once we have proved a $lor$ that tells us we have to be in one of the cases.
Now, what is the fundamental thing knowing $neg P$ tells us? Arguably it is that in the above rule we won't need to carry out the $Gamma, Pvdash R$ part of the proof because $P$ cannot actually happen.
We could achieve that by having a bunch of specialized $lor$-elimination rules such as
$$ fracGammavdash Plor Q qquad Gamma, Pvdash A qquad Gammavdashneg A qquad Gamma, Qvdash RGammavdash R $$
but it is simpler to wrap all the variants up in a single rule that says:
If you find yourself in a branch of a proof where two contradictory things appear to hold, it means that proof branch was not actually necessary, and you can cancel it completely by pretending you've already proved whatever you were aiming for in that branch.
That's basically what the principle of explosion does.
It is constructively acceptible because intuitively there are only two ways it's ever possible to use it:
Either your initial assumptions in the proof are impossible to satisfy. Then we don't really care if we conclude nonsense. What we do care is that if our assumptions hold then the conclusion will also hold. Otherwise we're happy with garbage-in, garbage-out.
Or you have introduced an additional temporary assumption somewhere in the proof tree which creates the contradiction. For example, the $Gamma,Pvdash R$ premise in our $lor$-elimination rule does that. Then we can justify the use of explosion by arguing that the branch that the explosion happened in was not actually necessary because the conditions it would be relevant in cannot happen.
If the additional assumption came from an introduction rule such as $to$-introduction, the argument that "this branch is not needed" is not as immediately convincing. However, in that case we can argue that we're still "constructively safe", because then our conclusion of that introduction rule is something that involves $to$. And the only way we can use that result is by using it in modus ponens (aka $to$-elimination). At that time someone will be claiming they can prove the antecedent of the $to$, but we know that is not actually realistic because the assumption leads to a contradiction! So this tells us that the proof branch where the modus ponens is found will itself be an unneeded branch, so constructively we don't need to worry about shenanigans there. It will never be executed.
The story for $neg$-introduction is similar to that for $to$-introduction; then the principle of explosion itself is the relevant elimination rule.
answered 1 hour ago
Henning Makholm
231k16297529
add a comment |Â
up vote
3
down vote
Here's one way to look at it. Suppose we're working in a natural deduction system with a $lor$-elimination rule that goes
$$ fracGammavdash Plor Q qquad Gamma, Pvdash R qquad Gamma, Qvdash RGammavdash R $$
This allows us to prove things by case analysis once we have proved a $lor$ that tells us we have to be in one of the cases.
Now, what is the fundamental thing knowing $neg P$ tells us? Arguably it is that in the above rule we won't need to carry out the $Gamma, Pvdash R$ part of the proof because $P$ cannot actually happen.
We could achieve that by having a bunch of specialized $lor$-elimination rules such as
$$ fracGammavdash Plor Q qquad Gamma, Pvdash A qquad Gammavdashneg A qquad Gamma, Qvdash RGammavdash R $$
but it is simpler to wrap all the variants up in a single rule that says:
If you find yourself in a branch of a proof where two contradictory things appear to hold, it means that proof branch was not actually necessary, and you can cancel it completely by pretending you've already proved whatever you were aiming for in that branch.
That's basically what the principle of explosion does.
It is constructively acceptible because intuitively there are only two ways it's ever possible to use it:
Either your initial assumptions in the proof are impossible to satisfy. Then we don't really care if we conclude nonsense. What we do care is that if our assumptions hold then the conclusion will also hold. Otherwise we're happy with garbage-in, garbage-out.
Or you have introduced an additional temporary assumption somewhere in the proof tree which creates the contradiction. For example, the $Gamma,Pvdash R$ premise in our $lor$-elimination rule does that. Then we can justify the use of explosion by arguing that the branch that the explosion happened in was not actually necessary because the conditions it would be relevant in cannot happen.
If the additional assumption came from an introduction rule such as $to$-introduction, the argument that "this branch is not needed" is not as immediately convincing. However, in that case we can argue that we're still "constructively safe", because then our conclusion of that introduction rule is something that involves $to$. And the only way we can use that result is by using it in modus ponens (aka $to$-elimination). At that time someone will be claiming they can prove the antecedent of the $to$, but we know that is not actually realistic because the assumption leads to a contradiction! So this tells us that the proof branch where the modus ponens is found will itself be an unneeded branch, so constructively we don't need to worry about shenanigans there. It will never be executed.
The story for $neg$-introduction is similar to that for $to$-introduction; then the principle of explosion itself is the relevant elimination rule.
answered 1 hour ago
Henning Makholm
231k16297529
add a comment |Â
up vote
3
down vote
up vote
3
down vote
Here's one way to look at it. Suppose we're working in a natural deduction system with a $lor$-elimination rule that goes
$$ fracGammavdash Plor Q qquad Gamma, Pvdash R qquad Gamma, Qvdash RGammavdash R $$
This allows us to prove things by case analysis once we have proved a $lor$ that tells us we have to be in one of the cases.
Now, what is the fundamental thing knowing $neg P$ tells us? Arguably it is that in the above rule we won't need to carry out the $Gamma, Pvdash R$ part of the proof because $P$ cannot actually happen.
We could achieve that by having a bunch of specialized $lor$-elimination rules such as
$$ fracGammavdash Plor Q qquad Gamma, Pvdash A qquad Gammavdashneg A qquad Gamma, Qvdash RGammavdash R $$
but it is simpler to wrap all the variants up in a single rule that says:
If you find yourself in a branch of a proof where two contradictory things appear to hold, it means that proof branch was not actually necessary, and you can cancel it completely by pretending you've already proved whatever you were aiming for in that branch.
That's basically what the principle of explosion does.
It is constructively acceptible because intuitively there are only two ways it's ever possible to use it:
Either your initial assumptions in the proof are impossible to satisfy. Then we don't really care if we conclude nonsense. What we do care is that if our assumptions hold then the conclusion will also hold. Otherwise we're happy with garbage-in, garbage-out.
Or you have introduced an additional temporary assumption somewhere in the proof tree which creates the contradiction. For example, the $Gamma,Pvdash R$ premise in our $lor$-elimination rule does that. Then we can justify the use of explosion by arguing that the branch that the explosion happened in was not actually necessary because the conditions it would be relevant in cannot happen.
If the additional assumption came from an introduction rule such as $to$-introduction, the argument that "this branch is not needed" is not as immediately convincing. However, in that case we can argue that we're still "constructively safe", because then our conclusion of that introduction rule is something that involves $to$. And the only way we can use that result is by using it in modus ponens (aka $to$-elimination). At that time someone will be claiming they can prove the antecedent of the $to$, but we know that is not actually realistic because the assumption leads to a contradiction! So this tells us that the proof branch where the modus ponens is found will itself be an unneeded branch, so constructively we don't need to worry about shenanigans there. It will never be executed.
The story for $neg$-introduction is similar to that for $to$-introduction; then the principle of explosion itself is the relevant elimination rule.
answered 1 hour ago
Henning Makholm
231k16297529
Here's one way to look at it. Suppose we're working in a natural deduction system with a $lor$-elimination rule that goes
$$ fracGammavdash Plor Q qquad Gamma, Pvdash R qquad Gamma, Qvdash RGammavdash R $$
This allows us to prove things by case analysis once we have proved a $lor$ that tells us we have to be in one of the cases.
Now, what is the fundamental thing knowing $neg P$ tells us? Arguably it is that in the above rule we won't need to carry out the $Gamma, Pvdash R$ part of the proof because $P$ cannot actually happen.
We could achieve that by having a bunch of specialized $lor$-elimination rules such as
$$ fracGammavdash Plor Q qquad Gamma, Pvdash A qquad Gammavdashneg A qquad Gamma, Qvdash RGammavdash R $$
but it is simpler to wrap all the variants up in a single rule that says:
If you find yourself in a branch of a proof where two contradictory things appear to hold, it means that proof branch was not actually necessary, and you can cancel it completely by pretending you've already proved whatever you were aiming for in that branch.
That's basically what the principle of explosion does.
It is constructively acceptible because intuitively there are only two ways it's ever possible to use it:
Either your initial assumptions in the proof are impossible to satisfy. Then we don't really care if we conclude nonsense. What we do care is that if our assumptions hold then the conclusion will also hold. Otherwise we're happy with garbage-in, garbage-out.
Or you have introduced an additional temporary assumption somewhere in the proof tree which creates the contradiction. For example, the $Gamma,Pvdash R$ premise in our $lor$-elimination rule does that. Then we can justify the use of explosion by arguing that the branch that the explosion happened in was not actually necessary because the conditions it would be relevant in cannot happen.
If the additional assumption came from an introduction rule such as $to$-introduction, the argument that "this branch is not needed" is not as immediately convincing. However, in that case we can argue that we're still "constructively safe", because then our conclusion of that introduction rule is something that involves $to$. And the only way we can use that result is by using it in modus ponens (aka $to$-elimination). At that time someone will be claiming they can prove the antecedent of the $to$, but we know that is not actually realistic because the assumption leads to a contradiction! So this tells us that the proof branch where the modus ponens is found will itself be an unneeded branch, so constructively we don't need to worry about shenanigans there. It will never be executed.
The story for $neg$-introduction is similar to that for $to$-introduction; then the principle of explosion itself is the relevant elimination rule.
answered 1 hour ago
Henning Makholm
231k16297529
edited 1 hour ago
answered 1 hour ago
Henning Makholm
231k16297529
answered 1 hour ago
Henning Makholm
231k16297529
answered 1 hour ago
Henning Makholm
231k16297529
231k16297529
add a comment |Â
add a comment |Â
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2922457%2fwhy-is-the-principle-of-explosion-accepted-in-constructive-mathematics%23new-answer', 'question_page');
);
Post as a guest
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
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
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
3
You don't know $Q$ is true, you know $(P land lnot P) to Q$ which is a much weaker statement. It in fact contains zero knowledge because you won't be able to prove $(P land lnot P)$.
– DanielV
7 hours ago