Topos Without point, from the point of view of logic.

Question

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 !

Answer 1

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.)