Heyting algebra
A Heyting algebra is a bounded distributive lattice equipped with a binary implication operation \to that serves as the right adjoint to the meet operation \wedge, meaning that for all elements a, b, x in the algebra, a \wedge x \leq b if and only if x \leq a \to b.[1] The negation operation is defined as \neg a = a \to 0, where 0 is the bottom element, yielding a pseudocomplement that satisfies properties such as \neg\neg a \geq a but not necessarily equality unless the algebra is Boolean.[2] This structure generalizes Boolean algebras, which arise as Heyting algebras where the law of excluded middle holds, i.e., a \vee \neg a = 1 for all a, or equivalently, a \to b = \neg a \vee b.[3] Heyting algebras were introduced by the Dutch mathematician Arend Heyting in 1930 as a semantic framework to formalize the intuitionistic logic developed by L. E. J. Brouwer, which rejects the law of excluded middle in favor of constructive proofs.[4] Their origins trace back to early 20th-century developments in lattice theory, influenced by Richard Dedekind's work on lattices in 1897 and Ernst Schröder's algebraic logic in 1890, with Heyting's formulation providing algebraic models for Brouwer's intuitionism starting in the late 1920s.[5] Key properties include distributivity of meets over joins, the implication preserving finite meets in its second argument, and the algebra being a residuated lattice with \wedge as the monoid operation.[3] In complete Heyting algebras, infinite joins and meets distribute appropriately, enabling representations in pointless topology and domain theory.[3] Beyond logic, Heyting algebras appear in diverse applications: the lattice of open sets in a topological space forms a Heyting algebra under set-theoretic operations, supporting spatial reasoning in intuitionistic terms; they model the propositional structure in constructive type theory in computer science;[6] and they underpin duality theorems, such as Esakia's generalization of Stone duality for compact Heyting spaces.[2] Regular elements (those fixed by double negation) and complemented elements highlight connections to classical structures, while their equational theory is decidable, facilitating automated reasoning.[7]Definition and Characterizations
Formal Definition
A Heyting algebra is a tuple (H, \vee, \wedge, \to, \bot, \top) where H is a set, \vee and \wedge are binary operations on H (join and meet, respectively), \to is a binary operation on H (implication), and \bot, \top \in H are constant elements (bottom and top, respectively), such that (H, \vee, \wedge, \bot, \top) forms a bounded lattice and, for all a, b, c \in H, a \wedge b \leq c \iff a \leq b \to c, where the partial order \leq on H is defined by x \leq y if and only if x \wedge y = x (or equivalently, x \vee y = y).[8][2] In a bounded lattice, every pair of elements has a supremum (join \vee) and infimum (meet \wedge), with \bot serving as the least element such that a \wedge \bot = \bot for all a \in H, and \top as the greatest element such that a \vee \top = \top for all a \in H. The implication operation \to satisfies the above equivalence, ensuring that b \to c is the largest element x \in H such that b \wedge x \leq c. This structure captures the semantics of implication in a lattice setting.[9] The defining property of implication establishes an adjunction between the meet and implication operations: \to is the right adjoint to \wedge in the sense that, for all a, b, c \in H, c \wedge a \leq b \iff c \leq a \to b. This adjunction formalizes the relational aspect of implication within the lattice. Common notations include \perp for \bot and \top for the top element, aligning with conventions in order theory and logic.[2]Lattice-Theoretic Characterizations
A Heyting algebra can be characterized purely in terms of its lattice structure through the existence of relative pseudocomplements. In a lattice H, given elements a, b \in H, the relative pseudocomplement of a relative to b, denoted a \to b, is defined as the supremum a \to b = \bigvee \{ x \in H \mid a \wedge x \leq b \}, provided this supremum exists in H. A Heyting algebra is then equivalent to a distributive lattice in which relative pseudocomplements exist for every pair of elements a, b \in H.[10] Such lattices are necessarily bounded, with top element $1 (the identity for joins) and bottom element 0, where the absolute pseudocomplement of any element a is given by a \to 0 (the largest element x such that a \wedge x = [0](/page/0)). Moreover, the relative pseudocomplement operation distributes over existing joins: if \bigvee_i b_i exists in H, then a \to \left( \bigvee_i b_i \right) = \bigwedge_i (a \to b_i). This distribution property arises because the relative pseudocomplement acts as a residual operation in the residuated lattice structure inherent to Heyting algebras.[10] These characterizations are equivalent to the formal definition involving an explicit implication operation via the adjunction property a \wedge x \leq b if and only if x \leq a \to b. To see the equivalence, note that in a distributive lattice, the supremum defining the relative pseudocomplement a \to b automatically satisfies the right adjoint condition to the monomial map x \mapsto a \wedge x, as the distributivity ensures the Galois connection holds uniquely. Conversely, given an implication satisfying the adjunction in a distributive lattice, the set \{ x \mid a \wedge x \leq b \} has a \to b as its supremum by the adjointness.Implication-Based Definition
A Heyting algebra is defined as a bounded lattice (L, \wedge, \vee, 0, 1) equipped with a binary implication operation \to: L \times L \to L satisfying the projection property a \to a = 1 for all a \in L and monotonicity: if a \leq a' and b' \leq b, then a' \to b' \leq a \to b for all a, a', b, b' \in L.[11] These conditions ensure that \to behaves as a relative pseudocomplement in the lattice structure, preserving the order in a contravariant manner with respect to the first argument and covariant with respect to the second.[11] The negation operation is derived from implication as \neg a = a \to 0 for all a \in L.[11] This yields key properties such as \neg \neg a \geq a, reflecting double negation introduction in intuitionistic logic, though double negation elimination does not generally hold.[12] Specifically, \neg a \leq 1 always, and \neg 0 = 1, but \neg 1 = 0 only in Boolean cases.[12] A notable structural property is the currying identity (a \to (b \to c)) = ((a \wedge b) \to c) for all a, b, c \in L, which follows from the distributivity inherent to Heyting algebras via the implication operation. The lattice operations distribute over each other due to the axioms involving \to, such as a \to (b \wedge c) = (a \to b) \wedge (a \to c) and (a \vee b) \to c = (a \to c) \wedge (b \to c).[11] This implication-based view is equivalent to the lattice-theoretic characterization using relative pseudocomplements.[11]Axiomatic Characterization via Intuitionistic Logic
Heyting algebras provide a precise algebraic semantics for intuitionistic propositional logic (IPC), analogous to the role Boolean algebras play for classical propositional logic. In this framework, the elements of a Heyting algebra are interpreted as equivalence classes of propositions under logical equivalence, with the lattice operations corresponding to the logical connectives: the meet \wedge represents conjunction, the join \vee represents disjunction, the relative pseudocomplement a \to b represents implication, the least element $0 represents falsehood, and the greatest element $1 represents truth.[13] The axioms defining Heyting algebras directly mirror the axioms and inference rules of IPC. A key axiom is the detachment principle, expressed algebraically as (a \to b) \wedge a \leq b, which corresponds to the modus ponens rule allowing inference of b from a \to b and a. The structure also satisfies the distributive law a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c), reflecting the valid distribution of conjunction over disjunction in intuitionistic logic. Additional axioms for implication include a \to a = 1, ensuring reflexivity; (a \to b) \to ((b \to c) \to (a \to c)) = 1, capturing transitivity; and a \to (b \to a) = 1, expressing currying or prefixing. These, together with the axioms of a bounded distributive lattice (such as a \wedge 1 = a, a \vee 0 = a, and absorption laws like a \vee (a \wedge b) = a), form the complete equational basis.[13] The variety of Heyting algebras is sound and complete with respect to IPC: a propositional formula is provable in IPC if and only if it evaluates to the top element $1$ in every Heyting algebra under the standard interpretation. This equivalence arises because the free Heyting algebra generated by a set of propositional variables is isomorphic to the Lindenbaum-Tarski algebra of IPC, where propositions are quotiented by logical equivalence, and the operations are induced by the connectives. Soundness follows from verifying that each axiom of IPC holds equationally in Heyting algebras and that the rules of inference preserve validity; completeness is established via the representability of Heyting algebras as algebras of open sets in topological spaces or through embedding into canonical extensions.[13] This correspondence distinguishes Heyting algebras from Boolean algebras, as the latter validate classical principles absent in intuitionistic logic. Notably, Peirce's law, ((a \to b) \to a) \to a = 1, holds in all Boolean algebras but fails in general Heyting algebras; for example, in the three-element chain Heyting algebra with elements \{0 < m < 1\}, setting a = m and b = 0 yields ((m \to 0) \to m) \to m = (0 \to m) \to m = 1 \to m = m \neq 1. This reflects the rejection of the law of excluded middle in IPC, as a \vee \neg a = 1 (where \neg a = a \to 0) does not hold universally.[13]Examples
Elementary Examples
The trivial Heyting algebra consists of a single element, often denoted as {0} where 0 serves as both the bottom and top element, with all lattice operations (meet, join, and bounds) collapsing to this element and the implication operation defined as $0 \to 0 = 0$.[14] This structure satisfies the Heyting algebra axioms vacuously due to the absence of distinct elements.[15] A basic nontrivial example is the two-element chain Heyting algebra on the set {0 < 1}, equipped with the standard lattice operations: meets and joins as minimum and maximum, respectively, with 0 as the bottom and 1 as the top. The implication operation is defined by $0 \to 0 = 1, $0 \to 1 = 1, $1 \to 0 = 0, and $1 \to 1 = 1, which corresponds to the relative pseudocomplement in this ordered structure.[14] This can be verified to satisfy the defining property a \wedge (a \to b) = a \wedge b for all elements a, b.[15] More generally, any finite totally ordered set (chain) with a least element 0 and greatest element 1 forms a Heyting algebra under pointwise meets (minimum), joins (maximum), and implication given by a \to b = 1 if a \leq b, and a \to b = b otherwise.[14] For instance, the three-element chain {0 < a < 1} yields a Heyting algebra where the implication table is as follows:| \to | 0 | a | 1 |
|---|---|---|---|
| 0 | 1 | 1 | 1 |
| a | 0 | 1 | 1 |
| 1 | 0 | a | 1 |