Let $P$ be a quantifier-free decidable formula, i.e. one can prove $P \lor \lnot P$. Does it follow that $\lnot \lnot P \to P$ intuitionistically?

Informally, a decidability of a formula means local LEM, but is it correct to treat it as "a piece of classical logic"?

  • 3
    $\begingroup$ Yes, at least for your first question. $\endgroup$ – Hanul Jeon May 21 '18 at 10:52
  • 1
    $\begingroup$ Constructively speaking, $P \lor \lnot P$ means "I can construct a proof for $P$, or I can construct a proof for $\lnot P$". $\lnot \lnot P \to P$ means "If I can't construct a proof for $\lnot P$, then I can construct a proof for $P$". Both of those statements are equivalent in that they rule out the possibility that $P$ is undecidable. $\endgroup$ – DanielV May 22 '18 at 12:13

Although the statement $\neg P\vee P$ is not a theorem in intuitionist logic, the conditional claim $\neg P\vee P\vdash \neg\neg P\to P$ may be constructed, through use of Explosion and Disjunctive Elimination.

$$\dfrac{\dfrac{\dfrac{}{\neg P\vee P~\vdash~ \neg P\vee P}{\small\sf Id}~~\dfrac{\dfrac{\dfrac{}{\neg\neg P~\vdash~ \neg\neg P}{\small\sf Id}~~\dfrac{}{\neg P~\vdash~ \neg P}{\small\sf Id}}{\neg\neg P, \neg P~\vdash~ \bot}{\small\sf \neg-}}{\neg\neg P, \neg P~\vdash~ P}{\small\sf Ex}~~\dfrac{}{P~\vdash~ P}{\small\sf Id}}{\neg P\vee P,\neg\neg P~\vdash~ P}{\small\sf \vee-}}{\neg P\vee P~\vdash~\neg\neg P\to P}{\small\sf \to+}$$


Here is another constructive proof. Assume $P \lor \lnot P$. Then either $P$ holds or $\lnot P$ holds. So we can reason by cases. If $P$ holds then $\lnot \lnot P \to P$ holds trivially. If $\lnot P$ holds, because $\lnot \lnot P$ is an abbreviation for $(\lnot P) \to \bot$, then $\bot$ holds, and by the principle of explosion (ex falso), $P$ holds. In either case, $\lnot \lnot P \to P$ holds.

The deeper point is that if we already know $A \lor B$ then we can prove a formula $C$ constructively by proving it under assumption $A$ and also by proving it under assumption $B$. Usually, the issue is that we cannot prove $P \lor \lnot P$ constructively, so we cannot reason by cases in that way. In other words, it is not that proof by cases is invalid constructively, it's that we have to prove that our cases are exhaustive (e.g. $P \lor \lnot P)$, which is often more difficult than in the classical case, making proof by cases a less broadly useful method.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.