co-Heyting algebra



Category theory

Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




When the lattice of open subsets of a topological space is the primordial example of a Heyting algebra then its dual lattice of closed subsets is the primordial example of a co-Heyting algebra.

In general, co-Heyting algebras are dual to Heyting algebras and like them come equipped with non-Boolean logical operators that make them interesting players in modal, paraconsistent, and co-intuitionistic logic, linguistics, topos theory, continuum physics, quantum theory and in mereology.


A co-Heyting algebra is a bounded distributive lattice LL equipped with a binary subtraction operation \:L×LL \backslash :L\times L\to L such that x\yzx\backslash y\leq z iff xyzx\leq y\vee z.1

A bi-Heyting algebra is a bounded distributive lattice LL that carries a Heyting algebra structure with implication \Rightarrow and a co-Heyting algebra structure with subtraction \\backslash.


  • Co-Heyting algebras were initially called Brouwerian algebras . Bi-Heyting algebras were introduced and studied in a series of papers by Cecylia Rauszer in the 1970s who called them semi-Boolean algebras which suggests to view them as a generalization of Boolean algebras.

  • A topos \mathcal{E} such that the lattice sub(X)sub(X) of subobjects is a bi-Heyting algebra for every object XX\in\mathcal{E} is called a bi-Heyting topos.


  • The lattice of closed subsets of a topological space is a co-Heyting algebra with X\Y=XY c¯X\backslash Y=\overline{X\cap Y^c}\quad.

  • A Boolean algebra provides a (degenerate) example of a bi-Heyting algebra by setting xy:=¬xyx\Rightarrow y:=\neg x\vee y and x\y:=x¬yx\backslash y:=x\wedge\neg y.

  • An irreflexive comparison, such as an apartness relation or a linear order, is a (0,1)-category enriched on the co-Heyting algebra Ω op\Omega^\op, where Ω\Omega is the Heyting algebra of truth values.


  • a\b=0a\backslash b=0 iff a\b0a\backslash b\leq 0 iff ab0a\leq b\vee 0 iff aba\leq b. In particular, a\a=0a\backslash a=0.

  • As _\x\backslash x has a right adjoint it preserves colimits hence: (ab)\x=(a\x)(b\x)(a\vee b)\backslash x =(a\backslash x)\vee (b\backslash x)\quad.

  • a\0a\0a\backslash 0\leq a\backslash 0 iff a0(a\0)a\leq 0\vee (a\backslash 0) iff aa\0a\leq a\backslash 0\quad. On the other hand, a0aa\leq 0\vee a and the adjunction yield a\0aa\backslash 0\leq a\quad, hence a\0=aa\backslash 0 = a\quad.

  • Suppose abxa\leq b\vee x then a\bxa\backslash b\leq x. As from a\ba\ba\backslash b\leq a\backslash b follows ab(a\b)a\leq b\vee (a\backslash b), hence a\b={x|abx}a\backslash b =\Wedge\{x|a\leq b\vee x\}\quad.

  • The subtraction operation permits to define the co-Heyting negation :LL\sim: L\to L, called non a in Lawvere (1991), by setting a:=1\a\sim a:=1\backslash a.

  • \sim in turn can then be used to define the co-Heyting boundary operator :LL\partial :L\to L by a:=aa\partial a:=a\wedge\sim a. That a\partial a is not necessary trivial is dual to the non-validity of the tertium non datur for general Heyting algebras and points to the utility of co-Heyting algebras for paraconsistent logic.

  • In bi-Heyting toposes like e.g. essential subtoposes of presheaf toposes (Lawvere, Reyes), the co-Heyting algebra operations are generally not preserved by inverse image functors, so that the co-Heyting logical operators are subject to de re and de dicto effects. The parallel between this and the commutator in quantum mechanics has been suggested by Lawvere thereby somewhat anticipating the view of Döring (2013).


  • G. Bellin, Categorical Proof Theory of Co-Intuitionistic Linear Logic , arXiv:1407.341 (2014). (pdf)

  • G. Bezhanishvili, N. Beshanishvili, D. Gelaia, A. Kurz, Bitopological duality for distributive lattices and Heyting algebras , Math. Struc. Comp. Sci. 20 no.3 (2010) pp.359-393. (preprint)

  • A. Döring, Topos-based Logic for Quantum Systems and Bi-Heyting Algebras , arXiv:1202.2750 (2013). (pdf)

  • M. La Palme Reyes, J. Macnamara, G. E. Reyes, H. Zolfaghari, The non-Boolean logic of natural language negation , Phil. Math. 2 no.1 (1994) pp.45-68.

  • M. La Palme Reyes, J. Macnamara, G. E. Reyes, H. Zolfaghari, Models for non-Boolean negation in natural languages based on aspect analysis , pp.241-260 in Gabbay, Wansing (eds.), What is Negation?, Kluwer Dordrecht 1999.

  • M. La Palme Reyes, G. E. Reyes, H. Zolfaghari, Generic Figures and their Glueings , Polimetrica Milano 2004.

  • F. W. Lawvere, Introduction , pp.1-16 in Lawvere, Schanuel (eds.), Categories in Continuum Physics , Springer LNM 1174 1986.

  • F. W. Lawvere, Intrinsic Co-Heyting Boundaries and the Leibniz Rule in Certain Toposes , pp.279-281 in A. Carboni, M. Pedicchio, G. Rosolini (eds.) , Category Theory - Proceedings of the International Conference held in Como 1990 , LNM 1488 Springer Heidelberg 1991.

  • T. Mormann, Heyting Mereology as a Framework for Spatial Reasoning , Axiomathes 23 no.1 (2013) pp.237-264. (draft)

  • G. E. Reyes, H. Zolfaghari, Bi-Heyting Algebras, Toposes and Modalities , J. Phi. Logic 25 (1996) pp.25-43.

  • C. Rauszer, Semi-Boolean algebras and their applications to intuitionistic logic with dual operations , Fund. Math. 83 no.3 (1974) pp.219-249. (pdf)

  • J.G. Stell, M.F. Worboys, The algebraic structure of sets of regions , pp.163-174 in Hirtle, Frank (eds.), Spatial Information Theory, Springer LNCS 1329 (1997).

  • M. H. Stone, Topological representation of distributive lattices and Brouwerian logics , Cas. Mat. Fys. 67 (1937) pp.1-25. (pdf)

  • F. Wolter, On logics with coimplication , J. Phil. Logic 27 (1998) pp.353-387. (draft)

  1. Existence of \\backslash amounts to an adjunction _\yy\backslash y\dashv y\vee_ and the existence of a left adjoint implies that yy\vee_ preserves limits \wedge hence the assumption of distributivity in the definition is redundant and has been put in for emphasis only.

Last revised on May 6, 2021 at 10:09:56. See the history of this page for a list of all contributions to it.