Heyting Algebra¶
A bounded lattice whose implication is the right adjoint of meet, giving an algebraic semantics for intuitionistic reasoning.
Core Idea¶
A Heyting algebra is a bounded lattice \(H\) with an operation \(a\to b\) satisfying \(c\wedge a\leq b\) exactly when \(c\leq a\to b\) for every \(a,b,c\in H\). The implication is the right adjoint of meet-with-\(a\), not just an arrow-shaped notation. Negation is derived as \(\neg a=a\to0\) and need not be Boolean complement.[ref-eddf278b27f1][ref-d54975c14a09]
The definition asks for finite meet and join, bottom and top, and this residual implication. Completeness—all joins and meets—is additional. Aczel's quotient of intuitionistic formulas by provable equivalence and Barr and Wells's algebra of topological opens are unlike carriers satisfying the same adjunction; the topological example is complete, but general Heyting algebras need not be.[ref-9a862aff3294][ref-eddf278b27f1][^ref-d54975c14a09]
Scope of Application¶
In intuitionistic logic, formula classes ordered by provable entailment use conjunction as meet and the logical conditional as its residual. In topology, opens ordered by inclusion use intersection as meet and \(U\to V=\operatorname{int}((X\setminus U)\cup V)\) as implication. For the Sierpinski topology \(\{\varnothing,\{1\},X\}\), \(\neg\{1\}=\varnothing\) and \(\neg\neg\{1\}=X\): a concrete non-Boolean Heyting algebra. Every Boolean algebra is nevertheless a Heyting algebra, so non-Boolean behavior is possible, not mandatory.[ref-9a862aff3294][ref-eddf278b27f1][^ref-d54975c14a09]
Clarity¶
To recognize the identity, specify the bounded lattice and verify the meet–implication equivalence for every triple. An arbitrary conditional connective, a bare relative pseudo-complement operation, or a complete lattice without this residual law is insufficient. Conversely, the fact that a topological open-set example is a Complete (complexity) Heyting algebra does not turn completeness into an axiom of every Heyting algebra.[ref-eddf278b27f1][ref-d54975c14a09]
The two frozen redirects require separate treatment: Relative pseudo-complement names an operation-centered question; Free Heyting algebra adds a universal-property construction. Neither is automatically an alias or fully covered merely because this general entry is drafted.[^ref-9a862aff3294]
Manages Complexity¶
The adjunction converts a proof about \(c\wedge a\leq b\) into one about \(c\leq a\to b\), replacing separate implication calculations with a uniform order rule. It also sorts hypotheses: a general theorem can use the residual law, a Boolean theorem may additionally use excluded middle, and a frame theorem may use arbitrary joins. These extra laws cannot be imported solely from a convenient example.[ref-9a862aff3294][ref-eddf278b27f1][^ref-d54975c14a09]
Abstract Reasoning¶
For a proposed carrier, establish bounded-lattice laws, find the greatest \(c\) with \(c\wedge a\leq b\), and show that it equals \(a\to b\) for all \(a,b\). In Aczel's intuitionistic formula quotient, the order is provable entailment and the equivalence follows from deduction. For opens, the largest qualifying open is the interior of \((X\setminus U)\cup V\). Check Booleanity or completeness only when the intended conclusion needs them.[ref-9a862aff3294][ref-eddf278b27f1][^ref-d54975c14a09]
Knowledge Transfer¶
The exact relation transfers from syntax to topology even though “element,” “meet,” and “order” have different realizations. The proposed strict parent is live Algebraic Structure, whose carrier–operations–laws signature is literally satisfied. Live Complete Heyting Algebra and Boolean Algebra are narrower kinds, not upward parents; Lindenbaum–Tarski Algebra names a quotient construction whose kind depends on the logic. A generic residual pattern outside bounded lattices is a future-prime question rather than a claim that this entry is prime.[ref-9a862aff3294][ref-eddf278b27f1][^ref-d54975c14a09]
[^ref-9a862aff3294]: Peter Aczel, Constructive Set Theory lectures, lecture 5, original author lecture, section “Heyting Algebras,” inspected 2026-10-01. [^ref-eddf278b27f1]: Peter Aczel, Constructive Set Theory lectures, lecture 6, original author lecture, definitions, topological examples and two-point model, inspected 2026-10-01. [^ref-d54975c14a09]: Michael Barr and Charles Wells, Toposes, Triples and Theories, original author text, §5.6, printed pp.164–166 (PDF pp.177–179), inspected 2026-10-01.
Relationships to Other Abstractions¶
Current abstraction Heyting Algebra Domain-specific
Parents (1) — more general patterns this builds on
-
Heyting Algebra is a kind of Algebraic Structure Domain-specific
A Heyting algebra is an algebraic structure with bounded lattice operations and a residuation law.
Hierarchy path (1) — routes to 1 parentless root
- Heyting Algebra → Algebraic Structure → Mathematical structure → Set and Membership
Neighborhood in Abstraction Space¶
Heyting Algebra sits in a moderately populated region (50th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Algebraic Operations & Quasigroup Structures (12 abstractions)
Nearest neighbors
- Complete Heyting algebra — 0.88
- Distributivity (order theory) — 0.86
- Join and meet — 0.86
- Complete lattice — 0.86
- Frink ideal — 0.85
Computed from structural-signature embeddings · 2026-10-08