Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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

share|improve this question
add comment

2 Answers

up vote 21 down vote accepted

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.

share|improve this answer
    
This is awesome. Thanks! –  Akhil Mathew Jun 21 '11 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 '13 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 '13 at 19:13
add comment

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

share|improve this answer
    
Thank you for the link to these notes! –  Akhil Mathew May 7 '13 at 3:22
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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