Arch. Math. Logic (1999) 38: 79–101

c Springer-Verlag 1999

A topological completeness theorem Carsten Butz1,2 1 2

Mathematisch Instituut, Universiteit Utrecht, Postbus 80.010, NL–3508 TA Utrecht, The Netherlands Current address: BRICS? , Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK–8000 Aarhus C, Denmark. email: [email protected]

Received: 27 September 1996 / Revised version: 15 January 1998

Abstract. We prove a topological completeness theorem for infinitary geometric theories with respect to sheaf models. The theorem extends a classical result of Makkai and Reyes, stating that any topos with enough points has an open spatial cover. We show that one can achieve in addition that the cover is connected and locally connected.

1 Introduction Sheaf models of infinitary first order theories were studied intensively in [15]. They are models in Grothendieck toposes and subsume Heyting valued models, boolean valued models, Kripke models, and permutation models. Of particular interest are so called geometric theories T (see Definition 2.1). To these theories one can associate a particular topos B(T) together with a generic (term) model U in B(T). The model U is generic since for any Grothendieck topos F there is an equivalence between the category of models of T in F and the category of geometric morphisms from F to B(T). Given such a geometric morphism ϕ: F → B(T) the corresponding model Φ is obtained as ϕ∗ U (see below). There are usually not enough models in Sets to test semantically whether a given geometric sequent holds in all models of T in all Grothendieck toposes. If this is the case we say that T satisfies the completeness theorem. ? BRICS: Basic Research in Computer Science, Centre of the Danish National Research Foundation.

80

C. Butz

In this paper we will prove the following topological completeness theorem: Theorem Let T be a geometric theory satisfying the completeness theorem. There exists a topological space X and an OX–valued model Φ of T (a model Φ of T in Sh(X) corresponding to a geometric morphism ϕ: Sh(X) → B(T)) such that for any first order formula σ we have Φ |= σ if and only if U |= σ (the geometric morphism ϕ is an open surjection). (ii) Any map in Sh(X) between first order definable sheaves is geometrically definable (functional completeness). (iii) The inverse image ϕ∗ preserves function types of first order definable types. (i)

Part (ii) and (iii) of the theorem extend a well known result by Makkai and Reyes, stating that any topos with enough points has an open spatial cover ([15], Theorem 6.3.3). This result appears here as part (i) of the Theorem. A geometric morphism is called connected if the inverse image is full and faithful. The geometric morphism ϕ we construct in this paper is connected, although part (ii) of the Theorem states something slightly weaker: ϕ∗ is full (and faithful by (i)) on arrows between first order definable sheaves. It is not difficult to use the techniques of Section 6 to show that ϕ∗ is full. Details are worked out in [3]. Part (iii) of the theorem needs some explanation. Even if the language has already function types there is no guaranty that these function types are interpreted by exponentials of sheaves. But one can always add new function types and interpret them in the universal model in the standard way, namely by exponentials. These new function types are interpreted in Φ by exponentials of sheaves too. A geometric morphism is called locally connected if its inverse image commutes with internal product functors. This implies in particular that the inverse image preserves all exponentials. Again, it is shown in [3] that the geometric morphism ϕ occurring in the theorem is locally connected, of which part (iii) is a particular instance. To keep our presentation within a logical framework we present proofs only of those consequences of ‘ϕ is connected and locally connected’ which have a clear logical meaning in terms of the universal model U in B(T). The geometric morphism is discussed in full detail in the author’s Ph.D. thesis [3], and in a topological framework in [6, 5]. In particular, it is shown that ϕ is acyclic, so that it induces isomorphisms in cohomology. The space X will contain the models of T in Sets, each model equipped with some extra structure.

A topological completeness theorem

81

We start reviewing sheaf models and fixing our notation. Then we define the space X, the model Φ, and take a closer look at the topology of the spaces involved. The rest of the paper is occupied by the proof of the theorem. A small appendix at the end of the paper relates our theorem to previous work, mainly of A. Joyal and co-workers. Acknowledgements. I would like to thank Ieke Moerdijk for his encouragement and many stimulating discussions. An anonymous referee gave valuable comments on an earlier version of this paper. This research was supported by a grant of the state Baden-W¨urttemberg, Germany, by a DAAD/NUFFIC grant, by a scholarship of the University of Utrecht, and by a grant from a project funded by the Netherlands Organization for Scientific Research NWO.

2 Review of sheaf models We assume that the reader is familiar with (Grothendieck) toposes, see for example [15], [8] or [14]. For sheaves over topological spaces we refer as well to [17]. In particular, we assume that the reader has seen the basic definition of a site (C, J), sheaves on a site and maps between sheaves. These data together yield the Grothendieck topos Sh(C, J). Maps between Grothendieck toposes are called geometric morphisms. A geometric morphism f : Sh(D, K) → Sh(C, J) is a pair of functors f∗ : Sh(D, K) o

/

Sh(C, J): f ∗ ,

f ∗ left adjoint to f∗ , and f ∗ is moreover left exact (preserves finite limits). f ∗ is called the inverse image and f∗ the direct image. Maps between geometric morphisms are natural transformations. In this way we get the category of geometric morphisms from Sh(D, K) to Sh(C, J), denoted by Hom(Sh(D, K), Sh(C, J)). A Grothendieck topos E has a rich structure. In particular we can speak about models of an infinitary first order theory T in the topos E as follows (cf. [14], Section X.2 and [15], Chapter 2): An interpretation M of a language assigns to each sort Y an object Y (M) in E, to each constant c of sort Y a global element c(M) : 1 → Y (M) , to each function symbol f : Y → Y an (M) arrow f (M) : Y → Y (M) and similar for relation symbols R. (Here we introduce the convention that Y stands for a sequence Y1 , . . . , Yn of sorts (M) (M) (M) and Y for Y1 × · · · × Yn .) If we have a one sorted language we simply write M for the underlying object. Interpreting the logical connectives and quantifiers in the canonical way we get for each formula ψ(y: Y ) a subobject {y | ψ(y)}(M) ,→ Y

(M)

.

82

C. Butz

