# nLab Barr's theorem

### Context

#### Topos Theory

Could not include topos theory - contents

foundations

## Foundational axioms

foundational axiom

# Contents

## Idea

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.

## Statement

###### Theorem

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.

## References

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)