# Barr's theorem and constructivity?

Barr's covering theorem assert that any Gorthendieck topos can be covered by a Grothendieck topos (even a locale) satisfying the axiom of choice (and hence also the law of excluded middle). Its corrolary is that if one can deduce from geometrical hypothesis $H$ a geometric conclusion $C$ using (AC) and classical logic, then one can deduce $C$ from $H$ in any Grothendieck topos.

The proof of this theorem rely heavily on the axiom of choice (actually on the fact that the topos of sheaf over a boolean locale satisfy the axiom of choice) and hence is not valid in a general elementary topos.

My question is : Is there any know examples of something that can be proved using Barr's theorem (a deduction of geometric conclusion from geometric hypothesis which can be proved using (AC) ) and which is false in some elementary topos (preferably with a natural number object) ?

Also, could you confirm me that the weaker form of barr's theorem "every topos can be covered by a boolean topos" is actualy true also for elementary topos ? (it seems that one can consider the topos of double negation sheaf over the internal frame of nuclei of $\Omega$ in every elementary topos)

Edit : Thinking about Zhen Lin answer and comment I realize that my question was unclear : what I am looking for is an exemple of a geometric theory $H$ possibly stated in the language of some elementary topos, which have a geometric consequence $C$ deducible using the axiom of choice such that $C$ cannot be deduce from $H$ constructively. ie, I'm essentially looking for a proof that barr's theorem can't be constructive. In this situation, the completeness theorem for geometric logic (mentioned in Zhen Lin's comment) does not apply because as the theory $H$ can be stated in an elementary topos it does not mean anything to say that $C$ can be deduced from $H$ in any Grothendieck toposes.

• You've misunderstood: the completeness theorem I'm referring to is the one that says that any coherent sequent in a coherent theory that is true in all Grothendieck toposes can also be proved using the rules of inference of coherent logic. In particular it is valid in elementary toposes. – Zhen Lin Sep 26 '13 at 13:57
• Does the edit mean that you want to allow $H$ and $C$ to be in a language internal to an elementary topos $E$, and that the infinitary disjunctions of geometric logic can be indexed by objects of $E$, and that the "set" $H$ itself might not be a "real" set but an object of $E$, and that deducibility is to be interpreted internally in $E$? Or only some of these? "Deducible using the axiom of choice" looks suspicous in $E$ if $E$ doesn't satisfy the (internal) AC. Did you perhaps want the deducibility to work also in all topoi defined over $E$? – Andreas Blass Sep 26 '13 at 14:08
• Yes that's what I mean. What I call the logical form of Barr's theorem is "If from a family of geometric hypothesis I can deduce a geometric conclusion using the axiom of choice then I can deduce it also constructively". This theorem hold internally in any Grothendeick topos. But one generally said that it is non-constructive, I want a proof of this non-constructivity by a counterexample in a topos (which has to be elementary.) – Simon Henry Sep 26 '13 at 14:45
• @SimonHenry That is a very different question than your original question! But the "logical form of Barr's theorem" is not obviously true in the internal logic of even a Grothendieck topos – for one thing, a topos that is "internally localic" may not actually be localic. – Zhen Lin Sep 26 '13 at 16:28
• Consider a nondegenerate but non-Boolean Grothendieck topos $E$. Diaconescu's proof that AC implies excluded middle can be used to show that an internal version of choice fails in $E$. (More precisely, one can give an object $A$ such that the internal sentence "for every equivalence relation on $A$, the map from $A$ to the quotient has a section" is false.) So in $E$, from any set (even the empty set) of geometric hypotheses plus AC one can deduce anything, even the geometric conclusion "false", because AC fails. That inference won't work constructively. – Andreas Blass Sep 26 '13 at 17:58

1. In every Grothendieck topos, the following sequent is valid for the natural numbers object $N$, $$x : N \vdash \bigvee_{n : \mathbb{N}} x = s^n (z)$$ where $\mathbb{N}$ is the set of natural numbers, $s : N \to N$ is the internal successor operation, and $z : 1 \to N$ is the zero element. In words, "every natural number is standard". This can be proved directly without appealing to any kind of boolean completeness theorem. However, it is false in any non-standard topos, provided one makes the appropriate allowances to deal with the fact that such toposes do not have all infinite colimits: note that in every cocomplete topos, the indicated sequent is valid if and only if the collection $\{ s^n \circ z : 1 \to N \}$ is a jointly epimorphic family. It goes without saying that non-standard toposes exist: for instance, take the elementary topos associated with any non-trivial ultrapower of $V_{\omega + \omega}$.
2. Every elementary topos can be covered by a boolean topos: see Proposition 4.5.23 in [Sketches of an elephant, Part A]. Apparently this is a theorem of Freyd in [1972, Aspects of topoi], but I have not found the precise statement there. The construction is as follows: for an elementary topos $\mathcal{E}$, let $q$ be the local operator on $\mathcal{E}_{/ \Omega}$ defined by the formula $q (x) = ((x \Rightarrow t) \Rightarrow t)$, where $\Rightarrow$ is the Heyting implication and $t$ is the generic subobject $1 \rightarrowtail \Omega$ in $\mathcal{E}$ considered as a truth-value in $\mathcal{E}_{/ \Omega}$; then the obvious geometric morphism $\mathbf{sh}_{q} (\mathcal{E}_{/ \Omega}) \to \mathcal{E}$ is a geometric surjection.