For a closed formula τ we say that M is a model of τ (M |= τ ) if {· | τ }(M) (which is a subobject of 1E ) is equal to 1E . In the same way M |= T means M |= τ for all τ ∈ T. With the natural definition of morphisms between models we get the category Mod(T, E) of models of T in E. If E = Sh(X), the topos of sheaves over a topological space, we speak about topological models. The category of models in the topos Sh(H) of sheaves over a (complete) Heyting algebra H is naturally equivalent to the category of H–valued models, see [7]. Models in the topos BG of G–sets (G a group) are sometimes referred to as permutation models. We are mainly interested in geometric theories: Definition 2.1 A formula ψ(y) is called geometric if it is W built up by atomic formulas, finite conjunction ∧, arbitrary disjunction , the truth values true > and false ⊥, and existential quantification ∃. A theory T is called geometric if all its axioms are (equivalent to formulas) of the form ∀y(ψ1 (y) → ψ2 (y)) for ψ1 and ψ2 geometric. Examples are given by the standard axiomatizations of linear orders with or without endpoints, groups or rings. The inverse image f ∗ of a geometric morphism f : F → E induces for any theory T a functor f ∗ : Mod(T, F) → Mod(T, E) (see [14], X.3.6). With this observation the main theorem relating topos theory and logic becomes as follows: Theorem 2.2 For any infinitary geometric theory T there exists a unique Grothendieck topos B(T) such that for all Grothendieck toposes F there is an equivalence ' Mod(T, F) → Hom(F, B(T)), natural in F. Conversely, any Grothendieck topos E is of the form B(T) for some geometric theory T. 2 Uniqueness in this theorem is meant as “unique up to equivalence”. We say that B(T) is the classifying topos of the theory T. The theory classified by a topos is not unique. In the equivalence of the theorem the identity geometric morphism B(T) → B(T) corresponds to a model U of T in B(T), called the generic model (or universal model) of T. The model U is uniquely determined up to isomorphism. It is universal in the sense that for any model M of T in F there exists a geometric morphism f : F → B(T) such that f ∗ U ' M. The inverse image of a geometric morphism does usually not preserve the full internal first order logic of a topos. If this is true the geometric morphism is called open (see [9], [14]). A geometric morphism is called surjective if the inverse image is faithful. Both notions can be characterized model theoretically. In the following proposition we denote by Thg (−) the

A topological completeness theorem

83

class of all geometric sequents ∀y(ψ1 (y) → ψ2 (y)) for ψ1 , ψ2 geometric formulas which are true in a model. Similarly, Thfo (−) denotes the class of all closed first order formulas which are true in a model. Proposition 2.3 Let T be a geometric theory, ϕ: F → B(T) a geometric morphism with corresponding model Φ in F. Let U denote the universal model in B(T). (i) ϕ is surjective if and only if Thg (U) = Thg (Φ). (ii) ϕ is open if and only if Thfo (U) ⊂ Thfo (Φ). (iii) ϕ is an open surjection if and only if Thfo (U) = Thfo (Φ). Proof. This is implicitly in [15]. An explicit proof is given in [4].

2

If Thg (U) = Thg (Φ) we say that Φ is a conservative model of T. We remind the reader of the provability relation ` given in [15]. For a geometric theory T and geometric formulas ψ1 (y) and ψ2 (y) we have T ` ∀y(ψ1 (y) → ψ2 (y)) if and only if U |= ∀y(ψ1 (y) → ψ2 (y)). Definition 2.4 A geometric theory T is said to satisfy the completeness theorem if T |=Sets ∀y(ψ1 (y) → ψ2 (y)) implies T ` ∀y(ψ1 (y) → ψ2 (y)). (Here T |=Sets σ stands for ‘all models of T in Sets satisfy σ.) Thus, a theory T satisfies the completeness theorem if there are enough models in Sets to test semantically whether a geometric sequent ∀y(ψ1 (y) → ψ2 (y)) is derivable or not. It is well understood that T satisfies the completeness theorem if and only if B(T) has enough points: The geometric morphisms p: Sets → B(T) form a jointly surjective family (see for example [15], Lemma 6.1.4). Most toposes arising in geometric practice have enough points. We mention the toposes Sh(X) for X a topological space, BG for G a discrete or continuous group, or – as a less trivial example – the e´ tale topos Sh(Xe´t ) associated to a scheme X in algebraic geometry (see [1]). According to Deligne’s theorem (Deligne, Appendix to Expos´e VI in [1]) any ‘coherent’ topos has enough points. This can be strengthened to ‘separable’ toposes ([15], Theorem 6.4.2). In logical terms, a Grothendieck topos is coherent iff it is equivalent to the classifying topos of a finitary geometric theory (a geometric theory formulated in Lωω ). A topos is separable iff it is equivalent to the classifying topos of a geometric theory formulated in a countable fragment of Lω1 ω . Even though we consider on the right side of ` or |= only geometric sequents (but with possibly infinitary disjunctions) the two statements above are easily seen to be equivalent to classical completeness theorems: the first one to G¨odel’s completeness theorem for finitary logic and the second to the completeness theorem for countable fragments of Lω1 ω ([12], Section I.4). This relationship is discussed in detail in [15]. Finally, the toposes usually used to model synthetic differential geometry (SDG) [13, 16] probably do not have enough points. But we mention that

84

C. Butz

there are toposes with enough points that meet the axioms of SDG: Such toposes are constructed in a similar way as classifying toposes of geometric theories using a syntactic site (see [2] for the general account). A set of enough points of such a topos is given by a set of enough Henkin models of SDG. We sketch the construction of B(T) for a geometric theory T formulated in Lλω . For simplicity we assume to have a one–sorted language. A syntactic site Syn(T) for B(T) can be defined in terms of the provability relation `. – Objects of Syn(T) are equivalence classes [ψ(y)] of geometric formulas in Lλω . Two such formulas ψ1 (y 1 ) and ψ2 (y 2 ) are equivalent if T ` ∀y(ψ1 (y) ↔ ψ2 (y)), where y is a set of fresh variables. – Arrows from [δ(w)] to [ψ(y)] are equivalence classes [σ(w, y)] of geometric formulas in Lλω such that σ is provable functional: T ` ∀w∀y(σ(w, y) → δ(w) ∧ ψ(y)) T ` ∀w(δ(w) → ∃yσ(w, y)) T ` ∀w∀y∀z(σ(w, y) ∧ σ(w, z) → y = z) (We note that one has to take equivalence classes of provable functional formulas to get the composition of arrows well-defined. However, it is enough to take formulas instead of equivalence classes of formulas as objects of the category Syn(T).) – A family of arrows {[σi (wi , y)]: [δiW (wi )] → [ψ(y)]}i∈I is a cover if it is a provable cover: T ` ∀y(ψ(y) → I ∃wi σi (wi , y)). The category Syn(T) has all finite limits and the Grothendieck topology is subcanonical, see [14] or [15] for details. B(T) is now defined to be Sh(Syn(T)). The Yoneda map y: Syn(T) → B(T) gives U as follows: U = y([y = y]) were y is a free variable, f (U) : U

→ U = y([f (z) = y]): y([z = z]) → y([y = y])

