By a classifying topos for a first-order theory , we mean a topos such that, for any topos models of in correspond exactly to open geometric morphisms → . We show that not every 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. (shrink)

Let C be a small Barr-exact category, Reg the category of all regular functors from C to the category of small sets. A form of M. Barr's full embedding theorem states that the evaluation functor e : C →[Reg, Set ] is full and faithful. We prove that the essential image of e consists of the functors that preserve all small products and filtered colimits. The concept of κ-Barr-exact category is introduced, for κ any infinite regular cardinal, and the natural (...) generalization to κ-Barr-exact categories of the above result is proved. The treatment combines methods of model theory and category theory. Some applications to module categories are given. (shrink)

We give a general method for producing various effective Null and Positivstellensätze, and getting new Positivstellensätze in algebraically closed valued fields and ordered groups. These various effective Nullstellensätze produce algebraic identities certifying that some geometric conditions cannot be simultaneously satisfied. We produce also constructive versions of abstract classical results of algebra based on Zorn's lemma in several cases where such constructive version did not exist. For example, the fact that a real field can be totally ordered, or the fact that (...) a field can be embedded in an algebraically closed field. Our results are based on the concepts we develop of dynamical proofs and simultaneous collapse. (shrink)

From a logical point of view, Stone duality for Boolean algebras relates theories in classical propositional logic and their collections of models. The theories can be seen as presentations of Boolean algebras, and the collections of models can be topologized in such a way that the theory can be recovered from its space of models. The situation can be cast as a formal duality relating two categories of syntax and semantics, mediated by homming into a common dualizing object, in this (...) case 2.In the present work, we generalize the entire arrangement from propositional to first-order logic, using a representation result of Butz and Moerdijk. Boolean algebras are replaced by Boolean categories presented by theories in first-order logic, and spaces of models are replaced by topological groupoids of models and their isomorphisms. A duality between the resulting categories of syntax and semantics, expressed primarily in the form of a contravariant adjunction, is established by homming into a common dualizing object, now Sets, regarded once as a boolean category, and once as a groupoid equipped with an intrinsic topology.The overall framework of our investigation is provided by topos theory. Direct proofs of the main results are given, but the specialist will recognize toposophical ideas in the background. Indeed, the duality between syntax and semantics is really a manifestation of that between algebra and geometry in the two directions of the geometric morphisms that lurk behind our formal theory. Along the way, we give an elementary proof of Butz and Moerdijkʼs result in logical terms. (shrink)