Heyting algebra



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory


(0,1)(0,1)-Category theory




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

:L op×LL\Rightarrow: L^{op} \times L \to L

satisfying the condition (really a universal property)

(xa)bifandonlyifx(ab)(x \wedge a) \leq b \qquad if\;and\;only\;if \qquad x \leq (a \Rightarrow b)

This is equivalent to the following definition.


A Heyting algebra is a bicartesian closed poset, that is a poset which (when thought of as a thin category) is

The implication aba\Rightarrow b is the exponential object b ab^a.


Insofar as all these properties of a poset are described by universal properties, being a Heyting algebra is a property-like structure on a poset; a poset can be a Heyting algebra in at most one way.

The definition of Heyting algebra may be recast into purely equational form: add to the equational theory of lattices the inequalities (xy)xy(x \Rightarrow y) \wedge x \leq y and yx(yx)y \leq x \Rightarrow (y \wedge x), writing these inequalities in equational form via the equivalence aba \leq b iff a=aba = a \wedge b. Hence we can speak of an internal Heyting algebra in any category with products.


A Heyting algebra homomorphism is a homomorphism of the underlying lattices that preserve \Rightarrow. Heyting algebras and their homomorphisms form a concrete category HeytAlg.

Relation to other concepts

To logic

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 Sub(A)Sub(A) is a Heyting algebra. In particular, this holds for every topos. Furthermore, in a topos, the power object 𝒫(A)\mathcal{P}(A) is an internal Heyting algebra that corresponds to the external Heyting algebra Sub(A)Sub(A). 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.

To topology

One of the chief sources of Heyting algebras is given by topologies. As a poset, the topology of a topological space XX 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

(UV)=int(U cV)(U \Rightarrow V) = int(U^c \vee V)

where U,VU, V are open sets, U cU^c is the set-theoretic complement of UU, and int(S)int(S) denotes the interior of a subset SXS \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

