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?
Best Answer
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.)