INCLUSION CRITERIA
An entry belongs in this subdivision if and only if it is complete for Heyting algebras or a subvariety of them—a logic bounded below by intuitionistic logic that restricts excluded middle and double-negation elimination.
Required: At least one of the following:
- Completeness for the variety of Heyting algebras, a proper subvariety (intermediate/superintuitionistic logics), the weak Heyting algebras that generalize them (subintuitionistic logics), or their order duals (co-Heyting and bi-Heyting algebras)
- A proof system that rejects or restricts excluded middle and double-negation elimination over an intuitionistic base
- An intuitionistic connective algebra extended by strong negation (Nelson) or a related operator
Not sufficient: Bivalent classical semantics (Boolean). A many-valued matrix whose motivation is degrees rather than a Heyting reduct (Many-Valued). A term calculus presented purely as a typing discipline (Type). A proof-conditional interpretation of the connectives (BHK, realizability, Dialectica), which is metatheory.
Boundary: Intuitionistic type theories present the same content as term calculi and live in Type; their Heyting-algebra and Kripke semantics live here. A constructive development of a theory (set theory, analysis) is individuated by its non-logical axioms, not a Heyting subvariety, and is cross-listed with its foundational home in Metatheory. Gödel-Dummett logic (LC) is the linear-Heyting subvariety and equally a BL-subvariety, cross-listed with Many-Valued.