Pierce's law, Consequentia Mirabilis, ¬¬-Elimination and LEM without Explosion

Consequentia_Mirabilis.txt

Proofs discussed in the video:

https://youtu.be/h1Ikhh3J1vY

Legend and conventions:

$(P \to \bot) \lor P\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,$ ... $PEM$ ... Principle of excluded middle (a.k.a. $LEM$)
$((P \to \bot) \land P) \to Q\,\,\,$ ... $EXPL$ ... principle of explosion, a.k.a. ex falso
$((P \to Q) \to P) \to P$ ... $PP$ ... Pierce's principle
$((P \to \bot) \to P) \to P$ ... $CM$ ... consequentia mirabilis, a.k.a. Clavius's principle
$((P \to \bot)\to\bot)\to P$ ... $DNE$ ... Double-negation elimination

We write $\neg P$ for $P \to\bot$.

We use subscripts for mere instances of the principles, thus presenting more fine grained results.
E.g. mean that $DNE_{\neg P}$ denotes $(\neg\neg\neg P)\to\neg P$.

We write $\vdash$ for provability in minimal logic, i.e. none of the above hold.

---

Summary:

$\bullet$ Related to Classical logic
$DNE_{PEM_P} \vdash PEM_P$
$DNE_Q \vdash EXPL_Q$
$DNE_P \vdash P \leftrightarrow (\neg \neg P)$

$\bullet$ Related to Intuitionistic logic:
$EXPL \vdash CM \Leftrightarrow PP \Leftrightarrow PEM \Leftrightarrow DNE$

$EXPL_P+PEM_P \vdash DNE_P$
$EXPL_Q+PEM_P \vdash PP_{P,Q}$
$EXPL_Q+PEM_P \vdash (Q \to P) \lor (P \to Q)$

$\bullet$ Related to Minimal logic:
$\vdash EXPL_{\neg Q}$
$\vdash DNE_{\neg P}$
$\vdash ((\neg P) \to \neg \neg P) \to (\neg \neg P)$
$\vdash PEM_P \leftrightarrow CM_P$

(And many of the above entailments also shall follow as implications,
via the deduction theorem, but I don't do such metalogic here)

Also (not this video), e.g.
$\vdash (P\to\neg Q) \to (Q\to\neg P)$
$\vdash (P\to\neg \neg Q) \to \neg \neg (P\to Q)$

---

But note:

$EXPL \nvdash (Q \to P) \lor (P \to Q)$
$EXPL \nvdash \big(P\to(Q\lor R)\big)\to\big((P\to Q)\lor(P\to R)\big)$
(Adopting either of this gives Gödel-Dummett logic.)

$EXPL \nvdash WPEM$
$EXPL \nvdash$ 4th DeMorgan's law
(Adopting either of this gives Jankov's logic)

And there's many more $EXPL$-unprovable classical theorems that were sometimes considered as axioms.
Most are weak variants of things we have considered.

First order metalogic result:
$EXPL \nvdash \big(\forall x. \neg\neg A(x)\big)\to\neg\neg \big(\forall x. A(x)\big)$
(That's e.g. in conflict with the constructive Church's thesis principle)

See also 'intermediate logic'.

---

Warmup:
$EXPL_Q \vdash (P \to \bot) \to (P \to Q)$ (equivalent form)
Hence
$EXPL_Q \vdash PEM_P \leftrightarrow \big(P \lor (P \to Q)\big)$
In words: "Anything is either true or implies everything."
$EXPL_Q + PEM_P \vdash (Q \to P) \lor (P \to Q)$

$\vdash P \to ((R\to P)\to P)$
$\vdash R \to ((R\to P)\to P)$
$\vdash (P \lor R) \to ((R\to P)\to P)$
So
$\vdash (P \lor (P \to Q)) \to PP_{P,Q}$
So
$EXPL_Q+PEM_P \vdash PP_{P,Q}$

$\vdash P \to ( (P\to Q)\to Q)$
$\vdash (( (P\to Q)\to Q) \to R) \to (P \to R)$
$\vdash (\neg \neg \neg P) \to \neg P$
$\vdash (\neg \neg \neg P) \leftrightarrow \neg P$
$\vdash DNE_{\neg P}$

Also (by implication introduction and modus ponens)
$\vdash EXPL_{\neg Q}$

$\vdash (P \lor \neg Q) \to (Q \to (P \lor\bot))$
$EXPL_P \vdash (P \lor \neg Q) \to (Q \to P)$ (form of disjunctive syllogism)
$EXPL_P \vdash (P \lor \neg Q) \to (\neg \neg Q \to P)$
$EXPL_P+PEM_P \vdash DNE_P$

$\vdash (P \to (Q \to R)) \to ((P\to Q) \to (P\to R))$ (=Frege's theorem)
$\vdash (P \to \neg P) \to \neg P$
$\vdash ((\neg P) \to \neg \neg P) \to (\neg \neg P)$
(that's a weak $CM_P$)

$\vdash ((\neg P) \to P) \to (\neg \neg P)$
$\vdash P \to (\neg \neg P)$
$DNE_P \vdash P \leftrightarrow (\neg \neg P)$

$\vdash (\neg (P \lor Q)) \to \neg P$
$\vdash (\neg PEM_P) \to \neg P$
$\vdash \neg PEM_P \to PEM_P$
$\vdash \neg \neg PEM_P$
$DNE_{PEM_P} \vdash PEM_P$
So really
$EXPL \vdash PEM \Leftrightarrow DNE$

$\vdash (P \land \neg P) \to \neg Q$
$\vdash (P \land \neg P) \to \neg \neg Q$
$DNE_Q \vdash EXPL_Q$

$CM_{PEM_P} \vdash PEM_P$
$PP_{P,\bot} \vdash CM_P$
$PP_{PEM_P,\bot} \vdash PEM_P$
So really
$EXPL \vdash PEM \Leftrightarrow PP$

$\vdash ((Q\to P) \land (C\to P) \land (Q \lor C)) \to P$
$\vdash ((\neg P)) \to P) \land (P \lor \neg P)) \to P$
$PEM_P \vdash CM_P$
So really
$\vdash PEM_P \leftrightarrow CM_P$

$\vdash (P \to Q) \to ((P \land Q) \leftrightarrow P)$
$\vdash (((P \to Q) \to (P \land Q)) \to P) \leftrightarrow (((P \to Q) \to P) \to P)$
$\vdash ((\neg P \to (P \land\bot)) \to P) \leftrightarrow ((\neg P \to P) \to P)$
$\vdash DNE_P \to CM_P$

$EXPL \vdash DNE \Leftrightarrow CM$