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?