basic constructions:
strong axioms
further
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 $\mathcal{S}/K\to\mathcal{E}$ for a coherent topos $\mathcal{E}$ with set of points $K$. 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
where $\mathcal{F}$ satisfies the axiom of choice.
Deligne's completeness theorem says that a coherent Grothendieck topos has enough points in $Set$ 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.
Michael Makkai, Gonzalo E. Reyes, First-order Categorical Logic , LNM 611 Springer Heidelberg 1977.
See also the following MO discussion: (link)