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)
:
φ is the toLω-image of a first-order formula: it has no infinitary node.
Equations
- φ.IsFirstOrder = ∃ (φ₀ : L.BoundedFormula α n), φ₀.toLω = φ
Instances For
@[simp]
theorem
FirstOrder.Language.BoundedFormulaω.isFirstOrder_falsum
{L : Language}
{α : Type u'}
{n : ℕ}
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaω.isFirstOrder_equal
{L : Language}
{α : Type u'}
{n : ℕ}
(t₁ t₂ : L.Term (α ⊕ Fin n))
:
(equal t₁ t₂).IsFirstOrder
@[simp]
theorem
FirstOrder.Language.BoundedFormulaω.isFirstOrder_imp_iff
{L : Language}
{α : Type u'}
{n : ℕ}
{φ ψ : L.BoundedFormulaω α n}
:
@[simp]
theorem
FirstOrder.Language.BoundedFormulaω.isFirstOrder_all_iff
{L : Language}
{α : Type u'}
{n : ℕ}
{φ : L.BoundedFormulaω α (n + 1)}
:
@[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.