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.

  • $\begingroup$ 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. $\endgroup$
    – Zhen Lin
    Sep 26, 2013 at 13:57
  • 1
    $\begingroup$ 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$? $\endgroup$ Sep 26, 2013 at 14:08
  • $\begingroup$ 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.) $\endgroup$ Sep 26, 2013 at 14:45
  • 1
    $\begingroup$ @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. $\endgroup$
    – Zhen Lin
    Sep 26, 2013 at 16:28
  • 2
    $\begingroup$ 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. $\endgroup$ Sep 26, 2013 at 17:58

1 Answer 1

  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.

  • $\begingroup$ Your example is interesting, but I am interested in something which is specifically a consequence of Barr covering theorem. In this case, this formula is a consequence of the existence of a geometric morphism to set. $\endgroup$ Sep 15, 2013 at 19:42
  • 3
    $\begingroup$ By the completeness theorem, anything that can be proved with Barr's theorem can be proved without it. There's also the problem that elementary toposes simply do not interpret geometric logic in full – only the coherent fragment. $\endgroup$
    – Zhen Lin
    Sep 15, 2013 at 22:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.