R(U) ,→ U = y([R(y)] ,→ y([y = y]). For every geometric formula ψ(y) in Lλω there is an isomorphism {y | ψ(y)}(U) ' y([ψ(y)]). Given a geometric morphism ϕ: F → B(T) and corresponding model Φ of T in F we have for each geometric formula ψ(y) canonical isomorphisms {y | ψ(y)}(Φ) ' ϕ∗ {y | ψ(y)}(U) ' ϕ∗ y([ψ(y)]), the latter of course only if ψ is bounded, i.e., if ψ belongs to Lλω . The universal model U has the property that any subobject S ,→ U is geometrically definable: there exists a geometric formula ψ(y) such that S ' {y | ψ(y)}(U) .

A topological completeness theorem

85

(But note that if the theory T is formulated in Lλω such geometric formulas ψ(y) may only exist in Lλ0 ω for λ0 > λ.) 3 Definition of the space of models Let T be a geometric theory satisfying the completeness theorem. We assume for simplicity that T is formulated in a one–sorted language. We denote by S the fixed set of function and relation symbols. Constants are treated as 0–ary functions. We always suppress the arity of these symbols to keep notations simple. For a cardinal κ let Ptsκ (T) denote a fixed set of representatives of isomorphism classes of models such that the cardinality of the model is bounded by κ. By a downward L¨owenheim–Skolem argument there exists a cardinal κ such that the models M ∈ Ptsκ (T) form a set of enough models: For two geometric formulas ψ1 (y) and ψ2 (y) we have T ` ∀y(ψ1 (y) → ψ2 (y)) iff

M |= ∀y(ψ1 (y) → ψ2 (y)) for all M ∈ Ptsκ (T).

We fix such a cardinal κ. The space of models we are going to define will consist of all models M of T, bounded by κ and equipped with some extra structure: Definition 3.1 A κ–to–one enumeration of a model M is a map α: K → M, K ⊂ κ, such that for each a ∈ M the set α−1 (a) is cofinal in κ. We write α: κ ; M for such a map. Note that we do not distinguish between a model and its underlying set. If κ is a regular cardinal the definition is equivalent to say that each set α−1 (a) has cardinality κ. Since we use κ only as a large set to supply names for elements in a model M (along a map α) we denote elements of κ (the ordinals less than κ) by the letters k, l, m, . . ., and not by λ, β, . . . as would be more standard. Let X be the space with elements pairs (M, α) where M ∈ Ptsκ (T) and α: κ ; M. If necessary we write such an element as p = (Mp , αp ). The topology on X is generated by the following subbase: Uk,l = {(M, α) | α(k) = α(l)} Uk,l,f = {(M, α) |

f (M) (α(k))

= α(l)}

Uk,R = {(M, α) | R(M) (α(k))}

for k, l ∈ κ, for ki , l ∈ κ, f ∈ S, for ki ∈ κ, R ∈ S.

86

C. Butz

Here α(k) stands for the tuple (α(k1 ), . . . , α(kn )) and it is part of the definitions that the α(k), . . . are defined. Since expressions like f (M) (α(k)) = α(l) or M |= f (α(k)) = α(l) are long and hard to read we write them mostly as M |= f (k) = l. This makes sense since the elements k ∈ κ where α(k) is defined are so to say names for the elements in M. To construct a geometric morphism ϕ: Sh(X) → B(T) we have to give an interpretation Φ of the language in Sh(X):P The underlying object Φ is the P p set p∈X M with canonical projection π: p∈X Mp → X. We generate a topology on Φ by π −1 (U ) is open for U ⊂ X open, Vk = {(p, αp (k)) | αp (k) defined} is open. Lemma 3.2 Φ is a sheaf over X (π is a local homeomorphism, or an e´ tale map). Proof. π is continuous by definition and maps Vk bijectively onto Uk,k . S Moreover Φ = k∈κ Vk . To prove that π is e´ tale it is hence enough to show that the inverse of π restricted to Vk , which is the map (−, α(−) (k)): Uk,k → Vk , is continuous. By definition of the topology of Φ a typical open subset W of Vk is locally of the form T W = Vk ∩ π −1 (U ) ∩ i=1,...,n Vki = {(p, a) | p ∈ U, a ∈ Mp and a = αp (k) = αp (k1 ) = · · · = αp (kn )} for some ki ∈ κ, U ⊂ X open. It follows that [(−, α(−) (k))]−1 (W ) = U ∩

\

Uk,ki

i=1,...,n

and (−, α(−) (k)) is continuous, so π is a local homeomorphism.

2

In what follows, a product symbol between sheaves always means a product of sheaves, which is computed fibrewise:  [  Mp × · · · × Mp Φ = Φ × ··· × Φ = p∈X

with the appropriate topology. (As well, we usually identify a sheaf with its total space.) From this remark we see at once that for every function symbol f in p S there is a canonical map f (Φ) : Φ → Φ, namely the sum of all the f (M ) P p (i.e., f (Φ) = p∈X f (M ) ). The same applies to relation symbols R in S: There is a canonical subset R(Φ) ⊂ Φ, namely the sum (or disjoint union) p of all the R(M ) .

A topological completeness theorem

87

Lemma 3.3 (i) Every f (Φ) is a local homeomorphism. (ii) Every R(Φ) is a subsheaf of Φ. Proof. We leave the details to the reader and prove only the simplest case, (Φ) that of a unary relation symbol R. In that case h we have to showi that R is S open in Φ. This follows since R(Φ) = k∈κ π −1 (Uk,R ) ∩ Vk . 2 The two lemmas above prove that Φ is indeed an interpretation of the language in Sh(X). Each point p ∈ X defines a geometric morphism p: Sets → Sh(X) with inverse image the usual stalk map. In particular, p∗ carries the interpretation Φ to an interpretation p∗ Φ, which is isomorphic to Mp . Since Sh(X) has enough points we get for geometric formulas ψ1 (y) and ψ2 (y) that Φ |= ∀y(ψ1 (y) → ψ2 (y)) iff {y | ψ1 (y)}(Φ) ,→ {y | ψ2 (y)}(Φ) iff p∗ {y | ψ1 (y)}(Φ) ,→ p∗ {y | ψ2 (y)}(Φ) for all p ∈ X ∗ ∗ iff {y | ψ1 (y)}(p Φ) ,→ {y | ψ2 (y)}(p Φ) for all p ∈ X ∗ iff p Φ |= ∀y(ψ1 (y) → ψ2 (y)) for all p ∈ X p iff M |= ∀y(ψ1 (y) → ψ2 (y)) for all p ∈ X. iff T ` ∀y(ψ1 (y) → ψ2 (y)) Thus, Φ is a conservative model of the theory T and corresponds to a surjective geometric morphism ϕ: Sh(X) → B(T). For the record we state Proposition 3.4 Φ is a conservative model of T.

2

Remark 3.5 (Notational conventions.) In the sequel we will avoid superscripts as often as possible. But sometimes they are necessary or useful. For example, writing p = (Mp , αp ) allows to define the sections (−, α(−) (k)): Uk,k → Vk , which we henceforth write as α(−) (k): Uk,k → Vk to simplify notation. Elements in the stalk Φp are tuples ((p, a1 ), . . . , (p, an )) for ai ∈ Φp . Of course, we will write (p, a) for such a tuple. Remark 3.6 There are several variations of the construction described in this section, which will yield the same theorem. It is possible to start with an arbitrary family Pts(T) of models of T such that for geometric formulas ψ1 (y) and ψ2 (y) we have T ` ∀y(ψ1 (y) → ψ2 (y)) iff M |= ∀y(ψ1 (y) → ψ2 (y)) for all M ∈ Pts(T).

88

C. Butz

(We say that Pts(T) is a family of jointly conservative models.) Then κ has to be chosen such that the cardinality of all models in Pts(T) is less or equal to κ. For example, the finite linear orders {0, . . . , n} for n ∈ N are a family of jointly conservative models for the theory of non–empty linear orders. In this case, κ can be chosen as ℵ0 . Instead of κ–to–one enumerations one can use (partial) enumerations of models α: K → M, K ⊂ κ, such that for each a ∈ M the set α−1 (a) is infinite. 4 Definable open sets Let ψ(y) be a geometric formula with free variables exactly the listed tuple y. We define for a tuple k the open set Uk,ψ(y) = Uψ(k) of X by induction: U⊥ = ∅

U> = X

Uk=l = ∩i=0,...,n Uki ,li Uf (k)=l = Uk,l,f

UR(k) = Uk,R S UW ψi (k) = I Uψi (k)

U(ψ1 ∧ψ2 )(k) = Uψ1 (k) ∩ Uψ2 (k) I W U∃yψ(y,k) = l∈κ Uψ(l,k) W In the definition of the cases ∧ and we mean on the right side the tuples k restricted to the free variables actually occurring in ψ1 , ψ2 and in the ψi . Lemma 4.1 If ψ(y) is a geometric formula and k a tuple of elements of κ then Uψ(k) = {(M, α) | M |= ψ(k)}. 2 As above the notation implies that α(ki ) is defined. The collection of all open sets Uψ(k) forms obviously a base for the topology on X. In general it is not possible to assign to an arbitrary open set U of X a geometric formula ∆(w) and a tuple k so that U = U∆(k) . This is only true for basic open sets. But we can do slightly better. Lemma 4.2 (i) Let U ⊂ X be a nonempty basic open set. There exists a geometric formula ∆(w) and a tuple k such that: — U = U∆(k) . — For every N ∈ Ptsκ (T) and for every tuple b ∈ N such that N |= ∆(b) there exists a κ–to–one enumeration β of N so that β(k) = b and hence (N, β) ∈ U∆(k) . (ii) Let U ⊂ Un,n be an open set and p a point in U . There exists a geometric formula ∆(w, y) and a tuple k such that:

A topological completeness theorem

89

— p ∈ U∆(k,n) ⊂ U . — For every N ∈ Ptsκ (T) and for all tuples b ∈ N , c ∈ N such that N |= ∆(b, c) there exists a κ–to–one enumeration β of N so that β(k) = b, β(n) = c and hence (N, β) ∈ U∆(k,n) . Proof. Ad (i). Let ∆0 (w) be a geometric formula and k a tuple such that U = U∆0 (k) . The formula ∆(w) ≡ ∆0 (w) ∧

^

wi = wj

ki =kj

and the tuple k will do the job. Obviously U = U∆0 (k) = U∆(k) . To prove the second part take an arbitrary model N ∈ Ptsκ (T) and a tuple b ∈ N such that N |= ∆(b). Take an arbitrary κ–to–one enumeration β 00 of N and take out of the domain of β 00 the finite set k to get the κ–to–one enumeration β 0 . To get β extend β 0 to the set k by β(k) = b. The fact that N |= ∆(b) ensures that this is well–defined (compare the construction of ∆). Moreover (N, β) ∈ U∆(k) . Ad (ii). Let U 0 be a basic open set such that p ∈ U 0 ⊂ U . Choose a formula ∆0 (w) and a tuple k according to (i). The geometric formula ^ ∆(w, y) ≡ ∆0 (w) ∧ wi = yj ki =nj ki ∈k, nj ∈n

will do the job.

2

Next we state several lemmas which summarize the information we get from a section α(−) (n). To state the lemmas we first need a definition: Definition 4.3 We say that a formula ψ(y) is GT if it is built V up by formulas ψ1 (y) → ψ2 (y) for ψ1 , ψ2 geometric, arbitrary meets , and universal quantification ∀. The abbreviation GT is used to remind the reader that this class of formulas “is” the class of geometric theories, any theory put together into one axiom. The following two lemmas are proved by induction on ψ: Lemma 4.4 Let γ(y) be a geometric formula and ψ(y) a GT–formula. Then {y | γ(y)}(U) ,→ {y | ψ(y)}(U) if and only if for all M ∈ Ptsκ (T): M |= γ(y) → ψ(y).

2

90

C. Butz

Lemma 4.5 Let s: U → Φ be a section (a continuous map such that s(p) ∈ Mp for each p ∈ U ). Let ψ(y) be a GT–formula with associated subsheaf {y | ψ(y)}(Φ) ⊂ Φ. Then im(s) ⊂ {y | ψ(y)}(Φ) if and only if for all points p in U : Mp |= ψ(s(p)). 2 The next lemma combines Lemma 4.5, which always holds, with the special situation we are dealing with. The lemma is frequently used later. Lemma 4.6 Let U ⊂ Un,n be open sets and ψ(y) a GT–formula. Suppose that the image of α(−) (n)U has nonempty intersection with the sheaf {y | ψ(y)}(Φ) , say for p ∈ U that (p, αp (n)) ∈ {y | ψ(y)}(Φ) . Then there exists a geometric formula ∆(w, y) and a tuple k such that (i)

p ∈ U∆(k,n) ⊂ U .

(ii) α(−) (n)U∆(k,n) maps into {y | ψ(y)}(Φ) . In particular for all p0 ∈ 0

U∆(k,n) the model Mp satisfies ψ(n). (iii) All models N ∈ Ptsκ (T) satisfy N |= ∃w∆(w, y) → ψ(y). (Note that if ψ is geometric this is equivalent to saying that T ` ∃w∆(w, y) → ψ(y).) (iv) For every N ∈ Ptsκ (T) and for tuples b ∈ N , c ∈ N such that N |= ∆(b, c) there exists a κ–to–one enumeration β of N so that β(k) = b, β(n) = c and hence (N, β) ∈ U∆(k,n) .   Proof. If we write U 0 = [α(−) (n)]−1 {y | ψ(y)}(Φ) ∩ U we are in the

