Projecting finite sets of instances

A finite set of instances of members of a formation-closed fragment defines a formula of the fragment in any prescribed tuple of constants. The other constants are existentially quantified. The tuple need not be injective: equalities between its coordinates ensure that a realizing tuple extends to a consistent interpretation of the constants. This is the finite-parameter elimination used to refute non-isolated types in the omitting types theorem.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, Chapter 4.

theorem FirstOrder.Language.Fragment.FormationClosed.exists_formula_iff_exists_constants {L : Language} {A : L.Fragment} {γ : Type wγ} (hA : A.FormationClosed) {σ : (L.withConstants γ).Theoryω} (hσ : Set.Finite σ) (hσA : σ ⊆ A.instances γ) {n : ℕ} (c : Fin n → γ) : ∃ (φ : L.BoundedFormulaω Empty n), ⟨n, φ⟩ ∈ A ∧ ∀ (M : Type w) [inst : L.Structure M] [Nonempty M] (a : Fin n → M), BoundedFormulaInf.Realize φ Empty.elim a ↔ ∃ (e : γ → M), e ∘ c = a ∧ σ.Model M

A finite set of instances can be projected onto any tuple of constants by a formula in the fragment. In every nonempty structure, this formula holds at a exactly when the constants can be interpreted so that the prescribed tuple has value a and all the instances hold. Repeated constants in the prescribed tuple are allowed.