In this section we present a topos-theoretic interpretation of Fraïssé's construction in Model Theory leading to a substantial generalization of the well-known result (Theorem 7.4.1(a) in this book) providing the link between Fraïssé's construction and countably categorical theories. In fact, the three concepts involved in the classical Fraïssé's construction (i.e. amalgamation and joint embedding properties, homogeneous structures, atomicity of the resulting theory) are seen to correspond precisely to three different ways (resp. of geometric, semantic and syntactic nature) of looking at the same classifying topos, and the technical relationships between them are seen to arise precisely from the expression of topos-theoretic invariant properties of this classifying topos in terms of different sites of definition for it, according to the philosophy 'toposes as bridges'.
In other words, the classifying topos acts as a 'bridge' allowing a transfer of properties between the different sites of definition of it, the translation between any two such properties of the sites being given by the expression of a unique invariant defined at the topos-theoretic level in terms of the two different site representations of the topos.
The context in which we shall work is that of theories of presheaf type. Recall that this is a very extensive class of geometric theory notably including all the finitary algebraic theories and many other interesting mathematical theories pertaining to different fields of Mathematics.
Let be a theory of presheaf type such that its category of finitely presentable models satisfies the amalgamation property (i.e. the property that any two arrows with common domain can be completed to a commutative square):
Then we can put on the opposite category the atomic topology , obtaining a subtopos of the classifying topos of , which, once chosen a canonical Morita-equivalence for , corresponds by the duality theorem to a unique quotient of . This quotient can be characterized as the theory over the signature of obtained from by adding all the sequents of the form , where and are formulae which present a -model and is a -provably functional formula from to (since the sieves generated by a single arrow generate the topology - see here). Semantically, the theory axiomatizes the homogeneous models of , that is the models of in Set such that for any arrow in and any arrow in there exists an arrow in such that :
For this reason, we shall call the 'theory of homogeneous -models'.
Now, the duality theorem ensures that the topos can be identified with the classifying topos of the theory , and hence, by the syntactic method for constructing classifying toposes, we have a Morita-equivalence
,
where is the geometric syntactic site of the theory , which we can use to build 'bridges' between the two sites by considering appropriate topos-theoretic invariants on the given classifying topos:
First of all, we observe that the fact that
is an atomic site
implies, by a well-known site characterization, that the topos
is
atomic (i.e. every subobject lattice in the topos is an
atomic Boolean algebra, in other words every subobject in the topos can
be written as a union of subobjects which do not contain any proper
subobject). By looking at this invariant from the point of view of the
other site
we obtain, as an application of a general site characterization for
atomic toposes obtained in this
paper, that the theory
is
atomic in a model-theoretic sense, that is every geometric formula over its
signature is
-provably
equivalent to a disjunction of
-complete
formulae in the same context (where by a
-complete
formula we mean a geometric formula
such that
the sequent
is
not provable in
and
for every geometric formula
in the same
context either
or
is
provable in
).
Moreover, by considering site characterizations for the invariant property of an object of a topos to be an atom (that is, to be non-zero and to have no proper subobjects), we obtain that every formula which presents a -model is -complete. Indeed, if we denote by and the composition of the relevant Yoneda embedding and associated sheaf functor for the two sites, we have that for any finitely presentable -model the objects and , where is the formula presenting , correspond to each other under the Morita-equivalence for considered above. Now, the fact that is the atomic topology easily implies that is an atom, while the fact that is an atom is precisely equivalent to the condition of -completeness of the formula . In general, it is not true that all the atoms of the classifying topos of have this form, but we can say that if an object of the form is an atom, then there exists a -provably functional epimorphism from a formula presenting a -model to .
On the other hand, one can attempt to obtain a site characterization of the atoms in an atomic topos of the form , where is an atomic site (i.e., is a category satisfying the dual of the amalgamation property and is the atomic topology on it). We observe that, since every atom of is a quotient of an object of the form (for an object of ), where is the composite of the Yoneda embedding with the associated sheaf functor and in every topos any epimorphism is the coequalizer of its kernel pair, every atom of is of the form , where is the coequalizer in of the pair of natural projections corresponding to a subobject in containing the diagonal subobject; notice that can be thought of as a set of arrows with common domain and codomain which is closed under composition with arbitrary pairs of identifcal arrows. In particular, we can suppose to contain a subobject of the form for two arrows and with common domain and codomain . Now, if for any pair of arrows and in with common domain and codomain there is an arrow such that , then the -closure of is contained in the -closure of the diagonal subobject and hence the latter coincides with the -closure of , from which it follows that is isomorphic to . Summarizing, we have the following
Proposition: Let be an atomic site. If any pair of arrows in with common domain and codomain can be equalized by an arrow in , then any atom in the topos is isomorphic to an object of the form .
The proposition cannot be applied to non-trivial subcanonical atomic sites; indeed, an atomic site is subcanonical if and only if all the arrows in are regular epic (cf. Example C2.1.12(c) in the Elephant), and hence two distinct arrows are not equalized in . In fact, for subcanonical sites , a necessary condition for any atom of to be isomorphic to an object of the form is that possesses coequalizers.
For example, for any (discrete) group , the topos is atomic and its atoms can be identified with the transitive -sets, while there is only one representable, namely the functor sending the unique object of to the underlying set of .
Applying the proposition in the context of the atomic site considered above, we obtain in particular the following result: if every pair of homomorphisms between finitely presentable -models can be coequalized in , then any -complete formula presents a -model.
Now, we consider the invariant property of a topos to be two-valued (in the sense that its only two subterminal objects are the zero and the identity one, and they are distinct from each other) in connection with the above-mentioned Morita-equivalence for .
For any site , the subterminal objects of the topos can be identified with the -ideals on , that is the sets of objects of with the property that for any arrow in , implies , and for any -covering sieve on an object , if for all then . By using this characterization, it is easy to see that for any atomic site such that is non-empty, the topos is two-valued if and only if the opposite of satisfies the joint embedding property, that is the property that for any two objects in the category there exists a third object and arrows from the two objects to it:
On the other hand, the characterization applied to the case of the classifying topos of a geometric theory , represented as the topos of sheaves on its geometric synstactic site yields the following criterion: the topos is two-valued if and only if the theory is complete, in the sense that every geometric sentence over the signature of is either probably false or provably true, but not both. Notice that if a theory is complete then in particular all its set-based models satisfy the same geometric sentences; the converse also holds if the theory has enough set-based models.
By applying these criteria in the context of the Morita-equivalence
we obtain the following logical equivalence: the category satisfies the joint embedding property if and only if the theory is complete.
Finally, we recall from this paper that, assuming the axiom of countable choice, every geometric theory which is atomic and complete is countably categorical, that is any two of its set-based countable models are isomorphic.
Summarizing, we have the following
Theorem: Let be a theory of presheaf type such that the category of its finitely presentable models satisfies the amalgamation property. Then the theory of homogeneous -models is atomic, and it is complete if and only if the category satisfies the joint embedding property; in particular, assuming the axiom of countable choice, if satisfies both amalgamation and joint embedding properties then is countably categorical. Moreover, every geometric formula which presents a -model is -complete, and if every pair of homomorphisms between finitely presentable -models can be coequalized in then any -complete formula presents a -model.
Notice that the theorem represents a faithful application of our philosophy 'toposes as bridges' in the context of the canonical Morita-equivalence induced by a theory of presheaf type, and the invariant notion of subtopos, the invariant property of a topos to be atomic and two-valued and the invariant property of an object of a topos to be an atom:
Our main theorem represents a substantial generalization of the well-known result (Theorem 7.4.1(a) in this book) allowing to build countably categorical theories through Fraïssé's method. Indeed, the classical result can be obtained as a particular case of our theorem when the theory is the quotient of the empty theory over a finite signature corresponding, as in this remark, to a uniformly finite collection of finitely presented models of the empty theory satisfying the hereditary property.
In fact, as argued in this section, the context of theories of presheaf type is a very general and natural one both from a mathematical and model-theoretic perspective, and there are many effective means for generating theories of presheaf type or verifying that a certain theory if of presheaf type.
Among the most natural contexts of application of our theorem, we can mention the following:
The theory of decidable objects (that is, the theory over a one-sorted signature with no function or relation symbols except for a binary relation whose only axioms are the coherent sequents expressing the idea that this relation behaves as a complement to the equality relation on the given sort) is of presheaf type, and its homogeneous models in Set are precisely the infinite sets. The classifying topos for such a theory can be identified with the Schanuel topos, that is the topos of sheaves on the opposite of the category of finite sets (i.e. finitely presentable models of the theory of decidable objects) and injections between them.
The theory of decidable Boolean algebras (that is, the algebraic theory of Boolean algebras enriched with a provable complement to the equality relation as in the example above) is of presheaf type. Its finitely presentable models are precisely the finite Boolean algebras, while its homogeneous models are precisely the atomless Boolean algebras; under the assumption of the axiom of countable choice, we thus recover the well-known result that any two countable atomless Boolean algebras are isomorphic.
The theory of decidable linear orders (that is, the theory of linear orders enriched with a binary predicate providing a provable complement to the equality relation) is of presheaf type, and its category of finitely presentable models coincide with the category of finite linear orders and order-preserving injections between them. Its homogeneous models in Set are precisely the dense linear orders without endpoints. The theorem thus ensures that such a theory is atomic and complete.
As shown in this paper, the (infinitary) geometric theory of fields of finite characteristic which are algebraic over their prime fields is of presheaf type, while the theory of its homogeneous models can be identified with the theory of fields of finite characteristic which are algebraic over their prime fields and algebraically closed; the completions of this theory are obtained precisely by adding the axiom specifying a given characteristic of the field. Our theorem thus encompasses, if one assumes the countable axiom of choice, the well-known fact that any two (countable) algebraic closures of a given finite field are isomorphic, while, if one does not assume any form of the axiom of choice, it still implies a remarkable property, namely the fact that any two algebraic closures of a given finite field satisfy the same first-order sentences (possibly containing infinitary disjunctions) written in the language of fields (in fact, this property is true more generally for any base field, cf. this section).
Of course, the consideration of other invariants in connection with the same bridge leading to our main theorem will lead to other relationships between the geometry of the category and the syntactic properties of the theory . For example, the consideration of the invariant notion of arrow between two atoms leads to the following
Proposition: Let be a theory of presheaf type such that the category of its finitely presentable models satisfies the amalgamation property. If all the arrows in are regular epimorphisms, then any -provably functional geometric formula from a formula which presents a -model to another formula which presents a -model is -provably functional between the same formulae (equivalently, corresponds to a -model homomorphisms between the two models presented by the formulae).
Indeed, given two formulae and presenting respectively -models and , the objects and (resp., and ) correspond to each other under the Morita-equivalence
,
and the arrows in correspond precisely to the -provably functional formulae , while, if is subcanonical (equivalently, any arrow in is a regular epimorphism), the arrows in correspond to the arrows in (equivalently, by this result, the -provably functional formulae ).
In fact, we will re-consider the same invariant below in the context of the Galois-type representations for the classifying topos of .
Another natural application of the 'bridge technique' in the context of the above-mentioned Morita-equivalence is obtained by considering the invariant property of a topos to have enough points. Recall that a point of a topos is a geometric morphism from the topos Set of sets to the topos; a topos is said to have enough points if the collection of the inverse images of all its points is jointly conservative, i.e. jointly reflects isomorphism. One can easily prove (cf. this paper) that the classifying topos for a geometric theory has enough points if and only if the theory has enough set-based models, in the sense that any geometric sequent which is valid in all set-based models of the theory is provable in it. It is interesting to consider the invariant 'to have enough points' in combination with the invariant 'to be non-trivial' (recall that a topos is said to be non-trivial if the initial and terminal object of it are non-isomorphic) in the context of the investigation of the existence of points of a given topos; indeed, it is obvious that if a non-trivial topos has enough points then it has at least a point. It turns out that one can profitably exploit the geometry of sites of definition of a topos to investigate this kind of issues; for instance, any coherent topos (i.e., a topos admitting as site of definition a site consisting of a cartesian category and a finite-type topology on it - for example, the classifying topos of a coherent theory) has, under the assumption of the axiom of choice, enough points (by a theorem of Deligne). For instance, one can prove (see this paper) that for any small category , the theory of flat functors on can be axiomatized coherently over its language if and only if the category has all fc finite limits (that is, for any finite diagram with values in the category there is a finite family of cones over it such that every cone over the diagram factors through one in the family). Since this theory is classified by the presheaf topos , the theory obtained from it by adding the axiom
is classified by the topos, and hence it remains
coherent if the original theory is. Therefore, if the category
has all fc
finite limits, then the topos
is
coherent and hence, assuming the axiom of choice, it has enough points.
This remark is useful because it can be combined with the easy
observation that the topos
is
non-trivial if and only if the
category
is
non-empty.
By applying these considerations in connection to the Morita-equivalence
we thus obtain the following existence theorem for homogeneous models.
Theorem: Let be a theory of presheaf type such that its category of finitely presentable models satisfies the amalgamation property. Assuming the axiom of choice, if the category is non-empty (equivalently, has a model in Set) and has all fc finite colimits, then there exists a homogeneous -model in Set.
Notice that this result represents a consistency result for logical theories arising from purely combinatorial/geometrical considerations.
It is worth to remark that, for any theory of presheaf type such that its category satisfies the amalgamation property, the theory of homogeneous -models admits an alternative axiomatization arising from a different representation of its classifying topos.
In order to describe this axiomatization, we first need to introduce the notion of Booleanization of a topos. It is well-known that the double-negation operation on subobjects of the topos defines a closure operation, and that the full subcategory of the topos consisting of the sheaves w.r.t this operation (that is, of the objects such that any arrow to them can be uniquely extended along any dense monomorphisms w.r.t. the operation) defines a Boolean subtopos of the original topos, called the Booleanization of the topos. In fact, the Booleanization enjoys the universal property of being the largest dense Boolean subtopos of the given topos. The notion of Booleanization is a topos-theoretic invariant admitting natural site characterizations; in particular, we have the following results:
For any small category , the Booleanization of the topos is isomorphic to the canonical geometric inclusion , where is the dense topology on , that is the Grothendieck topology on whose covering sieves are exactly the stably non-empty ones; in particular, if the dual of satisfies the amalgamation property then the Booleanization of coincides with the canonical inclusion .
For any geometric theory , the Booleanization of its classifying topos can be identified with the subtopos of it corresponding via the duality theorem to the quotient of defined as follows: is obtained from by adding all the sequents of the form , where is stably consistent with repsect to , that is a geometric formula such that for any geometric formula in the same context, implies . We call the theory the Booleanization of the theory .
A consideration of the invariant notion of Booleanization of a topos in the context of the Morita-equivalence
thus leads, in view of the duality theorem, to the equality of the theory of homogeneous -models with the Booleanization of .
In fact, as we saw in this section, the invariant property of a topos to be Boolean also admits natural site characterizations. In particular, a geometric theory is Boolean (i.e., classified by a Boolean topos) if and only if for every geometric formula over the signature of there exists a geometric formula such that and are provable in .
Notice that, as any atomic topos is Boolean (since every atomic frame is isomorphic to a powerset and hence Boolean), any atomic theory is Boolean.
An important property of Boolean geometric theories is the fact that every first-order formula (possibly containing infinitary disjunctions) is provably equivalent in the theory, using classical logic, to a geometric formula in the same context (cf. this paper for a detailed proof). This property has two easy but remarkable consequences:
Any Boolean geometric theory is complete as a geometric theory (in the sense which we defined above) if and only if it is complete in the sense of classical Model Theory (that is, every first-order sentence over the signature of the theory is provably false or provably true using classical logic, but not both). In general, such an equivalence between the two notions only holds at the cost of replacing the given first-order theory with a geometric theory over a larger signature, e.g. its Morleyization.
Any Boolean geometric theory (in particular, any theory of homogeneous models) is model-complete (in the sense of classical Model Theory), that is every embedding of set-based models of it is an elementary embedding.