An Omitting Types Theorem for Sheaves over Topological Spaces
Andreas B. M. Brunner, Francisco Miraglia · Logic Journal of IGPL · 2004
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⃗ψ(x⃗, y⃗), where ψ is in L♯. Our main result (Theorem 5.2) is an intuitionistic generalization of the classical Omitting Types Theorem, as follows. Let Σ be a consistent set of sentences in ∀L♯ and Γ(ν1, …, νn) 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.