BRICS RS-97-20 Butz & Johnstone: Classifying Toposes for First Order Theories BRICS

Basic Research in Computer Science

Classifying Toposes for First Order Theories

Carsten Butz Peter T. Johnstone BRICS Report Series RS-97-20 ISSN 0909-0878 July 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/20/

Classifying Toposes for First Order Theories

Carsten Butz^{∗} and Peter Johnstone^{†}

7 July 1997

Abstract

By a classifying topos for a first-order theory 𝕋, we mean a topos E such that, for any topos F, models of 𝕋 in F correspond exactly to open geometric morphisms F → E. We show that not every (infinitary) first-order theory has a classifying topos in this sense, but we characterize those which do by an appropriate ‘smallness condition’, and we show that every Grothendieck topos arises as the classifying topos of such a theory. We also show that every first-order theory has a conservative extension to one which possesses a classifying topos, and we obtain a Heyting-valued completeness theorem for infinitary first-order logic.

0 Introduction

It is by now well known that Grothendieck toposes are ‘the same thing as’ Morita-equivalence classes of geometric theories, in the following sense: for every geometric theory 𝕋, there exists a topos B(𝕋) (called the classifying topos of 𝕋) containing a model G_{𝕋} of 𝕋 which is generic in the sense that, for any Grothendieck topos F, the functor

∗Current address: BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation, Computer Science Department, Aarhus University, Ny Munkegade, DK–8000 Århus C, Denmark. butz@brics.dk

†Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, 16 Mill Lane, Cambridge CB2 1SB, U.K. ptj@pmms.cam.ac.uk

Top (F, B(𝕋)) \overline{}𝕋-Mod(F) ,

which sends a geometric morphism f: F → B(𝕋) to the 𝕋-model f^{∗}(G_{𝕋}), is an equivalence of categories. Conversely, for every Grothendieck topos E, there exists a geometric theory 𝕋 such that E ≃ B(𝕋). This theory is not uniquely determined by E, in that one can have many different presentations of ‘the same’ theory; but if we regard two theories as (Morita- )equivalent whenever they have equivalent categories of models in an arbitrary topos, then the correspondence between (categorical) equivalence classes of Grothendieck toposes and Morita-equivalence classes of geometric theories becomes one-to-one.

However, although a very large proportion of the first-order theories encountered in mathematical practice are (at least Morita-equivalent to) geometric ones, we do occasionally need to consider models of theories which are not geometric. (For example, as was first observed by Kock [14], it can often be profitable to consider the non-geometric first-order sentences satisfied by the generic model of a geometric theory.) For such theories, we cannot hope to have a classifying topos in the above sense, since it is well-known that geometric theories are exactly those whose models are preserved by inverse image functors. Nevertheless, we do know several characterizations of those geometric morphisms whose inverse image functors preserve arbitrary (infinitary) first-order logic: they are exactly the open geometric morphisms in the sense of [9] or [12]. So we might hope that, for at least some first-order theories 𝕋 of interest, we could find a topos B^{fo}(𝕋) and a natural equivalence

Open (F, B^{fo}(𝕋)) ≃ 𝕋-Mod(F) ,

where the left-hand side denotes the full subcategory of Top (F, B^{fo}(𝕋)) whose objects are open geometric morphisms. (Since every geometric theory may also be considered as a first-order theory, we shall henceforth write B^{g}(𝕋) for the classifying topos of such a theory as defined in the first paragraph, in order to distinguish it from the concept just introduced.)

Sadly, it is not possible to construct such a topos for an arbitrary firstorder theory 𝕋. The problem is, in a sense, that open geometric morphisms are ‘too well-behaved’: their inverse image functors preserve the interpretations, not only of finitary first-order formulae, but of arbitrary (L_{∞ω}) infinitary ones as well. And there are simply too many of the latter, even if we restrict ourselves to propositional logic. It is well known ([6], [7], [20]) that the free complete Boolean algebra on a countable infinity of generators is a proper class; perhaps less familiar is the fact [11] that the corresponding problem for complete Heyting algebras occurs already with two generators—that is, there is a proper class of L_{∞ω} formulae in two propositional variables, no two of which are (constructively) provably equivalent. The model-theoretic version of this fact says that, for any cardinal κ, we can build a complete Heyting algebra H_{κ} of cardinality at least κ which is generated by two elements. Now let 𝕋 be the empty theory in a language L with two primitive propositional symbols: we can regard the generators of H_{κ} as a model of 𝕋 in the topos Sh(H_{κ}) of sheaves on H_{κ}. If the classifying topos B^{fo}(𝕋) existed, this model would be classified by an open geometric morphism f: Sh(H_{κ}) → B^{fo}(𝕋); since f^{∗} preserves the interpretations of arbitrary first-order formulae, we see that it must be surjective on subobjects of 1, and hence (since this holds for all κ) that the lattice of subobjects of 1 in B^{fo}(𝕋) must be a proper class—which is impossible.

However, we shall show in this paper that the above ‘cardinality problem’ is the only obstruction to the existence of B^{fo}(𝕋). Specifically, we shall prove that, for an arbitrary 𝕋, there exists a topos B^{fo}(𝕋) with the universal property described above if and only if, for every finite string x⃗ of variables in the language of 𝕋, the complete Heyting algebra of 𝕋-provable-equivalence classes of formulae with free variables in x⃗ is a set. Moreover, for any 𝕋 and any cardinal κ such that 𝕋 may be axiomatized by formulae in L_{κω}, there exists a canonical extension of 𝕋 to a theory \overline{𝕋} with the above smallness property, which is L_{κω}-conservative (i.e. every L_{κω} sentence derivable from \overline{𝕋} is derivable from 𝕋). In particular, the generic \overline{𝕋}-model in B^{fo}(\overline{𝕋}) is an L_{κω}-conservative model of 𝕋. Also, every Grothendieck topos E occurs, up to equivalence, as B^{fo}(𝕋) for some 𝕋; thus we may, once again, identify Grothendieck toposes with Morita-equivalence classes of ‘provably small’ first-order theories.

The main ingredient in the proofs of the above statements is a characterization of the open geometric morphisms into a Grothendieck topos E = Sh(C, J) in terms of the flat and continuous functors on C which induce them. We prove this result in section 1 of the paper. Sections 2 and 3 are devoted to reviewing material from categorical logic, culminating in the ‘Heyting-valued completeness theorem’ for (intuitionistic) infinitary firstorder logic. In section 4, we show how to construct the first-order theory classified by a given topos E; in particular, if E is given as the classifying topos B^{g}(𝕋) of a geometric theory 𝕋, we show that its first-order theory may be taken to consist of all sentences satisfied in the generic model of 𝕋. In section 5 we prove our main theorem characterizing those first-order theories which admit classifying toposes. Finally, section 6 is devoted to the discussion of some examples and applications.

Throughout the paper, for simplicity, we shall work in the 2-category of Grothendieck toposes (that is, toposes defined and bounded over the classical topos of sets Set); the word ‘topos’, unless otherwise stated, will mean ‘Grothendieck topos’. However, those readers who are accustomed to working over a base topos S will have little difficulty in extending our results to the latter more general context (for any topos S with a natural number object); of course, the cardinality bounds which we use have to be replaced by bounds expressed in terms of subobjects of a suitable object of S.

Acknowledgements. The first author would like to thank Ieke Moerdijk and Steve Awodey for many helpful discussions on this topic. The second author would like to make a similar acknowledgement to Martin Hyland. Part of the first author’s research was supported by a scholarship of the University of Utrecht, and was part of a project funded by the Netherlands Organization for Scientific Research NWO.

1 Open maps into sheaf toposes

Let E be the topos of sheaves on a (small) site (C, J). Diaconescu’s theorem [3] asserts that, for any topos F, there is an equivalence between the category Top (F, E) of geometric morphisms from F to E, and the category of flat and continuous functors C → F (see also [15], section VII.7 or [8], proposition 7.13). Our aim in this section is to characterize those functors C → F which correspond to open geometric morphisms, in the sense of [9] or [12].

Although, for most of this paper, our working definition of open maps will be that they are precisely those geometric morphisms f: F → E whose inverse image functors preserve full (infinitary) first-order logic, in the present section it will be convenient to use the characterization of them in terms of the map \overline{τ}: Ω_{E} → f_{∗}Ω_{F} which is the transpose of the characteristic function τ of the monomorphism f^{∗}(⊤_{E}). We recall that f is open iff \overline{τ} has an internal left adjoint λ: f_{∗}Ω_{F} → Ω_{E} (see [9], theorem 3.2 or [12], p. 56).

Now suppose that E = Sh(C, J), and that the geometric morphism f corresponds to a flat continuous functor F: C → F. Let ε: C → E denote the composite of the Yoneda embedding C → [C^{op}, Set] with the associated sheaf functor. Then we may identify Ω_{E} with the sheaf which to an object A of C assigns the set of subobjects of ε(A) in E, or equivalently the set of J-closed sieves on A in C (recall that a sieve S is J-closed if, whenever we have a morphism α: B → A and a J-covering sieve R on B such that αβ ∈ S for all β ∈ R, then α ∈ S). Similarly, we may identify f_{∗}(Ω_{F}) with the sheaf whose value at A is the set of subobjects of f^{∗}ε(A) = F (A). In terms of these identifications, the map \overline{τ} may be identified with the action of f^{∗} on subobjects of ε(A); that is, \overline{τ}_{A}(S ↣ ε(A)) = (f^{∗}S ↣ F (A)). Note also that the action of a morphism α: A → B of C on both Ω_{E} and f_{∗}Ω_{F} is given by pullback of subobjects; since f^{∗} preserves pullbacks, it is clear that the square

Sub(ε(B)) \overline{^{\overline{τ}_{B}} ^{}}Sub(F (B))

[figure: Sub(ε(A)); ε(α)^{∗}; \overline{τ}_{A}; Sub(F (A)); F (α)^{∗}]

commutes.

