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