18

4

There is a theorem of Deligne in SGA4 that a "coherent" topos (e.g. one on a site where all objects are quasi-compact and quasi-separated) has enough points (i.e. isomorphisms can be detected via geometric morphisms to the topos of sets). I've heard it said that this is a form of Goedel's completeness theorem for first-order logic.

Why is that? I get the intuition that having a model for a formula is supposed to be analogous to a point of a suitable topos, but this is very vague.

I'm sorry for not providing more motivation, but I don't know enough about this connection to do so!

(This was first posted on math.SE here, where it did not (yet) receive a response.)

flag

3 Answers

20

They are indeed formally equivalent. See for instance Johnstone: Topos theory, p. 243 but here is a quick explanation. Given a topos $T$ one may define a geometric theory associated to it consisting of formulas describing essentially the topos. More specifically a geometric morphism from another topos $S$ to $T$ is the same thing as a model for the theory in $S$. In particular if $S$ is the category of sets this a set-theoretical model fo the theory. In general the language of the theory has arbitrary disjunctions leading to theories that in general do not have models. However, if the topos is coherent only finite disjunctions are needed and we are in the realm of the Gödel completeness theorem which then can be interpreted as saying that a coherent topos has enough points. Conversely, given a geometric theory one can associate to it a syntactic site whose objects are the formulas. An implication from a disjunction of formulas to a formula is a covering. The topos of sheaves on this site will then be a classifying topos for the theory (i.e., geometric morphisms to it are the same as models). If the theory is finitary (i.e., uses only finite disjunctions) then the topology is coherent and there are models for the theory by Deligne's theorem.

It is amusing that Deligne's fairly natural example of a topos without points, "measure sheaves" on a measure space for which all points have measure zero thus gives an example of a consistent geometric theory (with countable disjunctions) that doesn't have a model.

link|flag
This is awesome. Thanks! – Akhil Mathew Jun 21 2011 at 13:45
"consistent geometric theory (with countable disjunctions) that doesn't have a model" - what is the meaning of that? Is it theory on the empty Domain of Discourse? – kakaz May 6 at 12:44
1 
I believe Torsten meant it doesn't have a model in the category of sets. I believe any consistent theory in geometric logic has a model in some topos. For example, we can take the theory, build its 'syntactic site', and find a model in the topos of sheaves on its syntactic site. For details see section 4.1 of the exposition by Benjamin Frot mentioned below. – John Baez May 6 at 19:13
7

A good explanation of this topic can now be found here:

link|flag
Thank you for the link to these notes! – Akhil Mathew May 7 at 3:22
-4

Is this is equivalent to the SAT problem for an arbitrary Boolean formula to have an assignment that makes the formula "true"? http://mathworld.wolfram.com/SatisfiabilityProblem.html

link|flag
Probably not, but I suggest asking a separate question if you want to know this. And check mathoverflow.net/howtoask and the FAQ for tips if you do. – David Roberts May 17 at 8:06

Your Answer

Get an OpenID
or

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