nLab
Barr's theorem

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Foundations

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)