Heyting algebra
In mathematics, Heyting algebras are special partially ordered sets that constitute a generalization of Boolean algebras. Heyting algebras arise as models of intuitionistic logic, a logic in which the law of excluded middle does not in general hold. Complete Heyting algebras are a central object of study in pointless topology.
Formal definitions
A Heyting algebra H is a bounded lattice such that for all a and b in H there is a greatest element x of H such that
This element is the relative pseudo-complement of a with respect to b, and is denoted a→b.
An equivalent definition can be given by considering the mappings
- fa:H→H defined by

for some fixed a in H. A bounded lattice H is a Heyting algebra if and only if all mappings fa are the lower adjoint of a monotone Galois connection. In this case the respective upper adjoints ga are given by ga(x) = a→x, where → is defined as above.
A complete Heyting algebra is a Heyting algebra that is a complete lattice.
In any Heyting algebra, one can define the pseudo-complement
of some element x by setting
, where 0 is the
least element of the Heyting algebra. Note that
, and that
is the largest element having this property.
However, it is not in general true that
, thus
is only a pseudo-complement, not a real complement.
Properties
Heyting algebras are always distributive. That is, given a lattice A and a binary relation →, these together form a Heyting algebra if and only if the following hold:
- a→a = 1


(distributive law)
The distributive law is sometimes stated as an axiom, but in fact it follows from the existence of relative
pseudo-complements. The reason is that, being the lower adjoint of a Galois connection,
preserves all existing suprema.
Distributivity in turn is just the preservation of binary suprema by
.
By a similar argument, the following infinite distributive law holds in any complete Heyting algebra:
for any element x in H and any subset Y of H.
Not every Heyting algebra satisfies the two De Morgan laws. However, the following statements are equivalent for all Heyting algebras H:
- H satisfies both De Morgan laws.
, for all
.
,
for all
.
, for all x, y in H.
The pseudo-complement of an element x of H is the supremum of the set
and
it belongs to this set (i.e.
holds).
An element x of a Heyting algebra H is called regular if any of the following equivalent conditions hold:
.
for some y in
H.
A Heyting algebra H is a Boolean algebra If and only if any of the following equivalent conditions hold:
In this case, the element a→b is equal to
.
In any Heyting algebra, the least and greatest elements 0 and 1 are regular.
The regular elements of any Heyting algebra constitute a Boolean algebra. Unless all elements of the Heyting algebra are regular, this Boolean algebra will not be a sublattice of the Heyting algebra, because its join operation will be different.
Examples
- Every totally ordered set that is a bounded lattice is also a Heyting algebra, where
and
for all a other than 0.
- Every Boolean algebra is a Heyting algebra, with p → q given by ¬p ∨ q.
- Every topology provides a complete Heyting algebra in the form of its open set lattice. In this case, the element A→B is the interior of the union of Ac and B, where Ac denotes the complement of the open set A. Not all complete Heyting algebras are of this form. These issues are studied in pointless topology, where complete Heyting algebras are also called frames or locales.
- The Lindenbaum algebra of propositional intuitionistic logic is a Heyting algebra. It is defined to be the set of all propositional logic
formulae, ordered via logical entailment: for any two formulae F and G we have
if and only if
. At this stage
is merely a preorder that induces a partial order which is the desired Heyting algebra.
Heyting algebras as applied to intuitionistic logic
Arend Heyting (1898-1980) was himself interested in clarifying the foundational status of intuitionistic logic, when he introduced this type of structure. The case of Peirce's law illustrates the semantic role of Heyting algebras. No simple proof is known that Peirce's law cannot be deduced from the basic laws of intuitionistic logic.
A Heyting algebra, from the logical standpoint, is essentially a generalization of the usual system of truth values. Amongst
other properties, the largest element, in logic called
, is analogous to 'true'. The usual two-valued
logic system is the simplest example of a Heyting algebra, one in which the elements of the algebra are
(true) and
(false). That is, in abstract terms, the
two-element Boolean algebra is also a Heyting algebra.
Classically valid formulas are those formulas that have a value of
in this Boolean algebra under any possible
assignment of true and false to the formula's variables — that is, they are formulas which are tautologies in the usual
truth-table sense. Intuitionistically valid formulas are those formulas that have a value of
in any Heyting algebra under any assignment
of values to the formula's variables.
One can construct a Heyting algebra in which the value of Peirce's law is not always
. Consider the set {0,1,2} standardly ordered (the
simplest example of a Heyting algebra that is not Boolean) and observe that if we interpret P by 1 and Q by 0, then the
interpretation of Peirce's law ((P → Q) → P) → P is 1, whereas
is 2. From what has just been said, this shows
that it cannot be intuitionistically derived. See Curry-Howard isomorphism for the general
context, of what this implies in type theory.
Word problem
The word problem on free Heyting algebras is difficult.[3] The only known results are that the free Heyting algebra on one generator is infinite, and that the free complete Heyting algebra on one generator exists (and has one more element than the free Heyting algebra).
Notes
References
- Rutherford, Daniel Edwin (1965). Introduction to Lattice Theory. Oliver and Boyd.
- F. Borceux, Handbook of Categorical Algebra 3, In Encyclopedia of Mathematics and its Applications, Vol. 53, Cambridge University Press, 1994.
- G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003.
See also
External links
This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)


for all
x in H.


