Barr's theorem



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.

As surjections permit the transfer of logical properties, Barr’s theorem has the following important consequence:

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.

The proof of Barr’s theorem itself, however, is highly non-constructive.



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.


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

For a discussion of the importance of this theorem in constructive algebra see

  • 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

  • R. Goldblatt, Topoi - The Categorical Analysis of Logic , North-Holland 1982². (Dover reprint)

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

See also the following MO discussion: (link)

Revised on July 2, 2015 16:12:30 by Thomas Holder (