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 for a coherent topos with set of points . General toposes 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:
The proof of Barr’s theorem itself, however, is highly non-constructive.
where satisfies the axiom of choice.
Deligne's completeness theorem says that a coherent Grothendieck topos has enough points in 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:
For a discussion of the importance of this theorem in constructive algebra see
For proof-theoretic approaches to Barr’s theorem see
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.
See also the following MO discussion: (link)