×

Functors of Lindenbaum-Tarski, schematic interpretations, and adjoint cylinders between sentential logics. (English) Zbl 1155.03048

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 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 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.

MSC:

03G30 Categorical logic, topoi
18C10 Theories (e.g., algebraic theories), structure, and semantics
18C20 Eilenberg-Moore and Kleisli constructions for monads

Citations:

Zbl 0801.18005
PDFBibTeX XMLCite
Full Text: DOI