Functors of Lindenbaum-Tarski, schematic interpretations, and adjoint cylinders between sentential logics (Q929639)

The authors prove that there are left and right adjunctions: \[ K\dashv J: \mathbf{CSL} \to \mathbf{ISL}\quad\text{and}\quad J\dashv G: \mathbf{ISL} \to \mathbf{CSL} \] between the category \(\mathbf{CSL}\) of classical sentential pretheories and the category \(\mathbf{ISL}\) of intuitionistic sentential pretheories. The functor \(K\) is the category-theoretic analogue of the Gödel-Gentzen schematic interpretation of classical propositional logic in intuitionistic logic. The functor \(G\) is related to the law of excluded middle. Both \(K\) and \(G\) are full embeddings of \(\mathbf{CSL}\) into \(\mathbf{ISL}\). The functor \(J: \mathbf{ISL}\to \mathbf{CSL}\) is injective on objects. Moreover, the authors prove that there is a pointwise epimorphic natural transformation from \(K\) to \(G\). Therefore this is an example of an adjoint cylinder as defined by \textit{F. W. Lawvere} in [``Cohesive toposes and Cantor's `lauter Einsen''', Philos. Math., III. Ser. 2, No.~1, 5--15 (1994; Zbl 0801.18005)]. The authors recall Lawvere's slogan: ``Adjoint cylinders are mathematical models for many instances of the \textit{Unity and Identity of Opposites}''. It is also proved that there is an adjoint cylinder between the category of Boolean algebras and the category of Heyting algebras. This is related to the first mentioned adjoint cylinder by an equivalence of categories which is extended from Lindenbaum-Tarski operators that define algebras from pretheories.