The first-order image inside Lω₁ω

IsFirstOrder φ says φ is toLω of an ordinary first-order formula — i.e. it contains no infinitary node.

The point of the API is the exact constructor equations, especially

• isFirstOrder_imp_iff / isFirstOrder_all_iff — structural, both directions;
• not_isFirstOrder_iInf / not_isFirstOrder_iSup — the two negative facts.

Without these, every consumer that needs "this fragment contains no infinitary formula" re-does the same cases … <;> simp [toLω] inversion. With them the HF fragment's closure fields become one-liners.

def FirstOrder.Language.BoundedFormulaω.IsFirstOrder {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) : Prop

φ is the toLω-image of a first-order formula: it has no infinitary node.

Equations

• φ.IsFirstOrder = ∃ (φ₀ : L.BoundedFormula α n), φ₀.toLω = φ

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.isFirstOrder_imp_iff {L : Language} {α : Type u'} {n : ℕ} {φ ψ : L.BoundedFormulaω α n} : (φ.imp ψ).IsFirstOrder ↔ φ.IsFirstOrder ∧ ψ.IsFirstOrder

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.isFirstOrder_all_iff {L : Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormulaω α (n + 1)} : φ.all.IsFirstOrder ↔ φ.IsFirstOrder

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.not_isFirstOrder_iInf {L : Language} {α : Type u'} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) : ¬(iInf φs).IsFirstOrder

No infinitary conjunction is first-order. This is the fact HF's closure fields need.

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.not_isFirstOrder_iSup {L : Language} {α : Type u'} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) : ¬(iSup φs).IsFirstOrder

No infinitary disjunction is first-order.