Given a regular cardinal $\kappa $ such that $\kappa ^{<\kappa }=\kappa $, we study a class of toposes with enough points, the $\kappa $ -separable toposes. These are equivalent to sheaf toposes over a site with $\kappa $ -small limits that has at most $\kappa $ many objects and morphisms, the topology being generated by at most $\kappa $ many covering families, and that satisfy a further exactness property T. We prove that these toposes have enough $\kappa $ -points, that (...) is, points whose inverse image preserve all $\kappa $ -small limits. This generalizes the separable toposes of Makkai and Reyes, that are a particular case when $\kappa =\omega $, when property T is trivially satisfied. This result is essentially a completeness theorem for a certain infinitary logic that we call $\kappa $ -geometric, where conjunctions of less than $\kappa $ formulas and existential quantification on less than $\kappa $ many variables is allowed. We prove that $\kappa $ -geometric theories have a $\kappa $ -classifying topos having property T, the universal property being that models of the theory in a Grothendieck topos with property T correspond to $\kappa $ -geometric morphisms into that topos. Moreover, we prove that $\kappa $ -separable toposes occur as the $\kappa $ -classifying toposes of $\kappa $ -geometric theories of at most $\kappa $ many axioms in canonical form, and that every such $\kappa $ -classifying topos is $\kappa $ -separable. Finally, we consider the case when $\kappa $ is weakly compact and study the $\kappa $ -classifying topos of a $\kappa $ -coherent theory, that is, a theory where only disjunction of less than $\kappa $ formulas are allowed, obtaining a version of Deligne’s theorem for $\kappa $ -coherent toposes from which we can derive, among other things, Karp’s completeness theorem for infinitary classical logic. (shrink)

In this paper we study the logic $\mathcal{L}^\lambda_{\omega\omega}$, which is first-order logic extended by quantification over functions . We give the syntax of the logic as well as the semantics in Heyting categories with exponentials. Embedding the generic model of a theory into a Grothendieck topos yields completeness of $\mathcal{L}^\lambda_{\omega\omega}$ with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting-valued models. The logic $\mathcal{L}^\lambda_{\omega\omega}$ is the strongest for which Heyting-valued completeness is known. Finally, (...) we relate the logic to locally connected geometric morphisms between toposes. (shrink)

We establish a criterion for deciding whether a class of structures is the class of models of a geometric theory inside Grothendieck toposes; then we specialize this result to obtain a characterization of the infinitary first-order theories which are geometric in terms of their models in Grothendieck toposes, solving a problem posed by Ieke Moerdijk in 1989.

We use the language of categorical logic to construct generic saturated models of intuitionistic theories. Our main technique is the thorough study of the filter construction on categories with finite limits, which is the completion of subobject lattices under filtered meets. When restricted to coherent or Heyting categories, classifying categories of intuitionistic first-order theories, the resulting categories are filtered meet coherent categories, coherent categories with complete subobject lattices such that both finite disjunctions and existential quantification distribute over filtered meets. Such (...) categories naturally embed into Grothendieck toposes which then contain saturated models of the theory we started with. (shrink)

In this paper we study the logic , which is first-order logic extended by quantification over functions (but not over relations). We give the syntax of the logic as well as the semantics in Heyting categories with exponentials. Embedding the generic model of a theory into a Grothendieck topos yields completeness of with respect to models in Grothendieck toposes, which can be sharpened to completeness with respect to Heyting-valued models. The logic is the strongest for which Heyting-valued completeness is known. (...) Finally, we relate the logic to locally connected geometric morphisms between toposes. (shrink)

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

Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy (...) conservativity over HA. The analysis also shows that nonstandard HA has neither the disjunction property nor the explicit definability property. Finally, careful attention to the complexity of our definitions allows us to show that a certain weak fragment of intuitionistic nonstandard arithmetic is conservative over primitive recursive arithmetic. (shrink)

5.5. Every topos is linguistic: the equivalence theorem.