Embedding classical in minimal implicational logic (Q2793912)

Let \(\text{Stab}_V=\{\neg\neg P\to P\mid P\in V\}\) if \(V\) is a set of propositional variables. It is known (Kolmogorov, 1925) that a propositional formula \(A\) with the only connectives \(\to\) and \(\neg\) is deducible in classical logic iff \(A\) is deducible in intuitionistic (in fact, in minimimal) logic from \(\text{Stab}_{\mathcal V(A)}\), where \(\mathcal V(A)\) is the set of all the variables in \(A\). The authors consider which set of variables \(V\subseteq\mathcal V(A)\) is sufficient for this result.NEWLINENEWLINE One can consider only implicational formulas because in the context of minimal logic \(\neg A\) can be interpreted as \(A\to\bot\) for a distinguished variable \(\bot\) (absurdity). For implicational formulas \(A\), it is proved that classical derivability implies intuitionistic derivability from \(\text{Stab}_P\), where \(P\) is the final variable of \(A\). The Glivenko theorem is an easy consequence of this result. Another consequence is connected to the fact that classical logic can be obtained from intuitionistic one by adding the Peirce formula \(((Q\to P)\to Q)\to Q\) (\(\text{Peirce}_{Q,P}\)) as an axiom scheme. The authors prove that an implicational formula is deducible in classical logic iff it is deducible in intuitionistic logic from \(\text{Peirce}_{P,\bot}\) for the final variable \(P\) of \(A\).NEWLINENEWLINE The case of minimal logic instead of intuitionistic one is rather complicated. The authors describe the set of instances of the Peirce formula and the principle ex falso quodlibet which is sufficient for moving from classical derivability to derivability in minimal logic. It is shown that in general an unbounded number of Peirce formulas is necessary. In this context, multiple examples of implicational formulas deducible in classical but not in minimal logic are considered.