nLab
Heyting algebra

Definition

A Heyting algebra is a lattice $L$ which as a poset admits an operation of implication

$$\Rightarrow :L^{\mathrm{op}}\times L\to L$$\Rightarrow: L^{op} \times L \to L

satisfying the condition (really a universal property)

$$(x\wedge a)\le b\mathrm{if}\mathrm{and}\mathrm{only}\mathrm{if}x\le (a\Rightarrow b)$$(x \wedge a) \leq b \qquad if\;and\;only\;if \qquad x \leq (a \Rightarrow b)

Alternatively, a Heyting algebra could be described as a poset which is finitely complete, finitely cocomplete, and cartesian closed (equivalently, a poset which is bicartesian closed); the implication $a\Rightarrow b$ plays the role of an exponential object $b^a$. Insofar as all these properties of a poset are described by universal properties, the Heyting algebra operations are categorical? in the sense of logic; that is, a poset can carry at most one structure of Heyting algebra.

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.

The definition of Heyting algebra may be recast into purely equational form, and so we can speak of an internal Heyting algebra in any category with products. For example, it turns out that the subobject classifier of a topos carries an internal Heyting algebra with respect to that topos. (It is not generally an internal Boolean algebra, and this explains to a large degree why one often hears that the internal logic of a topos is intuitionistic.)

We require Heyting algebra homomorphisms to preserve $\Rightarrow$ (in addition to the lattice structure). Heyting algebras and their homomorphisms form a concrete category HeytAlg.

Relation to topologies

One of the chief sources of Heyting algebras is given by topologies. As a poset, the topology of a topological space $X$ is a lattice (it has arbitrary joins and meets, and therefore finite joins and meets), and the implication operator is given by

$$(U\Rightarrow V)=\mathrm{int}(U^c\vee V)$$(U \Rightarrow V) = int(U^c \vee V)

where $U,V$ are open sets, $U^c$ is the set-theoretic complement of $U$, and $\mathrm{int}(S)$ denotes the interior of a subset $S\subseteq X$.

Somewhat more generally, a frame (a sup-lattice in which finite meets distribute over arbitrary sups) also carries a Heyting algebra structure. In a frame, we may define

$$(u\Rightarrow v)=\underset{x\wedge u\le v}{\bigvee }x$$(u \Rightarrow v) = \bigvee_{x \wedge u \leq v} x

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?. Another example is the topology of a discrete space $X$.

Relation to Boolean algebras

In any Heyting algebra $L$, we may define a negation operator

$$\neg :L^{\mathrm{op}}\to L$$\neg: L^{op} \to L

by $\neg x=(x\Rightarrow 0)$, where $0$ is the bottom element of the lattice. A Heyting algebra is Boolean if the double negation

$$\neg \neg :L\to L$$\neg \neg: L \to L

coincides with the identity map; this gives one of many ways of defining a Boolean algebra.

In any Heyting algebra $L$, we have for all $a,b\in L$ the inequality

$$(\neg a\vee b)\le (a\Rightarrow b)$$(\neg a \vee b) \leq (a \Rightarrow b)

and another characterization of Boolean algebra is a Heyting algebra in which this is an equality for all $a,b$.

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

Lemma

The double negation $\neg \neg :L\to L$ 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 $L=\Omega$ of a topos, that is the subobject classifier, this lemma says exactly that the double negation operator $\neg \neg :\Omega \to \Omega$ defines a Lawvere-Tierney topology.

Now let $L_{\neg \neg }$ denote the poset of regular elements of $L$, that is, those elements $x$ such that $\neg \neg x=x$. (When $L$ is the topology of a space, an open set $U$ is regular if and only if it is the interior of its closure.) With the help of the lemma above, we may prove

Theorem

The poset $L_{\neg \neg }$ is a Boolean algebra. Moreover, the assignment $L\mapsto L_{\neg \neg }$ is the object part of a functor

$$F:\mathrm{Heyt}\to \mathrm{Bool}$$F: Heyt \to Bool

called Booleanization, which is left adjoint to the full and faithful inclusion

$$i:\mathrm{Bool}\hookrightarrow \mathrm{Heyt}.$$i: Bool \hookrightarrow Heyt.

The unit of the adjunction, applied to a Heyting algebra $L$, is the map $L\to L_{\neg \neg }$ which maps each element $x$ to its regularization $\neg \neg x$.

Thus $\neg \neg :L\to L_{\neg \neg }$ preserves finite joins and finite meets and implication. In the other direction, we have an inclusion $i:L_{\neg \neg }\to L$, and this preserves meets but not joins, and negations but not implications generally.

Categorification

An elementary topos is a vertical categorification of a Heyting algebra. In other words, a $0$-topos (or more precisely, a $(\mathrm{0,1})$-topos) is essentially a Heyting algebra. Note that a Grothendieck $0$-topos is a locale.

Examples

Some examples are spelled out at internal logic.