The first-order image fragment

The finitary formulas of a language L, embedded into L_{ω₁ω} by BoundedFormula.toOmega, form a fragment: a component of the image of a finitary formula is the image of a finitary formula, and the image contains no infinitary conjunction or disjunction. This fragment is formation-closed, since it contains every atomic formula and ⊥ and is closed under implication, universal quantification and relabelling of bound positions. It is the least formation-closed fragment, since every formation-closed fragment contains the image of every finitary formula. Over a language with countably many function and relation symbols it is countable, because there are countably many finitary formulas.

The first-order image is how results about countable formation-closed fragments, such as the omitting types theorem, specialize to first-order logic.

Main definitions

• FirstOrder.Language.Fragment.firstOrder: the fragment of images of finitary formulas.

Main results

• FirstOrder.Language.Fragment.mem_firstOrder_iff: the members of the first-order image are exactly the images of finitary formulas.
• FirstOrder.Language.Fragment.formationClosed_firstOrder: the first-order image is formation-closed.
• FirstOrder.Language.Fragment.FormationClosed.firstOrder_le and FirstOrder.Language.Fragment.formationClosure_empty: the first-order image lies below every formation-closed fragment, so it is the least one, the formation closure of the empty set.
• FirstOrder.Language.Fragment.firstOrder_countable: over a language with countably many function and relation symbols, the first-order image is countable.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, Chapter 1.
• The first-order image fragment also appears in cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Lomega1omega/FirstOrderImage.lean.

def FirstOrder.Language.Fragment.firstOrder (L : Language) : L.Fragment

The first-order image: the fragment of L_{ω₁ω} formulas that are images of finitary formulas under BoundedFormula.toOmega.

theorem FirstOrder.Language.Fragment.mem_firstOrder_iff {L : Language} {n : ℕ} {φ : L.BoundedFormulaω Empty n} : ⟨n, φ⟩ ∈ firstOrder L ↔ ∃ (ψ : L.BoundedFormula Empty n), ψ.toOmega = φ

A formula belongs to the first-order image exactly when it is the image of a finitary formula.

@[simp]

theorem FirstOrder.Language.Fragment.toOmega_mem_firstOrder {L : Language} {n : ℕ} (φ : L.BoundedFormula Empty n) : ⟨n, φ.toOmega⟩ ∈ firstOrder L

The image of a finitary formula belongs to the first-order image.

theorem FirstOrder.Language.Fragment.formationClosed_firstOrder {L : Language} : (firstOrder L).FormationClosed

The first-order image is formation-closed.

theorem FirstOrder.Language.Fragment.FormationClosed.toOmega_mem {L : Language} {A : L.Fragment} (hA : A.FormationClosed) {n : ℕ} (φ : L.BoundedFormula Empty n) : ⟨n, φ.toOmega⟩ ∈ A

Every formation-closed fragment contains the image of every finitary formula.

theorem FirstOrder.Language.Fragment.FormationClosed.firstOrder_le {L : Language} {A : L.Fragment} (hA : A.FormationClosed) : firstOrder L ≤ A

The first-order image lies below every formation-closed fragment.

theorem FirstOrder.Language.Fragment.formationClosure_empty {L : Language} : formationClosure ∅ = firstOrder L

The first-order image is the least formation-closed fragment: it is the formation closure of the empty set.

theorem FirstOrder.Language.Fragment.firstOrder_countable {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] : (↑(firstOrder L)).Countable

Over a language with countably many function and relation symbols, the first-order image is countable.