situation of Lemma 4.2 and find a formula ∆(w, y) and a tuple k such that (i), (ii) and (iv) hold. To prove (iii) take an arbitrary N ∈ Ptsκ (T) and a tuple c ∈ N such that N |= ∃w∆(w, c). There is thus a tuple b such that N |= ∆(b, c). By (iv) there exists a κ–to–one enumeration β such that β(k) = b,

β(n) = c,

and (hence)

(N, β) ∈ U∆(k,n) .

Since (N, β) ∈ U∆(k,n) we can apply (ii) to get N |= ψ(n), i.e. N |= ψ(c). 2 5 Preservation of universal quantifiers We will show the following proposition: Proposition 5.1 The inverse image ϕ∗ preserves the interpretation of first order formulas: For each first order formula ψ(y) there is an isomorphism {y | ψ(y)}(Φ) ' ϕ∗ {y | ψ(y)}(U) .

A topological completeness theorem

91

The following two corollaries are immediate: Corollary 5.2 The models Φ and U satisfy the same first order formulas: If ψ is any first order formula, U |= ψ if and only if Φ |= ψ. Proof. Take an arbitrary formula ψ. The objects {· | ψ}(Φ) and ϕ∗ {· | ψ}(U) are isomorphic by Proposition 5.1 and the corollary follows since ϕ∗ preserves and reflects isomorphisms. 2 Corollary 5.3 For each first order formula ψ(y) there exists a geometric formula γ(y) such that {y | ψ(y)}(Φ) ' {y | γ(y)}(Φ) . Proof. Given ψ there exists a geometric formula γ such that {y | ψ(y)}(U) ' {y | γ(y)}(U) . Applying ϕ∗ to both sides together with Proposition 5.1 yields the result. 2 We first proof Proposition 5.1 for some special cases: Lemma 5.4 The proposition holds for GT–formulas ψ(y). Proof. It is straightforward to check that for any GT–formula ψ(y) the inequality of subobjects ϕ∗ {y | ψ(y)}(U) ≤ {y | ψ(y)}(Φ) always holds. For the other inequality take (p, a) in {y | ψ(y)}(Φ) for p = (Mp , αp ) in X. Fix a tuple n such that αp (n) = a. Let U be the open set Un,n ∩ [α(−) (n)]−1 ({y | ψ(y)}(Φ) ) which contains p. We apply Lemma 4.6 to find a geometric formula ∆(w, y) and a tuple k such that p ∈ U∆(k,n) and for all M ∈ Ptsκ (T): M |= ∃w∆(w, y) → ψ(y). Since p ∈ U∆(k,n) it follows that (p, a) ∈ {y | ∃w∆(w, y)}(Φ) . Since ψ(y) is GT we can apply Lemma 4.4 and get {y | ∃w∆(w, y)}(U) ,→ {y | ψ(y)}(U) and hence (p, a) ∈ ϕ∗ {y | ψ(y)}(U) . But (p, a) was arbitrary. 2

