# nLab Barr's theorem

topos theory

foundations

## Foundational axioms

foundational axiom

# Contents

## Idea

Barr’s theorem states: 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

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 a discussion of the importance of this theorem in constructive algebra.

Revised on April 8, 2011 12:37:52 by Urs Schreiber (131.211.238.40)