Lemma 1.1 The geometric morphism f is open if and only if

(i) for each object A in C and each family {S_{i} | i ∈ I} of subobjects of ε(A) we have ⋀_{i∈I} \overline{τ}_{A}(S_{i}) = \overline{τ}_{A}(⋀_{i∈I} S_{i}); and

(ii) for each morphism α: A → B in C and each subobject S of ε(A) we have ∀_{F (α)}\overline{τ}_{A}(S) = \overline{τ}_{B}∀_{ε(α)}(S).

Here, as usual, ∀_{F (α)} and ∀_{ε(α)} denote the right adjoints of F (α)^{∗} and ε(α)^{∗} acting on subobjects. We note that, in both conditions, the equality sign could be replaced by an inclusion (≤) of subobjects, since the reverse inclusion ≥ is automatic for any f.

Proof Since Sub(ε(A)) and Sub(F (A)) are complete lattices, the first condition of the lemma is equivalent to saying that each \overline{τ}_{A} has a left adjoint λ_{A}: Ω_{E}(A) → f_{∗}Ω_{F}(A). Given the existence of these left adjoints, the second condition is equivalent to the commutativity of the diagram of left adjoints

Sub(F (B)) \overline{λ_{B} ^{}}Sub(ε(B))

[figure: Sub(F (A)); F (α)^{∗}; λ_{A}; Sub(ε(A)); ε(α)^{∗}]

for every α: A → B in C, i.e. to saying that the λ_{A} form a morphism of sheaves λ: Ω_{E} → f_{∗}Ω_{F}. So the two conditions together are equivalent to saying that \overline{τ} has an internal left adjoint in E, i.e. that f is open. □

We remark that Lemma 1.1 could also be deduced by combining [16], lemma 6.1.8, with [9], theorem 3.2(v).

Using the description of Ω_{E}(A) as the set of closed sieves on A, we get the following translation of Lemma 1.1, which we state for future reference:

Corollary 1.2 The geometric morphism f is open if and only if

(i) for each object A in C and each family {S_{i} | i ∈ I} of closed sieves on A,

⋀_{i∈I} ⋁{∃_{F (β)}F (B) | β: B → A ∈ S_{i}} = ⋁{∃_{F (β)}F (B) | β: B → A ∈ ⋂_{i∈I} S_{i}} ;

(1)

and

(ii) for each α: A → B in C and each closed sieve S on A,

∀_{F (α)} ⋁{∃_{F (β)}F (C) | β: C → A ∈ S} = ⋁{∃_{F (γ)}F (D) | γ: D → B ∈ ∀_{α}S} . (2)

□ Here ∀_{α}S denotes the closed sieve

{γ: D → B | (∀β: D → A)((αβ = γ) ⇒ (β ∈ S))} .

The map ∀_{α}: Ω_{E}(A) → Ω_{E}(B) is the right adjoint of the action α^{∗} of α on closed sieves.

We conclude this section with some more remarks about preservation of logical connectives. If {u_{i}: E_{i} → E | i ∈ I} is an epimorphic family of maps in E, we have an embedding of complete Heyting algebras

Sub(E)^{_{⊂} u^{∗} ^{}}∏_{i∈I} Sub(E_{i}) .

Applying this to the epimorphic family {e: ε(A) → E | e ∈ E(A), A ∈ ob C} where E is any object of E = Sh(C, J), and to the image of this family under f^{∗} for some geometric morphism f: F → E, we obtain a commutative square of complete Heyting algebras

Sub(E)^{⊂} ∏ Sub(ε(A))

[figure: Sub(f^{∗}E); ⊂; ∏ Sub(F (A))]

(3)

where F: C → F is the flat continuous functor corresponding to f, and the vertical maps are induced by the action of f^{∗} on subobjects.

Lemma 1.3 Let f: F → E = Sh(C, J) be a geometric morphism. The functor f^{∗} preserves meets of families of subobjects of cardinality less than κ (resp. all meets, implication, negation) if and only if it does so on subobjects of representables.

Proof The nontrivial direction follows from the existence of the diagram (3) for each object E in E. □

This allows us to translate properties of f into properties of F and vice versa, for example:

Corollary 1.4 The geometric morphism f is sub-open in the sense of [9] (i.e. f^{∗} preserves implication) if and only if, for each A ∈ ob C and every two closed sieves S_{1}, S_{2} on A, the image of the map

∐_{\{α: B→A | α^{∗}S_{1}=α^{∗}S_{2}\}} F (B) \overline{}F (A)

is the subobject f^{∗}S_{1} ⇔f^{∗}S_{2} of F (A)

Proof Since S_{1} ⇔ S_{2} = {α | α^{∗}S_{1} = α^{∗}S_{2}}, the condition says that f^{∗} preserves ⇔ on the level of the site. But this is equivalent to saying that f^{∗} preserves implication, because in any Heyting algebra (h ⇒ h′) ≡ (h ⇔ (h ∧ h′)). □

2 First-order theories and syntactic categories

In this section we briefly recall the fundamentals of first-order categorical model theory; for more details we refer the reader to [16], [15], chapter X or [5], appendix B.

We shall work over a (possibly) many-sorted signature Σ specified by giving a set of base sorts (denoted A, B, C, …), a set of primitive functionsymbols f, g, h, … and a set of primitive relation-symbols R, S, T, …; the latter will always include an equality predicate =_{A} for each sort A. Each function- or relation-symbol has a specified type which is a finite string of sorts; we write f: A⃗ → B or R ⊆ A⃗ to indicate the type of a primitive symbol. We identify constants of sort A with nullary function-symbols [ ] → A (where [ ] denotes the empty string of sorts), and primitive propositions with nullary relation-symbols R ⊆ [ ]. A Σ-structure M in a category C with (at least) finite products assigns to each sort A an object MA, to each function-symbol f: A⃗ → B a morphism Mf: MA⃗ → MB (where MA⃗ denotes the product MA_{1} × ⋯ × MA_{n}, if A⃗ = (A_{1}, …, A_{n})), and to each relation-symbol R ⊆ A⃗ a subobject MR ↣ MA⃗ (with the proviso that M(=_{A}) is necessarily the diagonal subobject of MA × MA).

Our formal language is the infinitary language L_{κω}(Σ) (which we shall abbreviate to L_{κ} when there is no danger of confusion): that is, we allow the formation of infinite conjunctions ⋀_{i∈I} ϕ_{i} and disjunctions ⋁_{j∈J} ψ_{j} of formulae provided (a) the cardinalities of the index sets I and J are less than κ, and (b) the total number of free variables in any formula remains finite. (Note that we always allow the empty conjunction ⊤ and the empty disjunction ⊥.) Here κ denotes an infinite regular cardinal (as it will throughout this paper); we allow the possibility that κ = ∞, the ‘cardinality of the universe’ (i.e. that we place no restrictions on the size of conjunctions and disjunctions). However, the restriction to finitely many free variables will remain in force throughout. By a context, we mean a finite string x⃗ of distinct variables; we shall write ϕ(x⃗) to indicate that x⃗ is a suitable context for the formula ϕ, i.e. that all the free variables of ϕ appear in it (though it may contain variables which do not appear in ϕ). The type of a context x⃗ is the string A⃗ of (not necessarily distinct!) sorts of the variables in x⃗.

By a first-order theory 𝕋 over Σ, we mean (informally) a set of sentences in L_{∞ω}(Σ); however, we shall identify two theories 𝕋 and 𝕋′ if each member of the first set is deducible from the second, and vice versa. (Here it should be emphasized that our notion of deducibility is relative to an intuitionistic deduction-system such as that in [2]—suitably extended to handle the infinitary connectives, cf. [18] or [13]—since we wish to study models of our theories in categories (such as non-Boolean toposes) where the rules of classical logic are not valid.) One might therefore be tempted to identify each theory with its deductive closure (i.e. the class of all sentences deducible from it); however, it is important for our purposes that the axioms of a theory form a set rather than a proper class. (Note that this implies, in particular, that for each theory 𝕋 we can find a cardinal κ such that 𝕋 is actually contained in L_{κω}(Σ).)