Proof of Proposition 5.1. TheWproof is by induction on ψ. For atomic formulas this is trivial. The cases ∧, and ∃ follow since the p ∈ X form together a jointly surjective family of geometric morphisms Sets → Sh(X). The details are standard and left to the reader. From the remaining three cases →, V and ∀ we treat one in detail: Let ψ1 (y) and ψ2 (y) be first order formulas and assume {y | ψi (y)}(Φ) ' ϕ∗ {y | ψi (y)}(U)

for i = 1, 2.

(1)

Since {y | ψi (y)}(U) ,→ U is geometrically definable there exist geometric formulas γi (y) so that {y | ψi (y)}(U) ' {y | γi (y)}(U) .

(2)

92

C. Butz

Now {y | ψ1 (y) → ψ2 (y)}(Φ) ' {y | ψ1 (y)}(Φ) → {y | ψ2 (y)}(Φ) (by definition) ' ϕ∗ {y | ψ1 (y)}(U) → ϕ∗ {y | ψ2 (y)}(U) (by (1)) ' ϕ∗ {y | γ1 (y)}(U) → ϕ∗ {y | γ2 (y)}(U) (by (2)) ' {y | γ1 (y)}(Φ) → {y | γ2 (y)}(Φ) (the γi are geometric) ' {y | γ1 (y) → γ2 (y)}(Φ) (by definition) ' ϕ∗ {y | γ1 (y) → γ2 (y)}(U) (by Lemma 5.4) ' ... ' ϕ∗ {y | ψ1 (y) → ψ2 (y)}(U) The other two cases are similar using the same trick.

2

6 Functional completeness In this section we present a result about functional completeness which we state as follows: Proposition 6.1 (Functional completeness) Let ψ(y) and ρ(z) be geometric formulas and g: {y | ψ(y)}(Φ) → {z | ρ(z)}(Φ) a map of sheaves. Then g is definable: There exists a geometric formula γ(y, z) such that graph(g) ' {(y, z) | γ(y, z)}(Φ) . p Equivalently, for arbitrary p, for all tuples b ∈ {y | ψ(y)}(M ) and p c ∈ {z | ρ(z)}(M ) g(b) = c

iff

Mp |= γ(b, c).

Note that by Corollary 5.3 the first part of the proposition extends automatically to the case where ψ and ρ are first order formulas. Of course we could assume that ρ(z) ≡ z = z. The proof of Proposition 6.1 needs some preliminary remarks. We leave most of their proofs to the reader. Fix a model M in Ptsκ (T). Thus M

A topological completeness theorem

93

corresponds to a geometric morphism (again denoted by M, since there is no confusion here) M: Sets → B(T). Let E(M) be the topological space with elements κ–to–one enumerations of M, i.e., maps α: κ ; M. The topology on E(M) is generated by the open sets Wk,a = {α | α(k) = a} for k ∈ κ, a ∈ M arbitrary. For tuples k and a we use as well Wk7→a for the open set ∩i=1,...,n Wki ,ai . There is a canonical map i = iM : E(M) → X sending α to (M, α). We will often identify E(M) along i with a subset of X. Lemma 6.2 (i) The map iM is continuous. (ii) The space E(M) and each basic open set Wk7→a are connected. Proof. As an example we show the second part. Suppose E(M) = U1 ∪ U2 for U1 , U2 nonempty, say for example αi : Ki → M in Ui . Each αi is in some basic open set Wi ⊂ Ui and there are only finitely many elements of κ occurring in the definition of W1 (and of W2 ). We first consider β defined by  α1 (k), if k occurs in the list defining W1 , β(k) = α2 (k), otherwise. β is obtained from α2 by changing the enumeration α2 in a finite number of places. β is clearly κ–to–one and β ∈ W1 . After renaming we may thus assume that α1 and α2 differ only in a finite number of places. Next consider the map γ: k 7→ α1 (k) iff

