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?

  • $\begingroup$ Just wondering. Why is the proof, that X has no set-theoretic models, internal to X? $\endgroup$ – Anton Fetisov Jun 3 '12 at 19:42
  • $\begingroup$ Well, when you have eliminated the impossible, whatever is left, however improbable, must be the truth. Therefore the proof of the inconsistency of your geometric theory $T$ cannot be internalised to $Y$, and this must be because it uses principles that are not available in a general boolean topos with choice. (For example, in ZF, we have unbounded replacement and unbounded separation...) $\endgroup$ – Zhen Lin Jun 3 '12 at 19:47
  • $\begingroup$ To Anton Festisov : not internal to X, but in Y which as axiom of choice and hence boolean logic. My idea (which of course has to be false) was that if you have boolean logic and axiome of choice then you can internalize any set theoretical proof. to Zhen Lin : Yes of course, but I haven't been able to exhibit example of such "improbable" situation... $\endgroup$ – Simon Henry Jun 3 '12 at 20:39
  • 2
    $\begingroup$ Johnstone gives such a theory/topos in Part D of the Elephant, Example 3.4.14, but I must admit I don't understand it... $\endgroup$ – Zhen Lin Jun 3 '12 at 21:34
  • 3
    $\begingroup$ "if you have boolean logic and axiom of choice then you can internalize any set theoretical proof", yes, but you need to use the 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. $\endgroup$ – David Roberts Jun 3 '12 at 22:25

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

  • 21
    $\begingroup$ Let me make explicit how this example detects the flaw in Simon Henry's original argument. The proof that $T_I$ has no models in Set uses the fact that $|I|>2^{\aleph_0}$. That fact is not something that's "proved" and there's no reason for it to remain true in other boolean topoi. $I$ is a parameter, not something defined in set theory. If one used, instead, a definition of it, say the cardinal $(2^{\aleph_0})^+$, then that would define a different $I^′$ in topoi where the continuum has been enlarged. $\endgroup$ – Andreas Blass Jun 4 '12 at 11:07
  • $\begingroup$ This looks like a funky way of talking about generic extensions. $\endgroup$ – Monroe Eskew May 11 '17 at 14:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.