We recall that a formula ϕ is said to be κ-geometric if it can be built up from atomic formulae by means of finite conjunctions, disjunctions of cardinality less than κ, and existential quantifications. (If κ = ∞, we simply say ϕ is geometric; if κ = ω, we say ϕ is coherent. A (κ-)geometric axiom is a sentence of the form (∀x⃗)(ϕ⇒ψ) where ϕ and ψ are (κ-)geometric formulae and x⃗ is a suitable context for them; a (κ-)geometric theory is one specified by a set 𝕋 of (κ-)geometric axioms.

In order to interpret compound formulae in a Σ-structure M, we need to impose further restrictions on the category C in which M lives. We recall that a regular category is one with finite limits and (regular epi/mono) factorizations, the latter being stable under pullback; by a κ-geometric category we mean a regular category having unions for arbitrary families of subobjects of cardinality less than κ, the unions being additionally stable under pullback. (Makkai and Reyes [16] call these κ-logical categories, and (in the case κ = ω) Freyd and Scedrov [5] call them pre-logoi.) By a κ-Heyting category, we mean a regular category C having unions and intersections for families of subobjects of cardinality less than κ, and such that the operation of pulling back subobjects of B along a fixed morphism f: A → B of C has a right adjoint ∀_{f} (it follows that the unions, as well as the intersections, are automatically stable under pullback; it is also easy to show that in such a category we automatically have an implication operation making each subobject lattice into a Heyting algebra, and that implication is also stable under pullback). Again, this concept has been given different names elsewhere in the literature; in particular, Freyd and Scedrov [5] call it a logos in the case κ = ω. It is well known that any (Grothendieck) topos is an ∞-Heyting category.

It is clear that, given a Σ-structure M in a κ-geometric (resp. κ-Heyting) category C, we may proceed to interpret any κ-geometric (resp. arbitrary L_{κ}) formula-in-context ϕ(x⃗) over Σ as a subobject [ϕ(x⃗)]_{M} of MA_{1} × ⋯ × MA_{n}, where A⃗ = (A_{1}, …, A_{n}) is the type of x⃗. Moreover, this interpretation is sound for the logical calculus mentioned above, in the sense that if a sentence σ is deducible from a theory 𝕋, then it is satisfied in all 𝕋-models in appropriate categories. (As usual, we say that σ is satisfied in a structure M if [σ([ ])]_{M} ↣ M[ ] = 1 is an isomorphism, and that M is a 𝕋-model if it satisfies all the sentences in 𝕋. For the geometric case, we need to modify the definition of satisfaction: a geometric axiom σ = (∀x⃗)(ϕ⇒ψ) is satisfied in M if [ϕ(x⃗)]_{M} ≤ [ψ(x⃗)]_{M} in Sub(MA⃗).)

In order to form a category of 𝕋-models in C, where 𝕋 is not necessarily geometric, we need to exercise some care in our choice of morphisms. Clearly, given Σ-structures M and N, we should expect a morphism f: M → N to provide a C-morphism f_{A}: MA → NA for each sort A of Σ. Given this, for each formula-in-context ϕ(x⃗) we shall have a diagram

\begin{matrix}[ϕ(x⃗)]_{M} & & [ϕ(x⃗)]_{N} \\ MA⃗ & [figure] & \overline{fA⃗ ^{}} & NA⃗ & [figure] \end{matrix}  (4)

where fA⃗ is the product of the f_{A_{i}}. The usual definition of a (homo)morphism of Σ-structures is equivalent to saying that we have [ϕ(x⃗)]_{M} ≤ f ∗ ; A⃗[ϕ(x⃗)]_{N} (i.e. that the above diagram can be completed to a commutative square) for all atomic formulae ϕ; an easy induction then shows that the same condition holds for all geometric formulae ϕ, but it is well known that the induction breaks down for formulae involving implication or universal quantification.

A stronger condition, commonly known by the name embedding of Σstructures, is to demand an equality [ϕ(x⃗)]_{M} = f ∗ ; A⃗[ϕ(x⃗)]_{N} for all atomic ϕ, i.e. to demand that the diagram (4) should be completable to a pullback square. Given that our language always includes the predicate =_{A} whose interpretation in any M is the diagonal subobject of MA×MA, this condition clearly forces each f_{A} to be monic. Once again, it is easy to show that this condition is inherited by all quantifier-free formulae ϕ, but it may fail for formulae involving quantifiers.

Classically, a morphism f is called an elementary embedding if the diagram (4) is completable to a pullback square for all L_{ω} formulae-in-context ϕ(x⃗); it seems reasonable to use the term κ-elementary embedding if (4) is a pullback for all L_{κ} formulae-in-context. (We shall give an example below to demonstrate the dependence of this concept on κ.) However, the fourth corner of the parallelogram, namely the condition that (4) should commute for all (L_{κ}) formulae, is not commonly considered by classical model-theorists. Of course, the reason is that, if we restrict our attention to structures in a Boolean topos such as Set, then the commutativity of (4) for the complementary subobjects [ϕ(x⃗)] and [¬ϕ(x⃗)] forces both the squares to be pullbacks; but this is far from being the case in a non-Boolean topos (again, we shall give an example below), and it turns out that this fourth condition is the one of greatest importance for us.

Morphisms satisfying this condition seem to have been first explicitly considered (in the case κ = ω) in [17], where they were called ‘weak elementary embeddings’; but this name seems unsatisfactory since such morphisms do not have to be monic. Accordingly, we introduce the name κ-elementary morphism of Σ-structures for a family of morphisms f_{A} such that we have [ϕ(x⃗)]_{M} ≤ f ∗ ; A⃗[ϕ(x⃗)]_{N} for all L_{κ} formulae-in-context ϕ(x⃗) over Σ. We write Σ-Str(C)_{κ} for the category of all Σ-structures in C and κ-elementary morphisms between them; and, if 𝕋 is a theory in L_{κ}, we write 𝕋-Mod(C)_{κ} for the full subcategory of Σ-Str(C)_{κ} whose objects are 𝕋-models. (Note that the subscripts cannot be omitted even in the case κ = ω; we use the unsubscripted notations for the categories whose morphisms are arbitrary homomorphisms of Σ-structures.)

Example 2.1 Let E be the Sierpiński topos whose objects are diagrams A = (A(0) → A(1)) in Set and whose morphisms are commutative squares. Let Σ be the one-sorted signature whose only primitive symbol is equality (so that Σ-structures are simply objects). Let N be the terminal object of E, and let M be any object such that M(1) is a singleton. An easy induction shows that the interpretation in N of any L_{∞} formula-in-context over Σ is either the whole of N^{n} ≅ 1 or its zero subobject (that is, the intermediate subobject (0 → 1) cannot occur); so, in order to prove that the unique morphism M → N is ∞-elementary, it suffices to show that whenever [ϕ(x⃗)]_{N} = 0 we also have [ϕ(x⃗)]_{M} = 0. But if [ϕ(x⃗)]_{N} = 0, then since the functor ‘evaluate at 1’ is the inverse image of an open geometric morphism Set → E we see that the interpretation of ϕ(x⃗) in the terminal object of Set is also 0, and hence also [ϕ(x⃗)]_{M}(1) = 0. And this forces [ϕ(x⃗)]_{M}(0) = 0; thus we have shown that M → N is an ∞-elementary morphism. But it is clearly not an embedding if M(0) has more than one element.

Example 2.2 To show the dependence of κ-elementarity on the cardinal κ, it suffices to consider models in Set. Let Σ be the single-sorted signature with a countable infinity of constant symbols c_{i} (i ∈ ω); let M be the set of natural numbers with c_{i} interpreted as i for each i, and let N be any uncountable set with each c_{i} interpreted as a different element of N. It is easy to see that the obvious embedding of Σ-structures M → N is ω-elementary, since M and N have isomorphic ultrapowers (indeed, for a suitable choice of its cardinality, N is isomorphic to an ultrapower of M); but it is not ω_{1}-elementary since the L_{ω_{1}} sentence (∀x) ⋁_{i∈ω}(x = c_{i}) is satisfied in M but not in N.

We next recall briefly the construction of the syntactic category Syn^{g}(𝕋) of a geometric theory 𝕋: for a detailed exposition, see [16], chapter 8 or [15], chapter X. The objects of Syn^{g}(𝕋) are equivalence classes [ϕ(x⃗)] of geometric formulae-in-context in the language of 𝕋, where the equivalence relation identifies ϕ(x⃗) with ψ(y⃗) if the contexts x⃗ and y⃗ have the same type, and ψ is obtained from ϕ by substituting y_{i} for x_{i}, for each i. In defining morphisms [ϕ(x⃗)] → [ψ(y⃗)] in Syn^{g}(𝕋), we may therefore assume (and it is convenient to do so) that the contexts x⃗ and y⃗ have no variables in common; such a morphism is then defined to be a 𝕋-provable-equivalence class of geometric formulae in the concatenated context x⃗, y⃗ which are ‘𝕋provably functional from ϕ to ψ’, in the sense that the appropriate geometric axioms are derivable in 𝕋. The composite of two morphisms

[figure: [ϕ(x⃗)]; [θ(x⃗, y⃗)]; [ψ(y⃗)]; [γ(y⃗, z⃗)]; [χ(z⃗)]]

is defined to be the provable-equivalence class of the formula (∃y⃗)(θ∧γ). The verification that Syn^{g}(𝕋) is a (geometric) category is tedious but straightforward. Moreover, it contains a structure U_{𝕋} for the signature of 𝕋 obtained by setting U_{𝕋}A = [⊤(x)] (where x is a variable of sort A), U_{𝕋}(R ⊆ A⃗) = [R(x⃗)] ↣ [⊤(x⃗)], and U_{𝕋}(f: A⃗ → B) = [(f(x⃗) = y)]. A straightforward induction shows that, for every geometric formula-in-context ϕ(x⃗), the interpretation [ϕ(x⃗)]_{U_{𝕋}} is simply [ϕ(x⃗)], and hence we have:

Proposition 2.3 The Σ-structure U_{𝕋} in Syn^{g}(𝕋) is a conservative model of 𝕋; that is, it satisfies exactly those geometric axioms which are derivable from 𝕋. Moreover, it is universal amongst 𝕋-models in geometric categories, in the sense that for any geometric category C the functor

Geom (Syn^{g}(𝕋), C) \overline{}𝕋-Mod(C)

which sends a geometric functor F: Syn^{g}(𝕋) → C to the 𝕋-model F (U_{𝕋}), is an equivalence of categories. (Here Geom (Syn^{g}(𝕋), C) denotes the category of geometric functors Syn^{g}(𝕋) → C and arbitrary natural transformations between them.) □

If the theory 𝕋 is κ-geometric (for some κ < ∞), then we may restrict ourselves to κ-geometric formulae in defining the objects and morphisms of the syntactic category, and thus obtain a (small) κ-geometric category Syn_{κ}^{g}(𝕋) with the corresponding universal property. However, there is no real need to do so. Although Syn^{g}(𝕋) is a large category, there is a canonical form theorem for geometric formulae which says that every such formula is provably equivalent to one of the form ⋁_{i∈I} ϕ_{i} where the ϕ_{i} are regular formulae (that is, constructed using only finite conjunction and existential quantification): since we may clearly omit duplicate copies of the same formula from any such disjunction, it follows that we have, up to provable equivalence, only a set of distinct geometric formulae in any context. Since 𝕋-provably equivalent formulae-in-context define isomorphic objects of Syn^{g}(𝕋), it follows that the latter is (not only locally small but) essentially small, i.e. equivalent to a small category—indeed, it is equivalent to Syn_{κ}^{g}(𝕋) for sufficiently large κ.

When working with full first-order logic, we do not have any such canonical form theorem (indeed, as we noted in the Introduction, it is possible to generate a proper class of inequivalent propositional formulae from just two primitive proposition symbols), and so we shall have to be more careful about the size of the formulae which we admit in the construction of our syntactic category. Nevertheless, the purely formal parts of the construction go through without any essential change. If 𝕋 is a theory in L_{κ} (for some κ ≤ ∞), we define the syntactic category Syn_{κ}^{fo}(𝕋), exactly as in the geometric case, but admitting arbitrary formulae of L_{κ} in the definition of both the objects and the morphisms of the category. Just as before, we may verify

Proposition 2.4 The category Syn_{κ}^{fo}(𝕋) is a κ-Heyting category (small if κ < ∞), and contains a conservative 𝕋-model U_{𝕋} which is universal amongst 𝕋-models in κ-Heyting categories, in the sense that for any such category C the functor

κ-Heyt (Syn_{κ}^{fo}(𝕋), C) \overline{}𝕋-Mod(C)_{κ}

which sends a κ-Heyting functor F: Syn_{κ}^{fo}(𝕋) → C to the 𝕋-model F (U_{𝕋}), is an equivalence of categories. □

For a detailed proof of 2.4 in the case κ = ω, see [5], B.314. Note, incidentally, the change in the codomain of the displayed functor of 2.4 as compared with 2.3: we are required to cut down to the κ-elementary morphisms between 𝕋-models, in order to ensure that such morphisms correspond to natural transformations between functors defined on the syntactic category.

3 Syntactic sites and the completeness theorem

If C is a small κ-geometric category (for example, the syntactic category of a κ-geometric theory), we may equip it with the κ-covering Grothendieck topology J_{κ}: a sieve R on an object A of C belongs to J_{κ} iff it contains a family of maps (α_{i}: B_{i} → A | i ∈ I) of cardinality less than κ, such that the union of the images of the α_{i} is the whole of A. By ([16], proposition 3.3.3) or ([15], lemma X.5.4), we know that this topology is subcanonical (that is, all the representable functors C^{op} → Set are sheaves): moreover, a functor F: C → E (where E is a topos) is flat and J_{κ}-continuous iff it preserves finite limits, images and unions of families of subobjects of cardinality less than κ—that is, iff it is a κ-geometric functor. Thus, on combining 2.3 with Diaconescu’s theorem, we immediately obtain the standard proof of the existence of classifying toposes for κ-geometric theories: given such a theory 𝕋, we may take B^{g}(𝕋) to be the topos Sh(Syn_{κ}^{g}(𝕋), J_{κ}). Note also that, since the Yoneda embedding y: Syn_{κ}^{g}(𝕋) → B^{g}(𝕋) is full and faithful, the generic 𝕋-model G_{𝕋} = y(U_{𝕋}) satisfies only those geometric sentences which are satisfied in U_{𝕋} (equivalently, derivable from 𝕋).

In passing, we remark that the choice of the cardinal κ is not crucial, provided it is large enough for all the axioms of 𝕋 to be expressible in L_{κ}. The canonical form theorem for geometric formulae, mentioned in the last section, ensures that if κ < λ then every object of Syn_{λ}^{g}(𝕋) is the union of a family of subobjects of cardinality less than λ, all of which lie in Syn_{κ}^{g}(𝕋). Hence it is easy to verify that the inclusion

(Syn_{κ}^{g}(𝕋), J_{κ}) \overline{}(Syn_{λ}^{g}(𝕋), J_{λ})

satisfies the hypotheses of the Grothendieck Comparison Lemma (cf. [15], p. 588) and so gives rise to an equivalence of sheaf toposes. Once again, the corresponding result is very far from being true when we replace the ‘geometric’ versions of the syntactic categories by the ‘full first-order’ ones.

The key result of this section is the following lemma which, although it has a claim to be considered ‘folklore’, appears never to have been noticed in print before.

Lemma 3.1 Let C be a small Heyting category, and let J be a subcanonical Grothendieck topology on C. Then the Yoneda embedding y: C → Sh(C, J) preserves universal quantification.

Proof Let f: A → B be a morphism of C, A′ ↣ A a subobject of A, and write B′ ↣ B for ∀_{f}(A′ ↣ A). Let R ↣ yB be any subobject of yB in Sh(C, J) such that (yf)^{∗}(R) ≤ yA′ in Sub(yA); we must show that R ≤ yB′, i.e. that every morphism in R factors through B′ ↣ B. Let g: C → B be such a morphism, and let h: D → A be its pullback along f; then h ∈ f^{∗}(R), and so h factors through A′ ↣ A; that is, the image A′′ ↣ A of h satisfies A′′ ≤ A′. Since image factorizations in C are stable under pullback, it follows that the image B′′ ↣ B of g satisfies B′′ ≤ B′; so we have our required factorization. □

The above proof may be compared with that of the result (which is undoubtedly ‘folklore’) that the Yoneda embedding of a small cartesian closed category preserves exponentials. Indeed, in the particular case when C is locally cartesian closed as well as a Heyting category, it follows from the latter, since the functors ∀_{f} are simply the restrictions of the functors Π_{f} (the right adjoints to pullback between slice categories) to subobjects. However, the significance of 3.1 itself is contained in the following two immediate corollaries.

Corollary 3.2 If C is a small κ-Heyting category and J_{κ} denotes the κcovering topology on C, then the Yoneda embedding C → Sh(C, J_{κ}) is a κ-Heyting functor.

Proof We have already observed that y is a κ-geometric functor (i.e. that it preserves finite intersections, unions of cardinality less than κ, and images). By the Lemma, it preserves universal quantification (and hence also implication in the subobject lattices); and it clearly preserves all intersections of subobjects which exist in C. □

Corollary 3.3 (Completeness theorem for L_{κω}) Let 𝕋 be an arbitrary theory in L_{κω}(Σ). Then there exists a Grothendieck topos containing a conservative model of 𝕋, i.e. one satisfying only those sentences of L_{κω}(Σ) which are derivable from 𝕋; moreover, this topos may be taken to be localic over Set. In particular, any sentence of L_{κω}(Σ) which is satisfied in all 𝕋-models in localic toposes is derivable from 𝕋.

Proof Apply 3.2 to the syntactic category Syn_{κ}^{fo}(𝕋). We have seen that the universal model of 𝕋 in this category is conservative, and since the Yoneda embedding is full and faithful it reflects isomorphisms; so y(U_{𝕋}) is also a conservative model of 𝕋. To obtain such a model in a localic topos, we combine this observation with the result ([12], p. 59; [9], Proposition 4.4) that for any Grothendieck topos E there exists an open surjection F → E with F localic. □

Since the completeness theorem holds for all κ < ∞, it follows easily that its weak form holds for κ = ∞ as well: that is,

Corollary 3.4 If 𝕋 is a first-order theory and σ is any L_{∞} sentence satisfied in all models of 𝕋 in localic toposes, then σ is derivable from 𝕋.

Proof Given 𝕋 and σ, we can clearly choose κ such that 𝕋 ∪ {σ} ⊆ L_{κ}. So the result follows from 3.3. □

On the other hand, the strong form of the theorem (the existence of a single 𝕋-model which is L_{κ}-conservative) clearly fails for κ = ∞; for if 𝕋 is the empty theory over a signature Σ with two primitive proposition symbols, then the result of [11] mentioned in the Introduction implies that a topos containing an L_{∞}-conservative model of 𝕋 would have to have a proper class of subobjects of 1.

In the case κ = ω, 3.3 was proved by P. Freyd, around 1975; his proof may be found in [5] under the name ‘Stone representation theorem for logoi’ (and see also [4], theorem 5.22, where the theorem is stated in terms of models in categories of Heyting-valued sets). However, Freyd’s proof (which admittedly yields a more precise result) is much less direct than the above. The observation that y(U_{𝕋}) yields a conservative model of 𝕋 was made independently by E. Palmgren [19] and the first author.

We note also that y(U_{𝕋}) is a minimal model of 𝕋 in the sense of Moerdijk and Palmgren [17]. Since any κ-Heyting functor is a κ-geometric functor, the equivalence of 2.4 yields a full and faithful functor

𝕋-Mod(F)_{κ} \overline{}Top (F, Sh(Syn_{κ}^{fo}(𝕋), J_{κ}))  (5)

for any topos F, sending a 𝕋-model M in F to the geometric morphism whose inverse image extends the κ-Heyting functor F: Syn_{κ}^{fo}(𝕋) → F corresponding to M. In particular, for any such 𝕋-model M, we have a geometric morphism f such that f^{∗}(y(U_{𝕋})) ≅ M. It is easy to see that every open geometric morphism F → Sh(Syn_{κ}^{fo}(𝕋)) is in the image of (5) (since if f is open then the composite f^{∗} ∘ y is a κ-Heyting functor Syn_{κ}^{fo}(𝕋) → F, and so must be the functor which corresponds to the 𝕋-model f^{∗}y(U_{𝕋})). However, it is not the case in general that every 𝕋-model in F can be ‘classified’ in this way by an open geometric morphism. Nor is it the case that an arbitrary geometric morphism f into Sh(Syn_{κ}^{fo}(𝕋)) is determined up to isomorphism by the Σ-structure f^{∗}y(U_{𝕋}) (recall that a Σ-structure, according to our definition, consists of the objects and morphisms interpreting the primitive symbols of our language), even when the latter is a model of 𝕋. We shall investigate this problem further in 4.4–4.6 below.

4 The first-order theory of a topos

Let E = Sh(C, J) be a topos; for convenience, we shall assume in this section that the category C (is small and) has finite limits, so that flat functors on C are just finite-limit-preserving ones. The standard proof that E occurs as a geometric classifying topos B^{g}(𝕋) takes 𝕋 to be the theory of flat continuous functors on (C, J), which we may present as follows. The sorts of our signature Σ are the objects of C, and each morphism f: A → B of C is regarded as a unary function-symbol of Σ; there are no primitive predicate symbols except equality. The axioms of 𝕋 fall into three groups: the first group, consisting of all sentences (∀x)(1_{A}(x) = x) where 1_{A} is an identity morphism of C, and (∀x)(f(g(x)) = h(x)) whenever fg = h in C, ensures that 𝕋-models in a category F are in particular functors C → F. Then we have a group of axioms to ensure that the functors preserve finite limits: specifically, we take the sentences (∃x)⊤ and (∀x, y)(x = y) where x and y are variables of sort 1 (the terminal object of C), and for each pullback square

[figure: P; p; A; B; q; g; C; f]

in C we take the axioms (∀x, y)((f(x) = g(y))⇒(∃z)((p(z) = x)∧(q(z) = y))) and (∀z, z′)(((p(z) = p(z′)) ∧ (q(z) = q(z′))) ⇒ (z = z′)), where the sorts of the variables x, y, z are A, B, P respectively. Finally, to ensure that models correspond to continuous (i.e. cover-preserving) functors, we adopt the axiom

(∀x)(⊤⇒ ⋁_{i∈I}(∃y_{i})(f_{i}(y_{i}) = x)) ,

for each family (f_{i}: B_{i} → A | i ∈ I) generating a J-covering sieve. (If J can be generated by covering families of cardinalities less than κ, we note that the resulting theory 𝕋 is κ-geometric.)

The conditions on a flat continuous F for the corresponding geometric morphism to be open, which we established in 1.2, can readily be translated into (infinitary) first-order sentences in this language. Condition (1) becomes the sentence

(∀x)(⋀_{i∈I}( ⋁_{j∈J_{i}}(∃y_{j})(β_{j}(y_{j}) = x))⇔ ⋁_{k∈K}(∃y_{k})(β_{k}(y_{k}) = x))  (6)

where {β_{j}: B_{j} → A | j ∈ J_{i}} is a family of morphisms generating the closed sieve S_{i}, and {β_{k}: B_{k} → A | k ∈ K} similarly generates ⋂_{i∈I} S_{i}. And (2) becomes

(∀y)((∀x)((α(x) = y)⇒ ⋁_{i∈I}(∃z_{i})(β_{i}(z_{i}) = x))⇔ ⋁_{j∈J}(∃w_{j})(γ_{j}(w_{j}) = y)) (7)

where {β_{i}: C_{i} → A | i ∈ I} and {γ_{j}: D_{j} → B | j ∈ J} are generating families for S and ∀_{α}S respectively. (As we observed after the statement of 1.1, the bi-implications which appear in these two sentences could be replaced by unidirectional implications (⇒), since the reverse implications are automatic.)

We have thus established:

Proposition 4.1 For any Grothendieck topos E, there is an infinitary firstorder theory 𝕋 such that we have a natural equivalence

Open (F, E) ≃ 𝕋-Mod(F)

for all Grothendieck toposes F. □

Note that, on the right-hand side of the above equivalence, we have the category whose morphisms are arbitrary homomorphisms between 𝕋models, and not just the elementary morphisms: this is because by definition Open (F, E) is a full subcategory of Top (F, E), and we know that morphisms in the latter correspond to arbitrary homomorphisms of Σ-structures. However, we shall see in a moment that it is at least possible to choose 𝕋 in such a way that every homomorphism of 𝕋-models is ∞-elementary.

To do this, we consider the case when E is given as the (geometric) classifying topos of a geometric theory 𝕋, i.e. when (C, J) has the form (Syn_{κ}^{g}(𝕋), J_{κ}). In this case, it would clearly be advantageous to express the first-order theory (\overline{𝕋}, say) corresponding to E over the same signature as 𝕋, instead of passing to the larger signature required to describe functors on the syntactic category. In particular, we should hope that by taking \overline{𝕋} to consist of all first-order sentences which are satisfied in the generic model G_{𝕋}, we might obtain a theory adequate to characterize the open geometric morphisms into E. (Of course, this \overline{𝕋} is a proper class, and therefore not a theory as we defined it in section 2. However, it is clearly sufficient to choose a cardinal λ which strictly exceeds the sizes of all the subobject lattices Sub(G_{𝕋}(A⃗)), for A⃗ a finite string of sorts of Σ, and then to take \overline{𝕋} to consist of all the L_{λ} sentences satisfied by G_{𝕋}. Note that λ may well be strictly larger than the cardinal κ required to express 𝕋 as a theory in L_{κ}.)

Lemma 4.2 For the first-order theory \overline{𝕋} just described, every first-order formula-in-context is provably equivalent to a geometric formula-in-context; that is, given any formula-in-context ϕ(x⃗), we can find a geometric formula ψ in the same context such that (∀x⃗)(ϕ⇔ψ) is derivable in \overline{𝕋}.

Proof The interpretation of ϕ(x⃗) in the generic 𝕋-model G_{𝕋} will be some subobject of G_{𝕋}(A⃗), where A⃗ is the type of x⃗; but every such subobject also occurs as the interpretation of some geometric (indeed, λ-geometric, where λ is as above) formula-in-context ψ(x⃗). So the sentence in the statement of the lemma is satisfied in G_{𝕋}, and hence derivable in \overline{𝕋}. □

We shall call a theory geometrically saturated if it has the property described in the statement of Lemma 4.2. We note that, if 𝕋 is geometrically saturated, then any homomorphism of 𝕋-models is automatically ∞- elementary, since we already observed that (4) is always completable to a commutative square for geometric formulae. (However, it seems unlikely that this property characterizes geometrically saturated theories, since it also holds when every formula-in-context is provably equivalent to a positiveexistential formula—that is, one constructed using infinitary conjunction as well as the ‘geometric’ connectives.)

Proposition 4.3 Let 𝕋 be a geometric theory. Then, for any topos F, we have

Open (F, B^{g}(𝕋)) ≃ \overline{𝕋}-Mod(F) = \overline{𝕋}-Mod(F)_{∞} ,

where \overline{𝕋} is the full first-order theory of the generic 𝕋-model in B^{g}(𝕋).

Proof The equality \overline{𝕋}-Mod(F) = \overline{𝕋}-Mod(F)_{∞} follows from the fact that \overline{𝕋} is geometrically saturated, as we observed after 4.2. The equivalence with Open (F, B^{g}(𝕋)) follows from the fact that, since every object and morphism of Syn^{g}(𝕋) is (the interpretation in G_{𝕋} of) a formula-in-context of L, we can rewrite the conditions (6) and (7) as first-order sentences in this language. (The other first-order sentences above, which we used to axiomatize the theory of flat continuous functors on a site, can be similarly rewritten; but there is no need to do so, since they translate into sentences which are derivable from 𝕋.) For example, if β: B → A is the morphism

[ψ(y⃗)] \overline{[θ(x⃗, y⃗)]^{}}[ϕ(x⃗)]

of Syn^{g}(𝕋), then the clause (∃y)(β(y) = x) (where x and y are variables of sorts A and B) becomes the formula-in-context (∃y⃗)θ(x⃗). Thus we see that if a 𝕋-model in F satisfies all the first-order sentences satisfied by G_{𝕋}, its classifying map must be open; the converse is immediate. □

We note that, in addition to being geometrically saturated, the theory \overline{𝕋} of 4.3 is a geometrically conservative extension of 𝕋—that is, any geometric axiom derivable from \overline{𝕋} is already derivable from 𝕋—since G_{𝕋} is a (geometrically) conservative model of 𝕋. We shall see in 5.4 below that these two properties suffice to characterize \overline{𝕋} amongst extensions of 𝕋; and in 6.4 we shall give an example of how an explicit description of the classifying topos B^{g}(𝕋) may be used to give an explicit axiomatization of the theory \overline{𝕋}.

We also note that the two properties ‘geometrically saturated’ and ‘geometrically conservative’ imply that \overline{𝕋} is maximal amongst geometrically conservative extensions of 𝕋; that is, any proper extension of it will prove geometric axioms not derivable from 𝕋. However, this property does not suffice to characterize \overline{𝕋}; see 6.2 below.

Finally in this section, we consider what can be said about the first-order theory of a topos which is given to be of the form Sh(Syn_{κ}^{fo}(𝕋), J_{κ}) for some first-order theory 𝕋 in L_{κω}(Σ). In this case, we may again translate conditions (6) and (7) into first-order sentences in L_{λω}(Σ) for sufficiently large λ, and thus we obtain:

Proposition 4.4 Let 𝕋 be a theory in L_{κω}(Σ). Then there exists a cardinal λ > κ, and a theory \overline{𝕋} in L_{λω}(Σ), such that we have a natural equivalence

Open (F, Sh(Syn_{κ}^{fo}(𝕋), J_{κ})) ≃ \overline{𝕋}-Mod(F)_{∞}

for any topos F. Moreover, \overline{𝕋} is an L_{κ}-conservative extension of 𝕋, and has the property that every L_{∞ω}(Σ) formula-in-context is \overline{𝕋}-provably equivalent to a disjunction of L_{κω} formulae-in-context.

Proof Let γ be the cardinality of the set of morphisms of Syn_{κ}^{fo}(𝕋). Then it is clear that any closed sieve on an object of this category can be generated by at most γ morphisms, and that there are at most 2^{γ} closed sieves on any such object. Thus the index set of the conjunction appearing in (6) has cardinality at most 2^{γ}, and the disjunctions in both this condition and (7) are indexed by sets of cardinality at most γ. So, if we take λ to be (2^{γ})^{+}, and take \overline{𝕋} to consist of all L_{λ} sentences satisfied by y(U_{𝕋}), it will certainly include all instances of these two conditions. Thus we see that, given a 𝕋-model M in F, the geometric morphism f: F → Sh(Syn_{κ}^{fo}(𝕋)) which corresponds to it under (5) will be open iff M is actually a model of \overline{𝕋}. It follows that any L_{∞} sentence satisfied by y(U_{𝕋}) is satisfied in all \overline{𝕋}-models in toposes, and hence (by the L_{∞} version of the completeness theorem) derivable from \overline{𝕋}; so the latter really is the full first-order theory of y(U_{𝕋}). The conservativity of \overline{𝕋} over 𝕋 follows from the fact, already noted in 3.3, that y(U_{𝕋}) is an L_{κ}-conservative model of 𝕋. And the final assertion follows from the fact that every L_{∞} formula-in-context over Σ, when interpreted in y(U_{𝕋}), yields a subobject of some object of the site, which can be expressed as a closed sieve on that object and hence as the union of at most γ subobjects corresponding to L_{κ} formulae. (The same argument shows that every κ-elementary morphism between models of \overline{𝕋} is ∞-elementary, and hence justifies the subscript ∞ on the right-hand side of the displayed equivalence in the statement of the Proposition.) □

Corollary 4.5 Let 𝕋 be a first-order theory. If, for some cardinal κ such that 𝕋 is expressible in L_{κ}, the theory \overline{𝕋} of Proposition 4.4 is equivalent to 𝕋, then 𝕋 has a classifying topos in the sense defined in the Introduction.

Proof If \overline{𝕋} is equivalent to 𝕋, then every 𝕋-model is classified by an open geometric morphism into Sh(Syn_{κ}^{fo}(𝕋)) (that is, the image of (5) consists precisely of the open geometric morphisms); also, the argument at the end of the proof of 4.4 shows that every κ-elementary morphism of 𝕋-models is ∞-elementary. So we may take Sh(Syn_{κ}^{fo}(𝕋)) to be B^{fo}(𝕋). □

The criterion provided by 4.5 for existence of B^{fo}(𝕋) is not a very practical one, since it is in general very hard even to determine the axioms of \overline{𝕋}, let alone to determine whether they are derivable from those of 𝕋. In the next section, we shall provide a criterion (local smallness) which at least has the appearance of being more manageable, and which incidentally enables us to show that the converse of 4.5 is also true.

If 𝕋 fails to satisfy the hypothesis of 4.5, it is still of interest to consider what can be said about the relationships between the toposes Sh(Syn_{κ}^{fo}(𝕋)) for different values of κ. For the moment, let us fix a pair of regular cardinals κ < λ such that 𝕋 is expressible in L_{κ}. The inclusion functor Syn_{κ}^{fo}(𝕋) → Syn_{λ}^{fo}(𝕋) is clearly a κ-Heyting functor, and hence continuous (i.e. coverpreserving) when these two categories are equipped with the topologies J_{κ} and J_{λ} respectively; so it induces a geometric morphism

Sh(Syn_{λ}^{fo}(𝕋), J_{λ}) \overline{r_{κ}^{λ} ^{}}Sh(Syn_{κ}^{fo}(𝕋), J_{κ})

whose inverse image sends the minimal 𝕋-model in Sh(Syn_{κ}^{fo}(𝕋)) to that in Sh(Syn_{λ}^{fo}(𝕋)).

Moreover, it is easy to see that the diagram

𝕋-Mod(F)_{λ}  \overline{}Top (F, Sh(Syn_{λ}^{fo}(𝕋)))

[figure: 𝕋-Mod(F)_{κ}; Top (F, Sh(Syn_{κ}^{fo}(𝕋)))]

(8)

(where the left vertical arrow is the inclusion, the right vertical arrow is induced by composition with r_{κ}^{λ}, and the horizontal arrows are instances of (5)) commutes up to natural isomorphism for any F, since both ways round send a 𝕋-model in F to the geometric morphism induced by the κ-Heyting functor Syn_{κ}^{fo}(𝕋) → F which corresponds to it. Taking F = Sh(Syn_{κ}^{fo}(𝕋)), we see that the geometric morphism i_{κ}^{λ}: Sh(Syn_{κ}^{fo}(𝕋)) → Sh(Syn_{λ}^{fo}(𝕋)) which corresponds to the minimal 𝕋-model in Sh(Syn_{κ}^{fo}(𝕋)) satisfies r_{κ}^{λ} ∘ i_{κ}^{λ} ≅ 1; that is, Sh(Syn_{κ}^{fo}(𝕋)) is a retract of Sh(Syn_{λ}^{fo}(𝕋)). However, composition with i_{κ}^{λ} does not in general induce a commutative diagram similar to (8).

Corollary 4.6 For a first-order theory 𝕋 in L_{κ}, the following are equivalent:

(i) Sh(Syn_{κ}^{fo}(𝕋)) has the universal property of a classifying topos B^{fo}(𝕋); that is, for any topos F, the image of the functor (5) is exactly the category of open geometric morphisms F → Sh(Syn_{κ}^{fo}(𝕋)).

(ii) For all λ > κ, the geometric morphisms r_{κ}^{λ} and i_{κ}^{λ} defined above are equivalences.

(iii) For all λ > κ, the morphism r_{κ}^{λ} is open.

Proof (i) ⇒ (iii) by the definition of B^{fo}(𝕋).

(iii) ⇒ (ii): If r_{κ}^{λ} is open, then the composite

[figure: Syn_{λ}^{fo}(𝕋); Sh(Syn_{κ}^{fo}(𝕋)); (r_{κ}^{λ})^{∗}; Sh(Syn_{λ}^{fo}(𝕋))]

is a λ-Heyting functor, where the first factor corresponds to the minimal 𝕋-model in Sh(Syn_{κ}^{fo}(𝕋)); and the composite clearly corresponds to the minimal 𝕋-model in Sh(Syn_{λ}^{fo}(𝕋)). It follows that the composite i_{κ}^{λ} ∘ r_{κ}^{λ} is isomorphic to the identity; so r_{κ}^{λ} and i_{κ}^{λ} are inverse equivalences in Top.

(ii) ⇒ (i): If (ii) holds, then the minimal 𝕋-model in Sh(Syn_{κ}^{fo}(𝕋)) is an L_{λ}-conservative model of 𝕋, for all λ > κ. In particular, taking λ to be the cardinal defined in the proof of 4.4, we deduce that \overline{𝕋} is equivalent to 𝕋; so the result follows from 4.5. □

Given a theory 𝕋 which has no classifying topos (cf. 6.6 below), we can therefore expect the sequence of toposes Sh(Syn_{λ}^{fo}(𝕋)) to ‘grow unboundedly’ with the cardinal λ. It is tempting to speculate that it might be possible to embed Top in some larger 2-category in which one could compute the ‘limit as λ → ∞’ of these toposes, and hence obtain an object which might support a truly generic 𝕋-model, even in the cases when the sequence does not ‘stabilize’ for sufficiently large λ. But we shall not pursue these speculations here.

5 Locally small theories

Definition 5.1 Let 𝕋 be an infinitary first-order theory over a signature Σ. We say 𝕋 is locally small in a context x⃗ if there is a set Sx⃗ of formulae in the context x⃗, such that every L_{∞} formula in this context is 𝕋-provably equivalent to a member of Sx⃗. We say 𝕋 is locally small if it is locally small in every context over Σ.

Note that 𝕋 is locally small iff there exists a cardinal κ such that every L_{∞} formula-in-context over Σ is 𝕋-provably equivalent to an L_{κ} formula. Note also that any geometrically saturated theory, as defined after 4.2, is locally small, by the canonical form theorem for geometric formulae. Conversely, we have:

Lemma 5.2 Let 𝕋 be a locally small theory over a signature Σ. Then there exists a signature Σ′ extending Σ, and a geometrically saturated theory 𝕋′ over Σ′, such that 𝕋′ is ‘Morita-equivalent’ to 𝕋 in the sense that for every topos F we have an equivalence

𝕋-Mod(F)_{∞} ≃ 𝕋′-Mod(F)_{∞} ,

and these equivalences are natural with respect to open geometric morphisms.

Proof We use (a version of) the technique known to model-theorists as ‘Morleyization’: we extend the signature Σ by adding, for each context x⃗ and each member ϕ of Sx⃗, a new relation symbol R_{ϕ} ↣ A⃗ (where A⃗ is the type of x⃗). For the axioms of 𝕋′, we take those of 𝕋 together with all sentences of the form

(∀x⃗)(R_{ϕ}(x⃗)⇔ϕ) .

A straightforward induction then shows that every formula-in-context over Σ′ is 𝕋′-provably equivalent to a formula over Σ, and hence to an atomic formula over Σ′, so 𝕋′ is geometrically saturated (indeed ‘atomically saturated’). On the other hand, given any 𝕋-model M in a topos F, there is a unique way of interpreting the additional primitive symbols of Σ′ which makes M into a 𝕋′- model, and similar remarks apply to ∞-elementary morphisms between such models; so we have the required equivalence 𝕋-Mod(F)_{∞} ≃ 𝕋′-Mod(F)_{∞}. □

We are now ready for our main theorem:

Theorem 5.3 For an infinitary first-order theory 𝕋, the following conditions are equivalent:

(i) 𝕋 is locally small.

(ii) 𝕋 is Morita-equivalent to a geometrically saturated theory.

(iii) 𝕋 has a first-order classifying topos; i.e. there exists a topos B^{fo}(𝕋) containing a 𝕋-model G_{𝕋} such that, for every topos F, the functor

Open (F, B^{fo}(𝕋)) \overline{}𝕋-Mod(F)_{∞}

sending an open geometric morphism f to f^{∗}(G_{𝕋}) is an equivalence of categories.

Proof (i) ⇒ (ii) is Lemma 5.2.

(ii) ⇒ (iii): It is clear that, if two theories are Morita-equivalent in the sense of 5.2, then one has a first-order classifying topos iff the other does; so we may as well assume that 𝕋 itself is geometrically saturated. But, for a geometrically saturated theory 𝕋, the inclusion functor Syn_{∞}^{g}(𝕋^{g}) → Syn_{∞}^{fo}(𝕋) is an equivalence, where 𝕋^{g} denotes the geometric part of 𝕋, i.e. the set of all geometric axioms (strictly, of κ-geometric axioms for a sufficiently large κ) derivable from 𝕋. In particular, for such a κ, the inclusions Syn_{κ}^{fo}(𝕋) → Syn_{λ}^{fo}(𝕋) are equivalences for all λ > κ (since both categories are equivalent to Syn_{κ}^{g}(𝕋^{g})); so condition (ii) of 4.6 is trivially satisfied.

(iii) ⇒ (i): Suppose B^{fo}(𝕋) exists. It follows from the L_{∞} version of the completeness theorem (3.4) that the generic 𝕋-model G_{𝕋} in B^{fo}(𝕋) must be L_{∞}-conservative. Thus the lattice of 𝕋-provable-equivalence classes of formulae in a context x⃗ maps injectively to the subobject lattice Sub(G_{𝕋}(A⃗)), where A⃗ is the type of x⃗; hence it is a set. □

Note that it would be possible to give a direct proof of (i) ⇒ (iii) by exploiting the fact that, for a locally small theory 𝕋, the inclusion Syn_{κ}^{fo}(𝕋) → Syn_{∞}^{fo}(𝕋) is an equivalence for sufficiently large κ. However, the detour via geometrically saturated theories is of interest in its own right (cf. Example 6.3 below). Another benefit of the detour is the following corollary, promised in the last section:

Corollary 5.4 For any geometric theory 𝕋, there is (up to equivalence) exactly one geometrically conservative extension of 𝕋 which is geometrically saturated, namely the full first-order theory of the generic model in B^{g}(𝕋).

Proof We saw after 4.3 that the full first-order theory \overline{𝕋} of the generic 𝕋model has these two properties. Conversely, suppose 𝕊 is any extension of 𝕋 with these properties. Then 𝕊 is locally small, and so has a classifying topos B^{fo}(𝕊); and by the proof of (ii) ⇒ (iii) in 5.3 we see that in fact B^{fo}(𝕊) ≃ B^{g}(𝕊^{g}), and that this equivalence identifies the generic model of 𝕊 with the generic model of 𝕊^{g}. But 𝕊^{g} is equivalent to 𝕋 by conservativity; so all the sentences in \overline{𝕋} must be derivable from 𝕊, and conversely. □

6 Examples and applications

Example 6.1 If 𝕋 is a propositional theory (that is, if the signature Σ has no sorts—so that the only primitive symbols are propositions, and the only context is the empty one), then the syntactic category Syn_{∞}^{fo}(𝕋) is simply the complete Heyting algebra generated by the primitive propositions, modulo the filter generated by the propositions in 𝕋. Provided this algebra is small, the classifying topos B^{fo}(𝕋) is simply the topos of sheaves on it (for its canonical topology). For example, it is well known that the free complete Heyting algebra on one generator (unlike that on two generators, as previously mentioned) is a set: it has just one more element than the free Heyting algebra H on one generator, which is pictured on page 35 of [10] (the extra element comes immediately below the top element of H, and is the supremum of all the other elements of H). Equivalently, we may describe the free complete Heyting algebra as the algebra of ideals of H (since all but one of these ideals are principal); so if 𝕋 is the empty theory over the propositional signature with a single primitive proposition, we may identify B^{fo}(𝕋) with the topos of sheaves on H for the finite cover topology. (Note, incidentally, that this particular 𝕋 is not itself geometrically saturated.)

Example 6.2 If we consider the empty theory on one propositional generator p as a geometric theory, then its classifying topos B^{g}(𝕋) is well known to be the Sierpiński topos [2, Set] (cf. Example 2.1), or equivalently the topos of sheaves on the Sierpiński space 𝕊 = {0, 1} with just one open point. It is easy to see that the full first-order theory of this topos is axiomatized by the single proposition ¬¬p; geometrically, this corresponds to the fact that a continuous map X → 𝕊 is open iff the corresponding open subset of X is dense. From the explicit description of the free complete Heyting algebra on one generator mentioned in the previous example, it may be seen that 𝕋 has just two maximal geometrically conservative extensions; one is axiomatized by ¬¬p and the other by (p ∨ ¬p). But the latter is not geometrically saturated, since ¬p is not provably equivalent to a geometric formula.

Example 6.3 Let 𝕋 be a geometric theory whose geometric classifying topos B^{g}(𝕋) is Boolean. Since every geometric morphism into a Boolean topos is open ([9], 3.5), it follows easily that B^{fo}(𝕋) (exists and) coincides with B^{g}(𝕋). Conversely, if a geometric theory 𝕋 is equivalent to its geometrically saturated extension \overline{𝕋}, as defined in 4.3, then every geometric morphism into B^{g}(𝕋) is open, and so the latter must be Boolean. (Thus the phenomenon first observed by Kock [14], that the generic model of a geometric theory may satisfy first-order sentences not derivable from that theory, is typical of all such theories having non-Boolean classifying toposes.)

We recall that in [1] Blass and Scedrov characterized those coherent (that is, ω-geometric) theories whose classifying toposes are Boolean: their characterization involved the conjunction of two conditions, of which the first was a finiteness condition and the second was (the finitary version of) what we have called ‘geometric saturatedness’. (Actually, in defining the latter, they used a notion of ‘𝕋-provable equivalence’ relative to a classical logical calculus, rather than the (much more restrictive) constructive provable equivalence which we require. However, if it is already known that B^{g}(𝕋) is Boolean, then the two notions of equivalence agree, since each is equivalent to saying that the interpretations of two formulae-in-context coincide in the generic model.) Examples of such theories include the theories of infinite decidable sets, and of dense (trichotomous) linear orderings without endpoints.

Example 6.4 As an example of the explicit computation of the full firstorder theory of the generic model of a geometric theory, we consider the theory 𝕆 of objects: that is, the empty theory over the single-sorted signature with no primitive symbols except equality. It is well known ([8], 6.33; [15], VIII 4.3) that the object classifier B^{g}(𝕆) may be identified with the functor category [Set_{f}, Set], where Set_{f} is (a small skeleton of) the category of finite sets, the generic object G_{𝕆} being the inclusion functor Set_{f} → Set. If one considers what first-order sentences are satisfied by G_{𝕆}, it is not hard for anyone familiar with Kripke–Joyal semantics to verify that they include (∀x, y)¬¬(x = y), ¬¬(∃x)⊤ and

(∀x_{1}, …, x_{n})¬(∀y) ⋁_{i=1}^{n}(y = x_{i})  (9)

for each n > 0. (We can think of the first two sentences as saying that G_{𝕆} is ‘not not a singleton’, and of (9) as saying that it is ‘not not infinite’. Note also that the second axiom may be considered as the case n = 0 of (9).)

Many years ago, the second author conjectured that the above sentences might suffice to axiomatize the full first-order theory of G_{𝕆}; but at the time he lacked any means of verifying or disproving this conjecture. With the machinery provided by section 1 of this paper, we are now able to show that the conjecture is false, but that it is in a sense ‘very close to the truth’. In the first place, we note that since any monomorphism with nonempty domain in Set_{f} is split, a cosieve on a nonempty object of Set_{f} is determined by the epimorphisms which it contains; and since there are (up to isomorphism) only finitely many epimorphisms with a given domain in Set_{f}, it follows that the subobject lattice of each representable functor Set_{f} → Set is finite. (In the notation introduced before 4.2, we can take the cardinal λ to be ω.) In particular, in determining what it means for a flat functor Set_{f}^{op} → F to induce an open geometric morphism, we do not have to worry about condition (1) of 1.2, on infinite intersections of subobjects; all the work is done by condition (2), on universal quantification. Further, since Set_{f} is generated as a category by the surjections (n + 1) → n which identify a single pair of elements and the injections n → (n + 1) which add a single new element, it suffices to consider condition (2) for morphisms of these two forms.

Of course, given an object A of a topos F, the corresponding flat functor F: Set_{f}^{op} → F is simply the functor n ↦ A^{n}; equivalently, it sends n to the interpretation [⊤(x_{1}, …, x_{n})]_{A}. A cosieve R on n in Set_{f}, as we observed above, is generated by a finite set of surjections with domain n: each of these is in turn specified by a finite list of pairs of elements of n to be identified, and so we can think of R as the interpretation in G_{𝕆} of a finite disjunction of finite conjunctions of equations (x_{i} = x_{j}); that is, of a positive quantifier-free formula ϕ in the context (x_{1}, …, x_{n}).

Now let α: n + 1 → n be the surjection which identifies the last two elements of n + 1, and suppose given a cosieve R on n, corresponding to a positive quantifier-free formula ϕ. The cosieve ∀_{α}(R) on n + 1 consists of all those morphisms n + 1 → p whose pushouts along α lie in R; but we may restrict our attention to surjections, which correspond to finite conjunctions of equations in (x_{1}, …, x_{n}, x_{n+1}), and the condition for such a conjunction ψ to determine a morphism in ∀_{α}(R) is simply that

(∀x_{1}, …, x_{n+1})((ψ ∧ (x_{n} = x_{n+1}))⇒ϕ)  (10)

should be provable. On the other hand, if F: Set_{f}^{op} → F corresponds to an object A of F, then ∀_{F (α)}(F (R)) is the largest subobject of A^{n+1} whose intersection with F (α): A^{n} ↣ A^{n+1} is contained in F (R); that is, it is the interpretation in A of the formula ((x_{n} = x_{n+1})⇒ϕ). So in this case condition (2) becomes the validity in A of the sentence

(∀x_{1}, …, x_{n+1})(((x_{n} = x_{n+1})⇒ϕ)⇒ ⋁ ψ) ,  (11)

where the disjunction on the right is over all finite conjunctions of atomic formulae ψ satisfying (10). However, since ϕ does not involve x_{n+1}, from ((x_{n} = x_{n+1}) ⇒ ϕ) we may deduce ((x_{n} = x_{n}) ⇒ ϕ) by substitution, and provided ϕ actually involves a variable this reduces to ϕ; so (11) is automatically satisfied except possibly in the cases when ϕ is either ⊤ or ⊥. For ϕ = ⊤ it is again automatic; and for ϕ = ⊥ it simply reduces to (∀x_{1}, …, x_{n+1})(((x_{n} = x_{n+1}) ⇒ ⊥) ⇒ ⊥), which is (essentially) the first of the three sentences listed above.

For the injections n → n + 1, it is necessary to consider the case n = 0 separately, and we deal with this first. There are only two cosieves on 1 in Set_{f}, and the validity of (2) for the top one is again automatic, so we need only consider the empty cosieve. The universal quantification of this cosieve along 0 → 1 is again empty, whereas if we perform the quantification in F we obtain [(∀x)⊥]_{A} = [¬(∃x)⊤]_{A}, so the condition we obtain is simply the sentence ¬¬(∃x)⊤.

Finally, consider the inclusion β: n → n + 1 (n > 0) and a cosieve R on n + 1, corresponding to a positive quantifier-free formula ϕ in (x_{1}, …, x_{n+1}). We find that a surjection from n, corresponding to a conjunction of atomic formulae ψ in (x_{1}, …, x_{n}), belongs to ∀_{β}(R) iff (∀x_{1}, …, x_{n+1})(ψ ⇒ ϕ) is provable. So condition (2) in this case becomes the sentence

(∀x_{1}, …, x_{n})((∀x_{n+1})ϕ⇒ ⋁ ψ),

where the disjunction is over all ψ as above. If ϕ itself does not mention x_{n+1}, this is trivially satisfied; if it does, then from ϕ we may deduce (⋁_{i=1}^{n}(x_{n+1} = x_{i}) ∨ ϕ′), where ϕ′ is the disjunction of all those conjunctions of equations in ϕ that do not mention x_{n+1}. So the condition we require is

(∀x_{1}, …, x_{n})((∀x_{n+1})( ⋁_{i=1}^{n}(x_{n+1} = x_{i}) ∨ ϕ)⇒ϕ) ,  (12)

where ϕ is any positive quantifier-free formula in (x_{1}, …, x_{n}). Of course,

(9) is just the special case of this when ϕ = ⊥; conversely, we could deduce (12) from (9) if we had the (constructively invalid) ‘dual Frobenius rule’ that (∀x)(χ ∨ ϕ) entails ((∀x)χ ∨ ϕ) provided x is not free in ϕ. Thus our axiomatization of the full first-order theory of G_{𝕆} is exactly that conjectured above, except for the replacement of the scheme (9) by the stronger (12).

We remark that (12) is a genuine strengthening of (9). Let F = [N, Set] where N is the ordered set of natural numbers; thus objects of F are diagrams of the form

[figure: A(0); α_{0}; A(1); α_{1}; A(2); · · · .]

Let A be the object defined by A(i) = {0, 1} for all i, and α_{i}(0) = α_{i}(1) = 0 for all i. Then A satisfies (9) (as well as the other two conditions in our axiomatization), but fails to satisfy (12) for n = 2 with ϕ taken to be (x_{1} = x_{2}). Note also that the classifying map F → B^{g}(𝕆) of A is induced by a functor N → Set_{f} (namely A itself!); it may be verified that this functor satisfies (the dual of) condition (a) of ([9], 2.5) but not condition (b) or (c), and so the classifying map of A is sub-open but not open. On the other hand, if we modify A by taking each A(i) to be a three-element set, then its classifying map is not even sub-open.

Similar techniques may be used to axiomatize the full first-order theories of other familiar toposes such as the topos of simplicial sets.

Example 6.5 In [17], Moerdijk and Palmgren construct a topos containing a minimal model of Heyting arithmetic (HA). It is easy to see that their construction is exactly that of the topos Sh(Syn_{ω}^{fo}(HA)), together with the minimal model y(U_{HA}). On the other hand, the minimal model which they construct for the theory HAI (Heyting arithmetic extended by an external induction scheme for standard natural numbers and an overspill principle), is not simply y(U_{HAI}), since it is not conservative (see [17], 4.10).

Example 6.6 The fact (already mentioned in the Introduction) that the free complete Heyting algebra on two generators is a proper class [11] enables us to show that ‘most’ familiar theories are not locally small. Given a theory 𝕋 and a context x⃗, let us say that two formulae ϕ and ψ in the context x⃗ form a free pair if, given any topos E and any two subobjects U, V of the terminal object of E, we can find a 𝕋-model M in E, together with an assignment of elements c_{i}: 1 → MA_{i} to the variables x_{i} in x⃗, such that the interpretations [ϕ(c⃗)]_{M} and [ψ(c⃗)]_{M} are U and V respectively. (For example, if 𝕋 is the theory of objects (as in 6.4), then the formulae (x = y) and (y = z) are a free pair in the context (x, y, z), since we can take M to be the colimit of the diagram

[figure: 1; U; 1; V; 1 ,]

with the obvious assignment of values to the three variables. The same pair of formulae will be free for any (single-sorted) theory 𝕋 with the property that any object of a topos can occur as a subobject of the underlying object of a 𝕋-model.) If 𝕋 has a free pair of formulae in the context x⃗, then it cannot be locally small in that context, since by taking E = Sh(H_{κ}) (where H_{κ} is a two-generator complete Heyting algebra of cardinality at least κ, as in the Introduction) and taking U and V to be the generators of H_{κ}, we see that the propositional combinations of the free pair of formulae will yield at least κ inequivalent formulae in the context x⃗.

References

[1] A. Blass and A. Scedrov: Boolean classifying topoi, J. Pure Appl. Alg. 28 (1983), 15–30.

[2] A. Boileau and A. Joyal: La logique des topos, J. Symbolic Logic 46 (1981), 6–16.

[3] R. Diaconescu: Change of base for toposes with generators, J. Pure Appl. Alg. 6 (1975), 191–218.

[4] M.P. Fourman and D.S. Scott: Sheaves and logic, in M.P. Fourman, C.J. Mulvey and D.S. Scott, editors, Applications of Sheaves, Lecture Notes in Math. 753 (Springer–Verlag, 1979), 302–401.

[5] P.J. Freyd and A. Scedrov: Categories, Allegories (North–Holland, 1990).

[6] H. Gaifman: Infinite Boolean polynomials, I, Fund. Math. 54 (1964), 229–250.

[7] A.W. Hales: On the non-existence of free complete Boolean algebras, Fund. Math. 54 (1964), 45–66.

[8] P.T. Johnstone: Topos Theory, L.M.S. Monographs no. 10 (Academic Press, 1977).

[9] P.T. Johnstone: Open maps of toposes, Manuscripta Math. 31 (1980), 217–247.

[10] P.T. Johnstone: Stone Spaces, Cambridge Studies in Advanced Math. 3 (Cambridge University Press, 1982).

[11] D. de Jongh: A class of intuitionistic connectives, In J. Barwise, H.J. Keisler and K. Kunen, editors, The Kleene Symposium (North– Holland, 1980), 103–111.

[12] A. Joyal and M. Tierney: An Extension of the Galois Theory of Grothendieck, Mem. Amer. Math. Soc. 309 (American Mathematical Society, 1984).

[13] C. Kalicki: Infinitary propositional intuitionistic logic, Notre Dame J. Formal Logic 21 (1980), 216–228.

[14] A. Kock: Universal projective geometry via topos theory, J. Pure Appl. Alg. 9 (1976), 1–24.

[15] S. Mac Lane and I. Moerdijk: Sheaves in Geometry and Logic (Springer– Verlag, 1992).

[16] M. Makkai and G.E. Reyes: First Order Categorical Logic, Lecture Notes in Math. 611 (Springer–Verlag, 1977).

[17] I. Moerdijk and E. Palmgren: Minimal models of Heyting arithmetic, J. Symbolic Logic, to appear.

[18] M.E. Nadel: Infinitary intuitionistic logic from a classical point of view, Ann. Math. Logic 14 (1978), 159–191.

[19] E. Palmgren: Constructive sheaf semantics, Math. Logic Quarterly, to appear.

[20] R.M. Solovay: New proof of a theorem of Gaifmann and Hales, Bull. Amer. Math. Soc. 72 (1966), 282–284.

Recent BRICS Report Series Publications

RS-97-20 Carsten Butz and Peter T. Johnstone. Classifying Toposes for First Order Theories. July 1997. 34 pp.

RS-97-19 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects. July 1997. iv+64 pp. Aappears also as Technical Report 429, University of Cambridge Computer Laboratory, June 1997. To appear in Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FCT&TCS ’97 Proceedings, LNCS, 1997.

RS-97-18 Robert Pollack. How to Believe a Machine-Checked Proof. July 1997. 18 pp. To appear as a chapter in the book Twenty Five Years of Constructive Type Theory, eds. Smith and Sambin, Oxford University Press.

RS-97-17 Peter Bro Miltersen. Error Correcting Codes, Perfect Hashing Circuits, and Deterministic Dynamic Dictionaries. June 1997. 10 pp.

RS-97-16 Noga Alon, Martin Dietzfelbinger, Peter Bro Miltersen, Erez Petrank, and Gábor Tardos. Linear Hashing. June 1997. 22 pp. A preliminary version appeared with the title Is Linear Hashing Good? in The Twenty-ninth Annual ACM Symposium on Theory of Computing, STOC ’97, pages 465–474.

RS-97-15 Pierre-Louis Curien, Gordon Plotkin, and Glynn Winskel. Bistructures, Bidomains and Linear Logic. June 1997. 41 pp.

RS-97-14 Arne Andersson, Peter Bro Miltersen, Søren Riis, and Mikkel Thorup. Dictionaries on AC^{0} RAMs: Query Time Θ(\sqrt{log n/ log log n}) is Necessary and Sufficient. June 1997. 18 pp. Appears in 37th Annual Symposium on Foundations of Computer Science, FOCS ’96 Proceedings, pages 441–450.

RS-97-13 Jørgen H. Andersen and Kim G. Larsen. Compositional Safety Logics. June 1997. 16 pp.