Completeness theorems via the double dual functor (Q1970592)

The `duality' implicitly referred to in the title is the dual adjunction between bounded distributive lattices and partially ordered sets, induced by the schizophrenic object \(2\); that is, the double dual of a distributive lattice \(L\) is the lattice of upper sets in its poset of prime filters. The latter is always a complete bi-Heyting algebra (indeed, it is completely distributive, though the authors do not mention this), and the authors regard it as a kind of completion of \(L\), even though the construction is not idempotent. Their key observation is that the canonical embedding of \(L\) in its double dual is conditionally bi-Heyting (that is, it preserves any implications and differences which exist); by exploiting this fact, and by specializing to particular classes of lattices, they obtain a number of completeness and conservativity results for various nonclassical and modal logics.