nLab De Morgan Heyting algebra



Category theory

Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




A Heyting algebra is called a De Morgan Heyting algebra if it satisfies the De Morgan laws, which may be considered a weak form of the law of excluded middle. The corresponding logic is an interesting intermediate logic between intuitionistic logic and classical logic.

De Morgan Heyting algebras are also known as Stone algebras or Stone lattices. They are also often called simply de Morgan algebras, although that clashes with a different notion; see De Morgan algebra.


A Heyting algebra MM that satisfies the following equivalent conditions is called a De Morgan Heyting algebra:

  1. For all a,bMa,b \in M: ¬(ab)=¬a¬b\not(a\wedge b) =\not a\vee\not b. (second De Morgan law)

  2. For all aMa\in M: ¬a¬¬a=\not a\vee\not\not a=\top. (weak excluded middle)

  3. For all a,bMa,b\in M: ¬¬(ab)=¬¬a¬¬b\not\not (a\vee b) =\not\not a\vee \not\not b.

Proof of equivalence

(2. implies 1.) First, it is automatic that ¬a¬b¬(ab)\neg a \vee \neg b \leq \neg(a \wedge b). Now, in a distributive lattice such as a Heyting algebra, if xy=x \wedge y = \bot and xz=x \vee z = \top, then yzy \leq z (consider applying y- \wedge y to the second equation). Putting x=¬¬a¬¬bx = \neg \neg a \wedge \neg \neg b and y=¬(ab)y = \neg(a \wedge b) and z=¬a¬bz = \neg a \vee \neg b, we check

¬¬a¬¬b¬(ab)=¬¬(ab)¬(ab)=\neg\neg a \wedge \neg\neg b \wedge \neg(a \wedge b) = \neg\neg (a \wedge b) \wedge \neg(a \wedge b) = \bot

(since ¬¬\neg\neg preserves meets; see Heyting algebra) and

(¬¬a¬¬b)¬a¬b=(¬¬a¬a¬b)(¬¬b¬a¬b)=(¬b)(¬a)==(\neg\neg a \wedge \neg\neg b) \vee \neg a \vee \neg b = (\neg \neg a \vee \neg a \vee \neg b) \wedge (\neg\neg b \vee \neg a \vee \neg b) = (\top \vee \neg b) \wedge (\neg a \vee \top) = \top \wedge \top = \top

whence ¬(ab)¬a¬b\neg(a \wedge b) \leq \neg a \vee \neg b follows.

(1. implies 3.) Given that ¬(xy)=¬x¬y\neg(x \wedge y) = \neg x \vee \neg y for all x,yx, y, put x=¬ax = \neg a and y=¬by = \neg b. Then

¬¬(ab)=¬(¬a¬b)=¬(xy)=¬x¬y=¬¬a¬¬b\neg\neg(a \vee b) = \neg(\neg a \wedge \neg b) = \neg(x \wedge y) = \neg x \vee \neg y = \neg\neg a \vee \neg\neg b

as desired.

(3. implies 2.) We have ¬a=¬¬¬a\neg a = \neg\neg\neg a, and so we may calculate

¬a¬¬a=¬¬¬a¬¬a=¬¬(¬aa)=¬(¬¬a¬a)=¬()=\neg a \vee \neg\neg a = \neg\neg\neg a \vee \neg\neg a = \neg\neg(\neg a \vee a) = \neg(\neg \neg a \wedge \neg a) = \neg(\bot) = \top

as desired.


The dual first De Morgan law ¬(ab)=¬a¬b\not (a\vee b) = \not a\wedge\not b is valid in every Heyting algebra.



  • Francis Borceux, Handbook of Categorical Algebra vol.3 , Cambridge UP 1994. (sections 1.2, 7.3)

  • K. B. Lee, Equational Classes of Distributed Pseudo-Complemented Lattices , Can. J. Math. 22 (1970) pp.881-891. (pdf)

  • M. E. Szabo, Categorical De Morgan Laws , Alg. Universalis 12 (1981) pp.93-102.

Last revised on February 20, 2024 at 05:53:07. See the history of this page for a list of all contributions to it.