HEYTING ALGEBRAS
The logics complete for Heyting algebras: intuitionistic logic, which identifies truth with construction and drops unrestricted excluded middle, and the systems bounded below by it. Consequence is preservation of designated values over Heyting-algebra models, equivalently validity in the Kripke frames those algebras dualize.
Entries are organized as the subvariety lattice. Intuitionistic logic is the base, complete for all Heyting algebras; minimal logic sits just below it, dropping ex falso; the intermediate (superintuitionistic) logics are exactly the subvarieties between intuitionistic and Boolean, so Intermediate Logics is not one entry beside the others but the shape of the subdivision itself. Nelson's constructive logic with strong negation extends the base with a second negation. Constructive developments of whole theories—set theory, analysis, and their foundations—reason in this logic; individuated by their axioms rather than a subvariety, they are cross-listed with Metatheory. Proof-conditional and realizability interpretations of the connectives are accounts of the correspondence, not logics, and live in Metatheory/Proof-Systems and Metatheory/Computability.