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?

stack semantics, not just the usual internal logic (aka Mitchell-Benabou languge+Kripke-Joyal semantics) - see ncatlab.org/michaelshulman/show/stack+semantics. This takes care of the unbounded replacement and separation. The only thing you are lacking to actually define ETCS (a set theory) is well-pointedness and an axiom of infinity/nno. $\endgroup$ – David Roberts Jun 3 '12 at 22:25