nLab Barr's theorem



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



Barr’s theorem was originally conjectured by William Lawvere as an infinitary generalization of the Deligne completeness theorem for coherent toposes which can be expressed as the existence of a surjection 𝒮/K\mathcal{S}/K\to\mathcal{E} for a coherent topos \mathcal{E} with set of points KK. General toposes \mathcal{E} may fail to have enough points but Michael Barr showed that a surjection from a suitable Boolean topos still exists.



If \mathcal{E} is a Grothendieck topos, then there is a surjective geometric morphism

\mathcal{F} \to \mathcal{E}

where \mathcal{F} satisfies the axiom of choice.


Deligne's completeness theorem says that a coherent Grothendieck topos has enough points in SetSet and this corresponds to the Gödel-Henkin completeness theorem for first-order theories. Similarly, Barr’s theorem can interpreted as saying that a Grothendieck topos has sufficient Boolean-valued points and is in turn closely related to Mansfield’s Boolean-valued completeness theorem for infinitary first-order theories.

Constructive proof and classical detour

Let 𝕋\mathbb{T} be a geometric theory and U 𝕋U_\mathbb{T} its universal model. Recall that U 𝕋U_\mathbb{T} represents deducibility in geometric logic in the sense that a geometric sequent σ \sigma is deducible from 𝕋\mathbb{T} precisely iff U 𝕋σU_\mathbb{T}\models \sigma .

Suppose that M=f *(U 𝕋)M=f^*(U_\mathbb{T}) is a 𝕋\mathbb{T}-model in a topos \mathcal{E} where f:Set[U 𝕋]f:\mathcal{E}\to Set[U_\mathbb{T}] is a surjective geometric morphism to the classifying topos of 𝕋\mathbb{T} and let (φ xψ) (\varphi \vdash_{\vec{x}} \psi) be a geometric sequent such that M(φ xψ)M\models (\varphi \vdash_{\vec{x}} \psi) . Now by the definition of the satisfaction relation, this is the same as to say that the monomorphism {x.φψ} M{x.φ} M\{\vec{x}.\varphi\wedge\psi\}_M\hookrightarrow\{\vec{x}.\varphi\}_M is an isomorphism but, ff being surjective, f *f^* is conservative whence U 𝕋(φ xψ)U_\mathbb{T}\models (\varphi \vdash_{\vec{x}} \psi) and, accordingly, (φ xψ)(\varphi \vdash_{\vec{x}} \psi) is deducible from 𝕋\mathbb{T} in geometric logic.

This together with the existence of a Boolean cover assured by Barr’s theorem implies the following important


Let 𝕋\mathbb{T} be a geometric theory and σ\sigma a geometric sequent that holds in all 𝕋\mathbb{T}-models in Boolean toposes. Then σ\sigma is deducible from 𝕋\mathbb{T} in geometric logic.

In other words, if a statement in geometric logic is deducible from a geometric theory using classical logic and the axiom of choice, then it is also deducible from it in constructive mathematics. Unfortunately, the proof of Barr’s theorem itself is highly non-constructive whence is of no direct help in finding such constructive replacements for classical proofs of geometric statements.


Extensive discussion of the context of Barr’s theorem is in chapter 7 of:

  • P. T. Johnstone, Topos Theory , Academic Press New York 1977 (Dover reprint 2014).

A proof sketch and a survey of its model-theoretic context is in

  • Gonzalo E. Reyes, Sheaves and concepts: A model-theoretic interpretation of Grothendieck topoi , Cah. Top. Diff. Géo. Cat. XVIII no.2 (1977) pp.405-437. (numdam)

For a discussion of the importance of the corollary in constructive algebra see also

  • Gavin Wraith, Intuitionistic algebra: some recent developments in topos theory In: Proceedings of the International Congress of Mathematicians (Helsinki, 1978), pages 331–337, Helsinki, 1980. Acad. Sci. Fennica. (pdf)

For proof-theoretic approaches to Barr’s theorem see

  • Sara Negri, Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem , Archive for Mathematical Logic 42 (2003) pp.389–401.

For the connection with the Boolean-valued completeness theorem see also

  • R. Goldblatt, Topoi - The Categorical Analysis of Logic , North-Holland 1982². (Dover reprint New York 2006; project euclid)

  • R. Mansfield, The Completeness Theorem for Infinitary Logic , JSL 37 no.1 (1972) pp.31-34.

  • Michael Makkai, Gonzalo E. Reyes, First-order Categorical Logic , LNM 611 Springer Heidelberg 1977.

Last revised on May 9, 2020 at 14:33:34. See the history of this page for a list of all contributions to it.