The duality of algebraic and Kripke models for linear logic
Gerard Allwein · 1992
This thesis presents two original results: (1) a Kripke (topological) semantics for general lattice based logics such as Linear Logic (sans certain operators called exponentials), and (2) a class of topological spaces dual to general lattices. Linear Logic has a variety of Computer Science applications including programming language semantics, machine architecture, and communication protocols. The analysis of Linear Logic starts by considering the algebraic semantics for much weaker logics. By a method of conservative extension, axioms and their resulting soundness conditions are built up until Linear Logic is reached. At each stage, soundness and completeness of the resulting algebraic models can be proved. Canonical Kripke models result from certain constructions on the algebraic models. These constructions generalize those of Dunn's gaggle theory (which assumes an underlying distributive lattice), which themselves already generalize constructions familiar from modal and relevance logic. Dual to one of these algebras is a particular type of ordered topological space. The duality is formalized using category theory. Each category of algebras is paired with a category of dual spaces. The relationship is accomplished with a pair of adjoint functors such that the induced monad in each of the categories can be described by a natural isomorphism (as opposed to simply a natural transformation). Operationally, this means that one can start with an algebra, apply the dualizing functor to get the dual space, and apply the other dualizing functor to get an algebra which is isomorphic to the original. A similar statement holds when starting with a space.