Abstract

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