Dialogues are turn-taking games which model debates about the satisfaction of logical formulas. A novel variant played over first-order structures gives rise to a notion of first-order satisfaction. We study the induced notion of validity for classical and intuitionistic first-order logic in the constructive setting of the calculus of inductive constructions. We prove that such material dialogue semantics for classical first-order logic admits constructive soundness and completeness proofs, setting it apart from standard model-theoretic semantics of first-order logic. Furthermore, we prove that completeness with regard to intuitionistic material dialogues fails in both constructive and classical settings. As an alternative, we propose material dialogues played over Kripke structures. These Kripke material dialogues exhibit constructive completeness when restricting to the negative fragment. The results concerning classical material dialogues have been mechanized using the Coq interactive theorem prover.

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