Heyting Algebra

- Mathematics & Logic -
Pure Mathematics Dictionary
A bounded lattice (with 0 and 1) equipped with a binary implication operation → satisfying the adjunction a ∧ b ≤ c iff a ≤ (b → c); provides an algebraic semantics for intuitionistic propositional logic where the law of excluded middle need not hold.