α1 (k) = α2 (k).

By construction, γ is κ–to–one. But γ has the additional property that γ ∈ W open implies α1 ∈ W and α2 ∈ W . Thus either α2 ∈ U1 or α1 ∈ U2 , i.e., either α1 or α2 is contained in U1 ∩ U2 and E(M) is connected. The same argument applies locally, that is, if we prescribe the enumerations α1 and α2 in a finite number of places (they are then prescribed at the same elements k ∈ κ). Hence E(M) is as well locally connected. 2 The map i induces a geometric morphism i: Sh(E(M)) → Sh(X) with inverse image the pullback functor: /E

i∗ (E) = i−1 (E) 

E(M)

i

 /X

94

C. Butz

Applying the functor i∗ to Φ we get the T–model i∗ Φ. There is another way to get a model of T: The projection π = πM : E(M) → 1 induces the geometric morphism Sh(E(M)) → Sets = Sh(1) with inverse image the constant sheaf over E(M) π ∗ (S) = E(M) × S → E(M), where S in Sets is viewed as a space with discrete topology. Applied to the model M we get the model π ∗ M. Lemma 6.3 The models i∗ Φ and π ∗ M are isomorphic. Equivalently, the following diagram of toposes commutes (up to isomorphism): Sh(E(M)) π

i

ϕ





Sets

/ Sh(X)

M

/ B(T)

Proof. Among other things one has to show that the canonical isomorphism of sets in the diagram below is in fact a homeomorphism: ' /P /Φ M × E(M) Mo (M,α) M 



1o

E(M)

π

π





E(M)

i

/X

2

The details are straightforward.

The following two lemmas are the ingredients in the proof of Proposition 6.1: Lemma 6.4 Let ψ(y) and ρ(z) be two geometric formulas and g: {y | ψ(y)}(Φ) → {z | ρ(z)}(Φ) a map of sheaves. Then the stalk maps gp : ({y | ψ(y)}(Φ) )p → ({z | ρ(z)}(Φ) )p depend only on the underlying model Mp , and not on the enumeration αp . Being more precise the lemma states that for such a map g, for a model M and two enumerations α1 and α2 of M which give rise to the points p1 = (M, α1 ) and p2 = (M, α2 ) of X, the following diagram in Sets commutes: gp1 :({y | ψ(y)}(Φ) )p1 '



gp2 :({y | ψ(y)}(Φ) )p2

/ ({z | ρ(z)}(Φ) ) p1 

'

/ ({z | ρ(z)}(Φ) ) p2

A topological completeness theorem

95

Proof. Fix M and consider i∗ g: i∗ {y | ψ(y)}(Φ) → i∗ {z | ρ(z)}(Φ) . Since we have a canonical isomorphism {y | ψ(y)}(Φ) ' ϕ∗ {y | ψ(y)}(U) and since i∗ ϕ∗ ' π ∗ M ∗ the map i∗ g can be written up to isomorphism as i∗ g: E(M)×{y | ψ(y)}(M) → E(M)×{z | ρ(z)}(M) (where it is important to note that this is a map of sheaves, i.e., i∗ g is compatible with the projections to E(M)). But E(M) is connected, so i∗ g is of the form id × gM for a unique map gM : {y | ψ(y)}(M) → {z | ρ(z)}(M) . 2 Lemma 6.5 Let V be a subsheaf of the definable sheaf Φ = {y | y = y}(Φ) . If the stalks of V depend only on the different models M and not on the enumeration of M (i.e., for two enumerations α1 and α2 of M and the two points p1 = (M, α1 ) and p2 = (M, α2 ) of X the stalks Vp1 and Vp2 are canonically isomorphic), then V is definable: There exists a geometric formula γ(y) such that V ' {y | γ(y)}(Φ) . Another formulation of the assumption of this lemma is that if a ∈ M and (p1 , a) ∈ V then (p2 , a) ∈ V . Proof. Let (p, a) ∈ Vp be arbitrary. Fix a tuple n such that αp (n) = a and consider the open set [α(−) (n)]−1 (V ) ⊂ X. By Lemma 4.6 there exists a geometric formula ∆(w, y) and a tuple k such that (i) p ∈ U∆(k,n) ⊂ [α(−) (n)]−1 (V ). (ii) For every N ∈ Ptsκ (T) and for all tuples b ∈ N , c ∈ N such that N |= ∆(b, c) there exists a κ–to–one enumeration β of N so that β(k) = b, β(n) = c and hence (N, β) ∈ U∆(k,n) . We claim that (p, a) ∈ {y | ∃w∆(w, y)}(Φ) ⊂ V which will prove the lemma: (p, a) was arbitrary and V is the union of definable sheaves, hence definable. To prove the claim note that by (i) the tuple (p, a) is in {y | ∃w∆ (w, y)}(Φ) . To show the inclusion take (q, c) ∈ {y | ∃w∆(w, y)}(Φ) arbitrary for q = (N, β). Fix b such that N |= ∆(b, c). By (ii) there exists a κ–to–one enumeration β 0 of N such that β 0 (n) = c and β 0 (k) = b. The 0 point q 0 = (N, β 0 ) is in U∆(k,n) , thus (by (i)) (q 0 , c) = (q 0 , αq (n)) is in V , 2 as is (q, c) by the assumption on V . Proof of Proposition 6.1: Consider g: {y | ψ(y)}(Φ) → {z | ρ(z)}(Φ) . By Lemma 6.4 the stalk maps gp of g depend only on the underlying model Mp , and not on the enumeration αp . Equivalently, graph(g) as a subobject of Φ × Φ satisfies the assumption of Lemma 6.5 and is definable. 2

96

C. Butz

