satisfying the condition (really a universal property)
This is equivalent to the following definition.
The implication is the exponential object .
The definition of Heyting algebra may be recast into purely equational form: add to the equational theory of lattices the inequalities and , writing these inequalities in equational form via the equivalence iff . Hence we can speak of an internal Heyting algebra in any category with products.
In logic, Heyting algebras are precisely algebraic models for intuitionistic propositional calculus, just as Boolean algebras model classical propositional calculus. As one might guess from this description, the “law of the excluded middle” does not generally hold in a Heyting algebra; see the discussion below.
In a Heyting category, every subobject poset is a Heyting algebra. In particular, this holds for every topos. Furthermore, in a topos, the power object is an internal Heyting algebra that corresponds to the external Heyting algebra . In a boolean topos, the internal Heyting algebras are all internal boolean algebras. In general, however, the internal logic of a topos (or other Heyting category) is intuitionistic.
One of the chief sources of Heyting algebras is given by topologies. As a poset, the topology of a topological space is a complete lattice (it has arbitrary joins and meets, although the infinitary meets are not in general given by intersection), and the implication operator is given by
where are open sets, is the set-theoretic complement of , and denotes the interior of a subset .
and the distributivity property guarantees that the universal property for implication holds. (The detailed proof is a “baby” application of an adjoint functor theorem.)
Thus frames are extensionally the same thing as complete Heyting algebras. However, intensionally they are quite different; that is, a morphism of frames is not usually a morphism of complete Heyting algebras: they do not preserve the implication operator.
A locale is the same thing as a frame, but again the morphisms are different; they are reversed.
Topologies that are Boolean algebras are the exception rather than the rule; basic examples include topologies of Stone spaces; see Stone duality. Another example is the topology of a discrete space .
In any Heyting algebra , we may define a negation operator
coincides with the identity map; this gives one of many ways of defining a Boolean algebra.
In any Heyting algebra , we have for all the inequality
and another characterization of Boolean algebra is a Heyting algebra in which this is an equality for all .
There are several ways of passing back and forth between Boolean algebras and Heyting algebras, having to do with the double negation operator. A useful lemma in this regard is
The double negation is a monad that preserves finite meets.
The proof can be made purely equational, and is therefore internally valid in any category with products. Applied to the internal Heyting algebra of a topos, that is the subobject classifier, this lemma says exactly that the double negation operator defines a Lawvere–Tierney topology. Similarly, we get the double negation sublocale of any locale.
Now let denote the poset of regular elements of , that is, those elements such that . (When is the topology of a space, an open set is regular if and only if it is the interior of its closure, that is if it is a regular element of the Heyting algebra of open sets described above.) With the help of the lemma above, we may prove
The poset is a Boolean algebra. Moreover, the assignment is the object part of a functor
called Booleanization, which is left adjoint to the full and faithful inclusion
Thus preserves finite joins and finite meets and implication. In the other direction, we have an inclusion , and this preserves meets but not joins. It also preserves negations; more generally and perhaps surprisingly, it preserves implications as well.
Regular elements are not to be confused with complemented element?s, i.e., elements in a Heyting algebra such that , although it is true that every complemented element is regular. An example of a regular element which is not complemented is given by the unit interval as an element of the topology of ; a complemented element in a Heyting algebra given by a topology is the same as a clopen subset.
Complemented elements furnish another universal relation between Boolean algebras and Heyting algebras: the set of complemented elements in a Heyting algebra is a Boolean algebra , and the inclusion is a Heyting algebra map which is universal among Heyting algebra maps out of Boolean algebras . In other words, we have the following result.
The assignment is the object part of a right adjoint to the forgetful functor .
We prove the lemma and theorems of the preceding section.
Since preserves order, it is clear that and , so
follows. In the other direction, to show
we show . But we have , and we also have the general result
Putting , , , we obtain
and so now
Since is a monad, and is the corresponding category (poset) of -algebras, the left adjoint preserves joins. Since this map is epic, this also gives the fact that has joins. The map preserves meets by the preceding lemma, and . Thus is a surjective lattice map, and it follows that is distributive because is.
Working in (where the join will be written and the meet ), we have for any the equations
so that is the complement of . We have thus shown that is a complemented distributive lattice, i.e., a Boolean algebra. This calculation also shows that preserves negation.
To show preserves implication, we may start from the observation (see the following lemma) that in any Heyting algebra , we have
where the last expression is as computed in the Boolean algebra , since in a Boolean algebra we have .
Therefore is a Heyting algebra quotient which is the coequalizer of . It follows that a Heyting algebra map to any Boolean algebra factors uniquely through this coequalizer, and the induced map is a Boolean algebra map. In other words, is the universal Heyting algebra map to a Boolean algebra, which establishes the adjunction.
In a Heyting algebra, .
Since is contravariant and is covariant, we have
Since is contravariant, we have
We conclude that On the other hand, we have
whence , which completes the proof.
It follows from this lemma that double negation on a Heyting algebra preserves implication, since
This is important for the double negation translation.
In a Heyting algebra , the elements and are clearly complemented. If and are complemented, then so is since
By a similar proof, is complemented. Finally, has complement : writing for typographical clarity, we have
Thus the complemented elements form a Heyting subalgebra . Clearly is a Boolean algebra, and clearly if is Boolean, then any Heyting algebra map factors uniquely through . This proves the theorem.
An elementary topos is a vertical categorification of a Heyting algebra: the notion of Heyting algebra is essentially equivalent to that of (0,1)-topos. Note that a Grothendieck -topos is a frame or locale.
In other words, every topos is a Heyting category.
In particular for the subobject classifier, is a Heyting algebra.
More details and examples are spelled out at internal logic.
Named after Arend Heyting.