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)

Given a regular cardinal κ such that κ<κ=κ (e.g., if the generalized continuum hypothesis holds), we develop a proof system for classical infinitary logic that includes heterogeneous quantification (i.e., infinite alternating sequences of quantifiers) within the language Lκ+,κ, where there are conjunctions and disjunctions of at most κ many formulas and quantification (including the heterogeneous one) is applied to less than κ many variables. This type of quantification is interpreted in Set using the usual second-order formulation in terms of strategies (...) for games, and the axioms are based on a stronger variant of the axiom of determinacy for game semantics. With respect to this axiom system we prove the soundness and completeness theorem with respect to a class of set-valued structures that we call well determined. We also investigate intuitionistic systems with heterogeneous quantifiers for Lκ+,κ,κ (when only conjunctions of less than κ many formulas are allowed), and prove analogously a completeness theorem with respect to well-determined structures in categories in general, in κ-Grothendieck topoi in particular, and, when κ<κ=κ, also in Kripke models. Finally, we consider an extension of our system in which heterogeneous quantification with bounded quantifiers is expressible, and extend our completeness results to that case. (shrink)