I am a little troubled by the following "paradox" :
Let $X$ be a non trivial (Grothendieck) Topos without point.
We want to look this situation from the point of view of logic, $X$ classify some geometric theory $T$. The assumption on $X$ means that $T$ is consistent but have no model in Set. This is not in contradiction with Godel theorem because the theory $T$ might not be a "finitary first order theory".
But as we have been able to proove that $X$ doesn't have point, hence we have a proof (using boolean logic and possibly the axiome of choice) that the theory $T$ doesn't have any model.
So let now $Y$ 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 : The Barr covering theorem imply that there is a such topos $Y$ that cover $X$ and hence which have a $T$-model.
Can someone explain me why this is not working ? or give an example where T and Y are explicit ?
Thank you !