Contents

topos theory

foundations

# 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.

## 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.

## Remark

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.

## Constructive proof and classical detour

Let $\mathbb{T}$ be a geometric theory and $U_\mathbb{T}$ its universal model. Recall that $U_\mathbb{T}$ represents deducibility in geometric logic in the sense that a geometric sequent $\sigma$ is deducible from $\mathbb{T}$ precisely iff $U_\mathbb{T}\models \sigma$.

Suppose that $M=f^*(U_\mathbb{T})$ is a $\mathbb{T}$-model in a topos $\mathcal{E}$ where $f:\mathcal{E}\to Set[U_\mathbb{T}]$ is a surjective geometric morphism to the classifying topos of $\mathbb{T}$ and let $(\varphi \vdash_{\vec{x}} \psi)$ be a geometric sequent such that $M\models (\varphi \vdash_{\vec{x}} \psi)$. Now by the definition of the satisfaction relation, this is the same as to say that the monomorphism $\{\vec{x}.\varphi\wedge\psi\}_M\hookrightarrow\{\vec{x}.\varphi\}_M$ is an isomorphism but, $f$ being surjective, $f^*$ is conservative whence $U_\mathbb{T}\models (\varphi \vdash_{\vec{x}} \psi)$ and, accordingly, $(\varphi \vdash_{\vec{x}} \psi)$ is deducible from $\mathbb{T}$ in geometric logic.

This together with the existence of a Boolean cover assured by Barr’s theorem implies the following important

###### Corollary

Let $\mathbb{T}$ be a geometric theory and $\sigma$ a geometric sequent that holds in all $\mathbb{T}$-models in Boolean toposes. Then $\sigma$ is deducible from $\mathbb{T}$ in geometric logic.

In other words, 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. Unfortunately, the proof of Barr’s theorem itself is highly non-constructive whence is of no direct help in finding such constructive replacements for classical proofs of geometric statements.

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).

A proof sketch and a survey of its model-theoretic context is in

• Gonzalo E. Reyes, Sheaves and concepts: A model-theoretic interpretation of Grothendieck topoi , Cah. Top. Diff. Géo. Cat. XVIII no.2 (1977) pp.405-437. (numdam)

For a discussion of the importance of the corollary in constructive algebra see also

• 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 proof-theoretic approaches to Barr’s theorem see

• Sara Negri, Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem , Archive for Mathematical Logic 42 (2003) pp.389–401.