On superintuitionistic logics as fragments of proof logic extensions (Q1091383)

Let I be the intuitionistic propositional calculus, \(Grz=S4+\square (\square (p\to \square p)\to p)\to p\) be Grzegorczyk's logic, G be proof logic, i.e. the extension of classical propositional calculus by the new connective \(\Delta\), the axiom-schemes \(\Delta\) (p\(\to q)\to (\Delta p\to \Delta q)\) and \(\Delta\) (\(\Delta\) \(p\to p)\to \Delta p\) and the inference rule A/\(\Delta\) A, \(I^{\Delta}\) be the proof-intuitionistic logic, i.e. the extension of I by the new connective \(\Delta\) and the axiom-schemes \(p\to \Delta p\), (\(\Delta\) \(p\to p)\to p\) and ((p\(\to q)\to p)\to (\Delta q\to p)\) (where the intended meaning of \(\Delta\) is ``provable''). If we denote by \({\mathcal L}L\) the lattice of all logics extending the logic L (L being I, Grz, G or \(I^{\Delta})\) and define the maps \(\sigma\), \(\kappa\), \(\lambda\), \(\nabla\) and \(\mu\) by the following equalities: \(l\sigma =Grz+\{TrA|\) \(A\in l\}\), \(l\kappa =G+\{TrA|\) \(A\in l\}\), \(l\lambda =\{A\in FI^{\Delta}|\) TrA\(\in l\}\), \(l\nabla =l\cap FI\) and \(l\mu =\{A\in FGrz|\) \(A\in l\}\), where TrA is the formula obtained from A by placing \(\square\) before each of its subformulae, FL is the set of all formulae of the logic L and in the logic \(l\in {\mathcal L}G\) the formula \(\square A\) is decoded as \(A\wedge \Delta A\), then, the main result of the paper could be stated as follows: the diagram corresponding to the maps \(\kappa\) :\({\mathcal L}I^{\Delta}\to {\mathcal L}G\), \(\lambda\) :\({\mathcal L}G\to {\mathcal L}I^{\Delta}\), \(\sigma\) :\({\mathcal L}I\to {\mathcal L}Grz\), \(\sigma^{-1}:{\mathcal L}Grz\to {\mathcal L}I\), \(\nabla:{\mathcal L}I^{\Delta}\to {\mathcal L}I\) and \(\mu\) :\({\mathcal L}G\to {\mathcal L}Grz\), is commutative, the maps \(\sigma\), \(\kappa\) and \(\lambda\) are isomorphisms, the maps \(\nabla\) and \(\mu\) are semilattice epimorphisms (not commutative with lattice operation \(+)\) and the following equalities hold: \(\kappa^{-1}=\lambda\), \(\sigma^{-1}=\mu^{-1}\lambda \nabla\) and \(\sigma =\nabla^{-1}\kappa \mu\). The consequence of the last of these equalities is that every superintuitionistic logic is a superintuitionistic fragment of some proof logic extension.