In constructive logic, a proposition $P$ is called
decidable if $P\vee\neg P \;true$ is provable
constructively. That is, either we can write a proof to show $P \;true$, or we can write a proof to show $\neg P \;true$. Since $P$ might express an open problem for which we have neither a proof nor a refutation at present, not every proposition is decidable in the constructive sense. Hence, the
Law of the Excluded Middle (LEM) cannot be expected to hold universally in constructive logic as it does in classic logic, where every proposition is decidable under the truth table interpretation.
Note that this doesn't mean constructive logic refutes LEM. In fact, we are free to
assume LEM in constructive logic without fear of causing inconsistency. Even when $P$ is not known to be decidable, it may still be proved constructively with the proviso that $P\vee\neg P \;true$ holds. Adding such an assumption is always safe, precisely because constructive logic does not refute any instance of LEM. In fact, classical logic can be regarded as a special case of constructive logic in which LEM holds for all propositions. Proofs in classical logic may, and often do, rely implicitly on the universal validity of LEM, whereas in constructive logic we often prove without it. Hence, any proposition provable in constructive logic is also provable in classical logic.
What if one attempts to prove or disprove LEM, i.e., $P\vee\neg P \;true$, in constructive logic? In order to prove $P\vee\neg P \;true$, we must either prove $P \;true$ or prove $\neg P \;true$. However, we cannot expect to do this for
arbitrary proposition $P$ in the absence of further information about it. Similarly, the only option to prove $\neg (P\vee\neg P) \;true$ is to assume either $P \;true$ or $\neg P \;true$, which leads to $P\vee\neg P \;true$, and then deduce absurdity. This is also impossible, for doing so for arbitrary $P$ means refuting all propositions or their negations. Hence, constructive logic neither affirms nor refutes LEM.
Having known that one cannot prove either $P\vee\neg P \;true$ or $\neg (P\vee\neg P) \;true$, it may be surprising that $\neg \neg (P\vee\neg P) \;true$ is in fact provable. Here is an outline of the proof:
- Note that $\neg Q$ is a syntactic abbreviation of $Q\rightarrow \perp$. Hence, $\neg Q\;true$ can be proved by assuming $Q \;true$ and deriving a contradiction (i.e. $\perp \;true$) from the assumption. Also recall that a contradiction can be derived by assuming $Q\;true$ and $\neg Q\;true$, which is known as the Principle of Explosion.
- The strategy to prove $\neg \neg (P\vee\neg P) \;true$ is then to derive $P\vee\neg P \;true$ assuming $\neg (P\vee\neg P) \;true$, since $\neg (P\vee\neg P)\;true\Rightarrow P\vee\neg P \;true$ implies $\neg (P\vee\neg P)\Rightarrow \neg (P\vee\neg P)\;true, (P\vee\neg P)\;true$, which further implies $\neg (P\vee\neg P)\;true\Rightarrow\perp\;true$, i.e., the assumption leads to a contradiction.
- Assume that $\neg (P\vee\neg P) \;true$. If $P \;true$ is provable, then so is $P\vee\neg P \;true$. Since this leads to a contradiction, we have $P\;true\Rightarrow\perp\;true$, i.e., $\neg P \;true$ is provable. But again, this implies $P\vee\neg P \;true$ is provable, a contradiction. Since $\neg (P\vee\neg P) \;true$ always leads to contradictions, we have $\neg (P\vee\neg P)\;true \Rightarrow \perp\;true$, i.e., we found a proof of $\neg \neg (P\vee\neg P) \;true$.
The derivation described above can be formally written as follows [2, 3]:
$$
\genfrac{ }{ }{0.5}{0}
{
\genfrac{ }{ }{0.5}{0}
{
\genfrac{ }{ }{0.5}{0}{ }
{\Gamma\vdash\neg(P\vee\neg P)\;true}
R^u
\quad
\genfrac{ }{ }{0.5}{0}
{\genfrac{ }{ }{0.5}{0}{ }{\Gamma\vdash P\;true} R^v}
{\Gamma\vdash (P\vee\neg P)\;true}
\vee\!{-}I{-}L
}
{
\genfrac{ }{ }{0.5}{0}
{\Gamma \vdash\!\bot\; true}
{
\genfrac{ }{ }{0.5}{0}{ }{\Gamma\vdash\neg(P\vee\neg P)\; true} R^u
\quad
\genfrac{ }{ }{0.5}{0}
{\;\Gamma\vdash\neg P\;true}
{\;\Gamma\vdash P\vee\neg P\; true}
\vee\!{-}R
}
\neg I^v
}
}
{
\genfrac{ }{ }{0.5}{0}
{\Gamma\vdash\!\bot\;true}
{\neg\neg(P\vee\neg P)\;true}
\neg{-}I^u
}
$$
The fact that $\neg \neg (P\vee\neg P) \;true$ is provable means, while it is consistent to add LEM to constructive logic, we cannot add the refutation of LEM without degenerating the logic into inconsistency. Recall that, while LEM is not provable
in general, we can assume it in a proof without fear of contradiction. In contrast, since the double negation of LEM is provable for
every proposition, assuming the denial of LEM would soon lead us to absurdity.
As is shown in the foregoing argument, $P \;true$ is in general not provable even though $\neg\neg P \;true$ is provable. On the other hand, it is straightforward to show that $P\;true\Rightarrow\neg\neg P\;true$. Therefore, $\neg\neg P$ is a proposition
strictly weaker than $P$ itself in constructive logic. Namely, being able to reject any refutation of $P$ does not mean we actually know a proof of $P$, but being able to prove $P$ suffices to reject any refutation of it by absurdity. It is possible to interpret classical logic in terms of constructive logic by
doubly negating all statements, rendering them provable in constructive logic. From this perspective, constructive logic is more powerful than classical logic, in that it can distinguish constructive theorems from non-constructive ones whereas classical logic cannot.
References and further readings
1.
Practical Foundations for Programming Languages, Robert Harper, 1st ed., 2012
2.
Supplements of
Constructive Logic (Spring 2005), taught by Robert Harper
3.
Handouts of
Constructive Logic (Fall 2009), taught by Frank Pfenning
4.
On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Per Martin-Lof
5.
Truth of a Proposition, Evidence of a Judgement, Validity of a Proof, Per Martin-Lof
6. A compilation of
lecture notes on
Intuitionistic Type Theory given by Per Martin-Lof, and a
friendlier introduction to ITT by Silvio Valentini.
7.
Intuitionistic Logic, Dirk van Dalen