7 Preservation of function types In this section we prove that the geometric morphism ϕ: Sh(X) → B(T) ∗ preserves exponentials, i.e. ϕ∗ (RP ) ' ϕ∗ Rϕ P for P, R ∈ B(T), at least if P and R are representable sheaves. To simplify notation we use the internal Hom (Hom(−, −)) to denote both the exponential in B(T) and in Sh(X). Proposition 7.1 The model Φ preserves function types: For any two first order formulas ψ(y) and ρ(z) there is an isomorphism ϕ∗ Hom({y | ψ(y)}(U) , {z | ρ(z)}(U) ) ' Hom(ϕ∗ {y | ψ(y)}(U) , ϕ∗ {z | ρ(z)}(U) ). Since every object of the form {z | ρ(z)}(U) is geometrically definable we can assume that ρ and ψ are in fact geometric formulas. There is a canonical map ϕ∗ Hom({y | ψ(y)}(U) , {z | ρ(z)}(U) ) → Hom({y | ψ(y)}(Φ) ,){z | ρ(z)}(Φ), (3) which is the transposed of the evaluation map. It is a formal consequence of Corollary 5.2 and Proposition 2.3 that this map is mono (see [9]). To show that it is epi (locally surjective) we have to describe this map explicitly. In what follows we identify sheaves E over X with their section functors Γ (E, −): OX op → Sets. Following [17], p. 70, the right side of (3) is described by Γ (Hom({y | ψ(y)}(Φ) , {z | ρ(z)}(Φ) ), U ) n o = f : {y | ψ(y)}(Φ) U → {z | ρ(z)}(Φ) U f continuous, πρ ◦ f = πψ for U ⊂ X open. Here πρ is the canonical e´ tale map {z | ρ(z)}(Φ) → X and similar for πψ . For V ⊂ U there are canonical restriction maps. To describe the left side of (3) we have to go through Chapter VII of [14]. We first define a presheaf ϕ˜ Hom({y | ψ(y)}(U) , {z | ρ(z)}(U) ) on OX by ϕ˜ Hom({y | ψ(y)}(U) , {z | ρ(z)}(U) )(U ) n = (τ, s) [∆(w)] an object in Syn(T), τ : {w | ∆(w)}(U) × {y | ψ(y)}(U) → {z | ρ(z)}(U) , o /≡ . s: U → {w | ∆(w)}(Φ)

A topological completeness theorem

97

