Hello !

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 !

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. – David Roberts Jun 3 '12 at 22:25