I am a little troubled by the following "paradox" :


Let $X$ be a non trivial (Grothendieck) topos without Set points. 


We want to look at this situation from the point of view of logic: $X$ classifies some geometric theory $T$. The assumption on $X$ means that $T$ is consistent but has no model in Set. This is not in contradiction with Gödel's theorem because the theory $T$ might not be a "finitary first order theory".


We have been able to prove that $X$ doesn't have points, hence we have a proof (using boolean logic and possibly the axiom of choice) that the theory $T$ doesn't have any model.


Let now $Y$ be a Boolean topos with internal axiom of choice. It should be possible to apply the previous proof in the internal logic of $Y$, and then prevent $T$ to have any model in $Y$... But this is not the case: Barr's covering theorem implies there is a topos $Y$ that cover $X$ and hence which has a $T$-model.


Can someone explain me why this is not working ? Or give an example where $T$ and $Y$ are explicit? 



Topos Without point, from the point of view of logic
Here is a concrete example of a consistent geometric theory that has no model in $\mathbf{Set}$ but does have a model in a Boolean Grothendieck topos.


Our base theory $T$ is an expansion of the theory of linear orders with a constant $c\_q$ for each rational number $q$. In geometric form, the base axioms are:
$$x = y \lor x \lt y \lor y \lt x$$
$$x \lt y \land y \lt z \Rightarrow x \lt z$$
$$x \lt x \Rightarrow \bot$$
together with the axioms $c\_q \lt c\_r$ for all pairs of rationals $q \lt r$.
In addition to the above, we add an axiom which says that the $c\_q$'s form a dense subset
$$x \lt y \Rightarrow \bigvee\_q (x \lt c\_q \land c\_q \lt y).$$
A model of $T$ is a linear order with a countable dense subset isomorphic to $\mathbb{Q}$. In other words, models of this theory in $\mathbf{Set}$ are, up to isomorphism, subsets of $\mathbb{R}\cup\lbrace\pm\infty\rbrace$ that contain $\mathbb{Q}$. In particular, models of this theory all have size at most $2^{\aleph\_0}$.


Now expand the theory further to a theory $T\_I$ by adding new constants $d\_i$ for each $i$ in the set $I$, together with the axioms $d\_i \lt d\_j \lor d\_j \lt d\_i$ when $i, j$ are distinct elements of $I$. If $|I| \gt 2^{\aleph\_0}$ then our new theory $T\_I$ has no model in $\mathbf{Set}$. However, in the Grothendieck topos for adding $I$ many Cohen reals side by side (see below) this theory does have a model since $2^{\aleph\_0} \geq |I|$ in that topos. So this is a consistent geometric theory that has a model in some Boolean Grothendieck topos but no model in $\mathbf{Set}$.


(The Grothendieck topos for adding $I$ many Cohen reals side-by-side is obtained by imposing the double-negation topology on the poset category of finite partial functions $I\times\omega\to2$. Note that the double-negation topology is always Boolean. This is not the Barr cover for the classifying topos of $T\_I$ but it's perhaps easier to understand what it looks like.)


