nLab
Barr's theorem

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)