co-Heyting negation


Category theory

Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




In a co-Heyting algebra it is possible to define a negation operator \sim which validates the law of excluded middle but invalidates the law of non-contradiction dual to the negation in a Heyting algebra.


Let aa be an element of a co-Heyting algebra LL with subtraction \\backslash. The co-Heyting negation of aa , called non a (Lawvere 1991) or the supplement of aa, is defined as a:=1\a\sim a:=1\backslash a.


A bi-Heyting algebra is naturally equipped with two negation operators: the Heyting negation ¬\neg and the co-Heyting supplement \sim. Both coincide in a Boolean algebra considered as a bi-Heyting algebra.

In applications, such co-occuring pairs of negation operators ¬\neg and \sim are the most interesting cases as their combination give rise to adjoint modalities e.g. in mereology they yield thickened boundaries (Stell&Worboys 1997). Beside mereology they have found applications in linguistics, intuitionistic logic and physics.


  • a\sim a minimally supplements aa to truth in the sense that a\sim a is the least xx with ax=1a\vee x=1. This follows from the adjointness of \\backslash which unwinds as ax\sim a\leq x iff 1=ax1=a\vee x.

  • 1=0\sim 1=0 and 0=1\sim 0= 1.

  • \sim can 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 already points to the utility of the co-Heyting negation for paraconsistent logic.

  • The co-Heyting supplement satisfies the dual de Morgan rule (ab)=(a)(b)\sim (a\wedge b)=(\sim a)\vee(\sim b), but not (ab)=(a)(b)\sim (a\vee b) = (\sim a)\wedge (\sim b) in general.

  • For aLa\in L define its core as a\sim\sim a. Then a=a(a)a=\partial a\vee(\sim\sim a). Call aa with a=aa=\sim\sim a regular. Lawvere (1986) proposes in the vein of classical mereology e.g. Tarski 1927 on regions as regular open sets, to consider only regular subbodies as bodies in the full sense.

  • Suppose the element aa of a co-Heyting algebra has a complement xx i.e. ax=1a\vee x = 1 and ax=0a\wedge x = 0, then the complement xx coincides with a\sim a. Because from ax=1a\vee x=1 follows ax\sim a\leq x since a\sim a is the least element with this property; conversely, a=a(ax)=(aa)(ax)=ax\sim a=\sim a\vee (a\wedge x)=(\sim a\vee a)\wedge (\sim a\vee x)=\sim a\vee x whence xax\leq \sim a.

  • A complemented element is obviously regular. Conversely, a regular element aa is complemented since 0=1=(aa)=(a)(a)=aa0=\sim 1=\sim (a\vee\sim a)=(\sim a )\wedge (\sim\sim a)=\sim a\wedge a.

  • In a bi-Heyting algebra: ¬a=¬a1=¬a(aa)=(¬aa)(¬aa)=0(¬aa)=¬aa\neg a=\neg a\wedge 1=\neg a\wedge (a\vee\sim a)=(\neg a\wedge a)\vee (\neg a\wedge \sim a)= 0\vee (\neg a\wedge\sim a)=\neg a\wedge\sim a hence ¬aa\neg a\leq\sim a and we see that ¬\neg is more strongly negative than \sim.


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

  • Y. Gauthier, A Theory of Local Negation: The Model and some Applications , Arch. Math. Logik 25 (1985) pp.127-143. (gdz)

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

  • F. W. Lawvere, Intrinsic Co-Heyting Boundaries and the Leibniz Rule in Certain Toposes , pp.279-281 in Springer LNM 1488 (1991).

  • 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.

  • M. Menni, C. Smith, Modes of Adjointness , J. Philos. Logic 43 no.3-4 (2014) pp.365-391.

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

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

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

  • 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).

  • H. Wansing, Negation , pp.415-436 in Goble (ed.), The Blackwell Guide to Philosophical Logic , Blackwell Oxford 2001.

Revised on July 29, 2016 17:33:11 by Thomas Holder (