Barr's theorem and constructivity?

Question

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.

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.