Nikolaj-K · April 13, 2024 11:24
diff --git a/Consequentia_Mirabilis.txt b/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$
	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$