Embedding classical in minimal implicational logic
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.
- Minimal from classical proofs
- scientific article; zbMATH DE number 874285
- An embedding of the implicative fragment of classical logic into the implicative fragment of intuitionistic logic
- A new normalization strategy for the implicational fragment of classical propositional logic
- scientific article; zbMATH DE number 1858065
- Classifying material implications over minimal logic
- An embedding of the implicative fragment of classical logic into the implicative fragment of intuitionistic logic
- On a new class of implications: (g,)-implications and several classical tautologies
- Embedding from multilattice logic into classical logic and vice versa
- The Jacobson radical for an inconsistency predicate
- THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
- Proof compression and NP versus PSPACE. II
- A general Glivenko-Gödel theorem for nuclei
- Conservation as translation
- Verified program extraction in number theory: the fundamental theorem of arithmetic and relatives
This page was built for publication: Embedding classical in minimal implicational logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2793912)
