Heyting algebra

In mathematics, a Heyting algebra is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b of implication such that c ∧ a ≤ b is equivalent to c ≤ a → b. From a logical standpoint, A → B is by this definition the weakest proposition for which modus ponens, the inference rule A → B, A ⊢ B, is sound. Equivalently a Heyting algebra is a residuated lattice whose monoid operation a⋅b is a ∧ b; yet another definition is as a posetal cartesian closed category with all finite sums. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.

As lattices, Heyting algebras are distributive. Every Boolean algebra is a Heyting algebra when a → b is defined as usual as ¬a ∨ b, as is every complete distributive lattice satisfying a one-sided infinite distributive law when a → b is taken to be the supremum of the set of all c for which a ∧ c ≤ b. The open sets of a topological space form such a lattice, and therefore a (complete) Heyting algebra. In the finite case every nonempty distributive lattice, in particular every nonempty finite chain, is automatically complete and completely distributive, and hence a Heyting algebra.

...
Wikipedia