The equivalence relation ≡ is generated by (τ ◦ (σ (U) × id), s0 ) ≡ (τ, σ (Φ) ◦ s0 ) for [σ]: [∆(w0 )] → [∆(w)] an arrow in Syn(T), τ : {w | ∆(w)}(U) × {y | ψ(y)}(U) → {z | ρ(z)}(U) a map in B(T), and a section s0 : U → {w0 | ∆0 (w0 )}(Φ) . For V ⊂ U there are canonical restriction maps. The sheaf ϕ∗ Hom({y | ψ(y)}(U) , {z | ρ(z)}(U) ) is the associated sheaf of the presheaf just defined. There is a canonical comparison map com of presheaves | ψ(y)}(U) , {z | ρ(z)}(U) ) ϕHom({y ˜ → Hom({y | ψ(y)}(Φ) , {z | ρ(z)}(Φ) ),

(4)

which sends the equivalence class [τ, s] to the map {y | ψ(y)}(Φ) U → {z | ρ(z)}(Φ) U (p, a) ∈ {y | ψ(y)}(Φ) for p ∈ U 7→ τ (Φ) (s(p), (p, a)). The sheafification of the map com is the map of (3). By [14], Corollary III.7.6, the map of (3) is locally surjective if and only if the comparison map com is locally surjective. This we will deduce from the following lemma: Lemma 7.2 Let U be a basic open set of X and P, R representable sheaves in B(T). There exists a geometric formula ∆(w) and a tuple k such that U = U∆(k) and each map f : (ϕ∗ P )U → (ϕ∗ R)U can be lifted to a continuous map of sheaves fˆ: {w | ∆(w)}(Φ) × ϕ∗ P → ϕ∗ R so that for all p ∈ U : fˆp (αp (k), −) = fp as maps (ϕ∗ P )p → (ϕ∗ R)p . Proof. Let ∆(w) and k as in Lemma 4.2 and fix a map f : ϕ∗ P U → ϕ∗ RU . To show the existence of fˆ note that such a map is uniquely determined by maps fˆ(M) : {w | ∆(w)}(M) × M ∗ P → M ∗ R

for M ∈ Ptsκ (T)

(this is Lemma 6.4). We use this to define fˆ as follows: fix a tuple b ∈ {w | ∆(w)}(M) . By Lemma 4.2 there exists a κ–to–one enumeration α of M such that α(k) = b and p = (M, α) ∈ U∆(k) = U . Now M ∗ P ' fp

p∗ ϕ∗ P → p∗ ϕ∗ R ' M ∗ R gives a map M ∗ P → M ∗ R and we do this for each tuple b ∈ {w | ∆(w)}(M) to get fˆ(M) . This construction is independent of the chosen α: If α1 and α2 are two enumerations which map k to b then α1 , α2 ∈ Wk7→b ⊂ i∗ (U∆(k) ) = E(M) ∩ U∆(k) .

98

C. Butz

But Wk7→b is connected, and i∗ f restricted to this set comes from a unique map M ∗ P → M ∗ R, viz. i∗ (ϕ∗ P U )Wk7→b '



i∗ f Wk7→b

/ i∗ (ϕ∗ RU )W k7→b 

id×fˆ(M)

'

Wk7→b × M ∗ P _ _ _ _ _ _ _/ Wk7→b × M ∗ R . It remains to show that the fˆ(M) glue together to a continuous map. Thus to complete the proof of this lemma we have to show that for any section t: O → {w | ∆(w)}(Φ) × ϕ∗ P the composition fˆ ◦ t is continuous. To this end fix t, which comes from two sections t∆ : O → {w | ∆(w)}(Φ)

and

t0 : O → ϕ∗ P.

Take q ∈ O arbitrary. Locally (say on V 3 q) we can assume that t∆ is the section α(−) (l) for a tuple l 6= k. Consider the bijection of κ   l 7→ k ι: k 7→ l  id elsewhere. ι induces a homeomorphism of X and maps U∆(l) to U∆(k) . The point q

is mapped to p = ι(q) in U∆(k) . Moreover, t∆ ◦ ι = α(−) (k) on ι(V ). To show that fˆ ◦ t is continuous around q ∈ V ⊂ O it is enough to show that fˆ ◦ t ◦ ι is continuous around p = ι(q) ∈ ι(V ) ⊂ U∆(k) . But on this set (fˆ ◦ t ◦ ι)(p0 ) = fˆ(t∆ ◦ ι(p0 ), t0 ◦ ι(p0 )) 0 = fˆ(αp (k), t0 ◦ ι(p0 ))

= fp0 (t0 ◦ ι(p0 ))

(by construction)

= f (t0 ◦ ι(p0 )) = f ◦ t0 ◦ ι(p0 ), which is continuous.

2

Proof of Proposition 7.1. To complete the proof of the proposition we have to show that the comparison map com of (4) is locally surjective. Start with a continuous map f : {y | ψ(y)}(Φ) U → {z | ρ(z)}(Φ) U for some open set U . Locally we can assume that U is a basic open set. By Lemma 7.2 we find a geometric formula ∆(w), a tuple k, and a lifting fˆ: {w | ∆(w)}(Φ) × {y | ψ(y)}(Φ) → {z | ρ(z)}(Φ)

A topological completeness theorem

99

such that for all p in U = U∆(k) fˆp (αp (k), −) = fp (−). By Proposition 6.1 the map fˆ is definable, say fˆ = τ (Φ) for an arrow τ in 2 Syn(T). Obviously, [τ (U) , α(−) (k)] is a pre–image of f . 8 Appendix: motivation of the presented construction In this section we relate out theorem to previous work, mainly of A. Joyal. We assume that the reader is familiar with topos theory and do not explain standard terminology, but refer to [8] and [14]. A covering theorem like the one proved in this paper measures how different a topos E can be from the category of sheaves over a topological space: what kind of properties of E can be preserved along an embedding ϕ∗ : E ,→ Sh(X) (that is the inverse image of a geometric morphism). Since a necessary assumption on E is to have enough points one has to relax the situation in general and one looks for surjective geometric morphisms ψ: Sh(L) → E where L is a locale, as opposed to a topological space. The techniques used to construct such covers are all variations of one theme, namely enumerating a suitable object of E. Here one uses that a topos E is a universe of set-theory, and that one can think of Sh(L) as being obtained from E by a forcing construction. The object S of E to be enumerated has to be such that the subobjects of finite products of S generate E. Equivalently, the classifying morphism of S (from E to the object classifier) has to be localic. In all the examples below, enumerating such an object will ensure that the topos containing the generic enumeration is localic over Sets, i.e., of the form Sh(L) for some locale L. In [11], Joyal and Tierney forced the existence of a generic surjective function N  S to get an open surjection E[N  S] → E. (Here E[N  S] is the topos containing the generic enumeration.) Later Joyal improved this result: If one forces the existence of a generic partially defined surjective function with infinite fibres, i.e., a map β

N  dom(β) → S β

such that β −1 (s) is infinite for all s ∈ S, then E[N  dom(β) → S] → E is connected and locally connected over E. A proof can be found in [10]. As before, we write β: N ; S for such a map.

100

C. Butz

If E has enough points one wants to replace the localic topos E[β: N ; S] by a topos of sheaves over some topological space X. A natural choice for X is pts L, the topological space of points of the locale L that represents E[β: N ; S], that is, Sh(L) ∼ = E[β: N ; S]. There arise mainly two difficulties: (i) The locale L (or the topos E[β: N ; S]) may have no points at all, or at least, not enough points so that the composite i ψ Sh(pts L) ,→ Sh(L) ∼ = E[β: N ; S] → E

is surjective. (ii) Even if the composite ψ ◦ i is a surjection, it is not true that properties of ψ like openness, connectedness, or local connectedness carry over immediately to ψ ◦ i. This always requires a new proof . The first difficulty can be overcome by replacing the natural numbers by a large set, for example a large cardinal κ. One can show that for any cardinal κ the topos E[β: κ ; S] is connected and locally connected over E. Here the requirement on β is that the fibres are cofinal in κ (as in this paper or in [3]), or just infinite as in [6, 5]. If E has enough points one can always choose κ big enough so that the composite Sh(pts L) ,→ Sh(L) ∼ = E[β: κ ; S] → E is surjective. Our paper starts with a topos E with enough points. We assume that E is given as the classifying topos of a possibly infinite geometric theory T, so that E ∼ = B(T) with universal model U. The underlying support of the model U, i.e., the object U in the topos B(T) is the object we enumerate. After choosing an appropriate cardinal κ we construct the topos B(T)[β: κ ; U] and look at the topological space X such that X is the space of points of the locale representing B(T)[β: κ ; U]. This is the space described in Section 3. The model Φ described there is the model corresponding to the canonical geometric morphism Sh(X) → B(T). As noted above, it requires a proof that the geometric morphism Sh(X) → B(T) shares many of the good properties of the morphism B(T)[β: κ ; U] → B(T), and this was the topic of our paper.

A topological completeness theorem

101

References ´ 1. M. Artin, A. Grothendieck, and J.-L. Verdier. Th´eorie des Topos et Cohomologie Etale des Sch´emas, (SGA4), Lecture Notes in Mathematics 269, 270. Springer–Verlag, Berlin, 1972. 2. S. Awodey and C. Butz. Topological completeness for higher-order logic. Preprint, June 1997. Submitted. 3. C. Butz. Logical and cohomological aspects of the space of points of a topos. Ph.D. thesis, Utrecht, 1996. 4. C. Butz and P. T. Johnstone. Classifying toposes for first order theories. Ann. Pure Appl. Logic 91: 33–58, 1998. 5. C. Butz and I. Moerdijk. Topological representation of sheaf cohomology of sites. Preprint, 1996. To appear in Compositio Mathematica. 6. C. Butz and I. Moerdijk. Representing topoi by topological groupoids. J. Pure Appl. Algebra 130: 223–235, 1998. 7. M. P. Fourman and D. S. Scott. Sheaves and logic. In: Applications of Sheaves, M. P. Fourman, C. J. Mulvey, and D. S. Scott (editors), Lecture Notes in Mathematics 753, pages 302–401, New York, 1979. Springer–Verlag. 8. P. T. Johnstone. Topos Theory. Academic Press, New York, 1977. 9. P. T. Johnstone. Open maps of toposes. Manuscripta Mathematica, 31:217–247, 1980. 10. P. T. Johnstone. How general is a generalized space? In: Aspects of Topology, I. M. James and E. H. Kronheimer (editors), London Math. Soc. Lecture Notes 93, pages 77–111, Cambridge, 1985. Cambridge University Press. 11. A. Joyal and M. Tierney. An extension of the Galois theory of Grothendieck. Mem. Amer. Math. Soc. 51:1984, no. 309. 12. H. J. Keisler. Model Theory for Infinitary Logic. Studies in Logic and the Foundations of Mathematics, Vol. 62. North–Holland Publishing Co., Amsterdam-London, 1971. 13. A. Kock. Synthetic Differential Geometry. London Math. Soc. Lecture Notes 51. Cambridge University Press, Cambridge, 1981. 14. S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. Springer–Verlag, New York, 1992. 15. M. Makkai and G. E. Reyes. First Order Categorical Logic, Lecture Notes in Mathematics 611. Springer–Verlag, Berlin, 1977. 16. I. Moerdijk and G. E. Reyes. Models for Smooth Infinitesimal Analysis. Springer– Verlag, New York, 1991. 17. B. R. Tennison. Sheaf Theory. London Math. Soc. Lecture Notes 20. Cambridge University Press, Cambridge, 1975.