Working in a fixed Grothendieck topos Sh(C, J C ) we generalize \({\mathcal{L}_{{\infty},\omega}}\) to allow our languages and formulas to make explicit reference to Sh(C, J C ). We likewise generalize the notion of model. We then show how to encode these generalized structures by models of a related sentence of \({\mathcal{L}_{{\infty},\omega}}\) in the category of sets and functions. Using this encoding we prove analogs of several results concerning \({\mathcal{L}_{{\infty},\omega}}\) , such as the downward Löwenheim–Skolem theorem, the completeness theorem and (...) Barwise compactness. (shrink)

The topos theory gives tools for unified proofs of theorems for model theory for various semantics and logics. We introduce the notion of power and the notion of generalized quantifier in topos and we formulate sufficient condition for such quantifiers in order that they fulfil downward Skolem-Löwenheim theorem when added to the language. In the next paper, in print, we will show that this sufficient condition is fulfilled in a vast class of Grothendieck toposes for the general and the existential (...) quantifiers. (shrink)

Let L be a countable first-order language with equality, let L♯ be the fragment consisting of the formulas constructed using the propositional connectives and the existential quantifier and let ∀L♯ be the set of formulas of the type ∀x⃗ψ, where ψ is in L♯. Our main result is an intuitionistic generalization of the classical Omitting Types Theorem, as follows. Let Σ be a consistent set of sentences in ∀L♯ and Γ be a set of formulas in L♯, intuitionisticaly consistent with (...) Σ. If Σ locally omits Γ, there is a spectral space Z and a separable sheaf of L-structures over Z, A, such that A is an intuitionistic model of Σ omitting Γ, and the set of stalks of A that are classical models of Σ and omit Γ is dense in Z. (shrink)