(uv)= xuvx(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; see Stone duality. Another example is the topology of a discrete space XX.

To Boolean algebras

In any Heyting algebra LL, we may define a negation operator

¬:L opL\neg\colon L^{op} \to L

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

¬¬:LL\neg \neg\colon L \to L

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

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

(¬ab)(ab), (\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,ba, 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


The double negation ¬¬:LL\neg \neg\colon 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=ΩL = \Omega of a topos, that is the subobject classifier, this lemma says exactly that the double negation operator ¬¬:ΩΩ\neg \neg\colon \Omega \to \Omega defines a Lawvere–Tierney topology. Similarly, we get the double negation sublocale of any locale.

Now let L ¬¬L_{\neg\neg} denote the poset of regular elements of LL, that is, those elements xx such that ¬¬x=x\neg\neg x = x. (When LL is the topology of a space, an open set UU 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 L ¬¬L_{\neg\neg} is a Boolean algebra. Moreover, the assignment LL ¬¬L \mapsto L_{\neg\neg} is the object part of a functor

F:HeytBoolF\colon Heyt \to Bool

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

i:BoolHeyt.i\colon Bool \hookrightarrow Heyt.

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

Thus ¬¬:LL ¬¬\neg\neg\colon L \to L_{\neg\neg} preserves finite joins and finite meets and implication. In the other direction, we have an inclusion i:L ¬¬Li\colon L_{\neg\neg} \to L, 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 xx in a Heyting algebra such that x¬x=1x \vee \neg x = 1, 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 (0,1)(0, 1) as an element of the topology of \mathbb{R}; 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 HH is a Boolean algebra Comp(H)Comp(H), and the inclusion Comp(H)HComp(H) \to H is a Heyting algebra map which is universal among Heyting algebra maps BHB \to H out of Boolean algebras BB. In other words, we have the following result.


The assignment HComp(H)H \mapsto Comp(H) is the object part of a right adjoint to the forgetful functor BoolHeytBool \to Heyt.


We prove the lemma and theorems of the preceding section.

Proof of lemma

Since ¬¬\neg \neg preserves order, it is clear that ¬¬(xy)¬¬x\neg \neg(x \wedge y) \leq \neg \neg x and ¬¬(xy)¬¬y\neg \neg(x \wedge y) \leq \neg \neg y, so

¬¬(xy)(¬¬x)(¬¬y)\neg \neg (x \wedge y) \leq (\neg \neg x) \wedge (\neg \neg y)

follows. In the other direction, to show

(¬¬x)(¬¬y)¬¬(xy),(\neg \neg x) \wedge (\neg \neg y) \leq \neg \neg (x \wedge y),

we show (¬¬x)(¬¬y)¬(xy)0(\neg \neg x) \wedge (\neg \neg y) \wedge \neg (x \wedge y) \leq 0. But we have ¬(xy)=(y¬x)\neg (x \wedge y) = (y \Rightarrow \neg x), and we also have the general result

(ab)(bc)(ac).(a \Rightarrow b) \wedge (b \Rightarrow c) \leq (a \Rightarrow c).

Putting a=ya = y, b=¬xb = \neg x, c=0c = 0, we obtain

¬(xy)(¬¬x)¬y\neg (x \wedge y) \wedge (\neg \neg x) \leq \neg y

and so now

¬(xy)(¬¬x)(¬¬y)(¬y)(¬¬y)0\neg (x \wedge y) \wedge (\neg \neg x) \wedge (\neg \neg y) \leq (\neg y) \wedge (\neg \neg y) \leq 0

as required.

Proof of theorem 1

Since ¬¬\neg \neg is a monad, and L ¬¬L_{\neg \neg} is the corresponding category (poset) of ¬¬\neg \neg-algebras, the left adjoint ¬¬:LL ¬¬\neg \neg \colon L \to L_{\neg \neg} preserves joins. Since this map is epic, this also gives the fact that L ¬¬L_{\neg \neg} has joins. The map LL ¬¬L \to L_{\neg\neg} preserves meets by the preceding lemma, and ¬¬1=¬0=1\neg \neg 1 = \neg 0 = 1. Thus LL ¬¬L \to L_{\neg\neg} is a surjective lattice map, and it follows that L ¬¬L_{\neg\neg} is distributive because LL is.

Working in L ¬¬L_{\neg \neg} (where the join will be written ¬¬\vee_{\neg\neg} and the meet ¬¬\wedge_{\neg\neg}), we have for any xL ¬¬x \in L_{\neg \neg} the equations

x ¬¬¬x=¬¬(x¬x)=¬(¬x¬¬x)=¬0=1x \vee_{\neg \neg} \neg x = \neg \neg (x \vee \neg x) = \neg (\neg x \wedge \neg \neg x) = \neg 0 = 1
x ¬¬¬x=x¬x=0x \wedge_{\neg\neg} \neg x = x \wedge \neg x = 0

so that ¬x\neg x is the complement of xL ¬¬x \in L_{\neg \neg}. We have thus shown that L ¬¬L_{\neg\neg} is a complemented distributive lattice, i.e., a Boolean algebra. This calculation also shows that ¬¬:LL ¬¬\neg\neg \colon L \to L_{\neg\neg} preserves negation.

To show LL ¬¬L \to L_{\neg\neg} preserves implication, we may start from the observation (see the following lemma) that in any Heyting algebra LL, we have

¬(ab)=(¬¬a)(¬b).\neg(a \Rightarrow b) = (\neg \neg a) \wedge (\neg b).


¬¬(ab) = ¬((¬¬a)(¬b)) = ¬((¬¬a)(¬¬¬b)) = ¬¬((¬a)(¬¬b)) = ¬a ¬¬(¬¬b) = ¬(¬¬a) ¬¬(¬¬b)\array{ \neg \neg(a \Rightarrow b) & = & \neg((\neg \neg a) \wedge (\neg b)) \\ & = & \neg ((\neg \neg a) \wedge (\neg \neg \neg b)) \\ & = & \neg \neg ((\neg a) \vee (\neg \neg b)) \\ & = & \neg a \vee_{\neg \neg} (\neg \neg b) \\ & = & \neg (\neg \neg a) \vee_{\neg \neg} (\neg \neg b) }

where the last expression is (¬¬a)(¬¬b)(\neg \neg a) \Rightarrow (\neg \neg b) as computed in the Boolean algebra L ¬¬L_{\neg \neg}, since in a Boolean algebra we have (xy)=(¬xy)(x \Rightarrow y) = (\neg x \vee y).

Therefore LL ¬¬L \to L_{\neg\neg} is a Heyting algebra quotient which is the coequalizer of 1,¬¬:LL1, \neg\neg \colon L \stackrel{\to}{\to} L. It follows that a Heyting algebra map LBL \to B to any Boolean algebra BB factors uniquely through this coequalizer, and the induced map L ¬¬BL_{\neg \neg} \to B is a Boolean algebra map. In other words, LL ¬¬L \to L_{\neg\neg} is the universal Heyting algebra map to a Boolean algebra, which establishes the adjunction.


In a Heyting algebra, ¬(ab)=(¬¬a)(¬b)\neg(a \Rightarrow b) = (\neg \neg a) \wedge (\neg b).


Since ¬\neg is contravariant and aa \Rightarrow - is covariant, we have

¬(ab)¬(a0)=(¬¬a).\neg(a \Rightarrow b) \leq \neg(a \Rightarrow 0) = (\neg \neg a).

Since b- \Rightarrow b is contravariant, we have

¬(ab)¬(1b)=(¬b).\neg(a \Rightarrow b) \leq \neg(1 \Rightarrow b) = (\neg b).

We conclude that ¬(ab)(¬¬a)(¬b).\neg(a \Rightarrow b) \leq (\neg \neg a) \wedge (\neg b). On the other hand, we have

(¬¬a)(¬b)(ab)(¬¬a)(¬a)0(\neg \neg a) \wedge (\neg b) \wedge (a \Rightarrow b) \leq (\neg \neg a) \wedge (\neg a) \leq 0

whence (¬¬a)(¬b)¬(ab)(\neg \neg a) \wedge (\neg b) \leq \neg (a \Rightarrow b), which completes the proof.


It follows from this lemma that double negation on a Heyting algebra ¬¬:LL\neg \neg \colon L \to L preserves implication, since

¬¬(ab)=¬((¬¬a)(¬b))=0 (¬¬a)(¬b)=(¬¬b) (¬¬a)=(¬¬a)(¬¬b).\neg \neg(a \Rightarrow b) = \neg ((\neg \neg a) \wedge (\neg b)) = 0^{(\neg \neg a) \wedge (\neg b)} = (\neg \neg b)^{(\neg \neg a)} = (\neg \neg a) \Rightarrow (\neg \neg b).

This is important for the double negation translation.

Proof of theorem 2

In a Heyting algebra HH, the elements 00 and 11 are clearly complemented. If xx and yy are complemented, then so is xyx \wedge y since

1=11=(x¬x¬y)(y¬x¬y)=(xy)(¬x¬y)1 = 1 \wedge 1 = (x \vee \neg x \vee \neg y) \wedge (y \vee \neg x \vee \neg y) = (x \wedge y) \vee (\neg x \vee \neg y)
(xy)(¬x¬y)=(xy¬x)(xy¬y)=00=0.(x \wedge y) \wedge (\neg x \vee \neg y) = (x \wedge y \wedge \neg x) \vee (x \wedge y \wedge \neg y) = 0 \vee 0 = 0.

By a similar proof, xyx \vee y is complemented. Finally, xyx \Rightarrow y has complement x¬yx \wedge \neg y: writing xy=y xx \Rightarrow y = y^x for typographical clarity, we have

1=11=(¬xx)(y¬y)(y xx)(y x¬y)=y x(x¬y),1 = 1 \wedge 1 = (\neg x \vee x) \wedge (y \vee \neg y) \leq (y^x \vee x) \wedge (y^x \vee \neg y) = y^x \vee (x \wedge \neg y),
y xx¬yy¬y=0.y^x \wedge x \wedge \neg y \leq y \wedge \neg y = 0.

Thus the complemented elements form a Heyting subalgebra Comp(H)HComp(H) \hookrightarrow H. Clearly Comp(H)Comp(H) is a Boolean algebra, and clearly if BB is Boolean, then any Heyting algebra map BHB \to H factors uniquely through Comp(H)HComp(H) \hookrightarrow H. This proves the theorem.

To toposes

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 (0,1)(0,1)-topos is a frame or locale.



For 𝒯\mathcal{T} a topos and X𝒯X \in \mathcal{T} any object, the poset Sub(X)Sub(X) of subobjects of XX is a Heyting algebra.

In other words, every topos is a Heyting category.

In particular for X=ΩX = \Omega the subobject classifier, Sub(Ω)Sub(\Omega) is a Heyting algebra.

In 𝒯=\mathcal{T} = Set for every set SS we have that Sub(S)Sub(S) is the Boolean algebra of subset of SS.

More details and examples are spelled out at internal logic.


A frame LL is a Heyting algebra.


By the adjoint functor theorem, a right adjoint xx \Rightarrow - to the map x:LLx \wedge -: L \to L exists since this map preserves arbitrary joins.


The original reference is

  • Arend Heyting,

    Die formalen Regeln der intuitionistischen Logik. I, II, III. Sitzungsberichte der Preußischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse (1930), 42-56, 57-71, 158-169.

A quick introduction can be found in §1.2 of

Last revised on May 6, 2021 at 08:01:41. See the history of this page for a list of all contributions to it.