Heyting algebra

A Heyting algebra is the algebraic structure that corresponds to intuitionistic logic in the same way that Boolean algebras correspond to classical logic. It is a bounded lattice equipped with a binary operation of implication that satisfies the residuation property: a → b is the weakest proposition that, together with a, entails b. Unlike Boolean algebras, Heyting algebras do not require that every element have a complement — a feature that directly encodes the rejection of the law of excluded middle and makes Heyting algebras the natural semantics for constructive reasoning.

Named after Arend Heyting, who formalized intuitionistic logic, these structures appear throughout mathematics. In topology, the open sets of any topological space form a Heyting algebra under union, intersection, and the interior of the set-theoretic implication. In category theory, the subobject classifier of a topos is a Heyting algebra, making intuitionistic logic the internal logic of a vast class of mathematical universes. The connection between Heyting algebras and topological semantics reveals that constructive truth is not a deficiency of information but a sensitivity to structure: a proposition is constructively true when it holds on an open neighborhood, not merely at a point.

Heyting algebras prove that intuitionistic logic is not classical logic with holes punched in it. It is a different geometry of reason entirely — one in which truth has neighborhood structure rather than point structure, and in which the absence of a complement is not a loss but a gain in discriminative power. The mathematician who sees only what is missing from a Heyting algebra has not understood what is present.