Documentation

LeanPool.InfinitaryLogic.Lomega1omega.QuantifierClass

The universal and existential quantifier classes (issue #15, Unit 0) #

The ∀₁/∃₁ classes of Harrison-Trainor–Kretschmer §2 (their hierarchy for counting quantifier alternations in infinitary formulas), realized as a signed quantifier traversal on the existing syntax:

One Bool-parameterised recursion carries both classes, so their mutual dependence through negation is definitional rather than a second induction — the same design as Lomega1omega/Polarity.lean, and, as there, no negation-normal form is constructed anywhere.

This module is deliberately neutral: it depends only on the syntax layer and is intended to be reused by any preservation theorem (issue #15's interpolation and relative preservation, and issue #16's end extensions), not to live inside the interpolation development.

source
def FirstOrder.Language.BoundedFormulaω.universalSigned {L : Language} {α : Type} {n : ℕ} :
Bool → L.BoundedFormulaω α n → Prop

The signed quantifier class. universalSigned true φ says φ is universal (∀₁) and universalSigned false φ says φ is existential (∃₁). An antecedent flips the sign, the countable connectives preserve it, and all is admissible only at the universal sign.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev FirstOrder.Language.BoundedFormulaω.IsUniversal {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
    Prop

    φ is universal (∀₁): every quantifier occurrence is a positive ∀.

    Equations
    Instances For

      Constructor equations #

      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_falsum {L : Language} {α : Type} {n : ℕ} (s : Bool) :
      universalSigned s falsum
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_equal {L : Language} {α : Type} {n : ℕ} (s : Bool) (t₁ t₂ : L.Term (α ⊕ Fin n)) :
      universalSigned s (equal t₁ t₂)
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_rel {L : Language} {α : Type} {n l : ℕ} (s : Bool) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
      universalSigned s (rel R ts)
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_imp {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) :
      universalSigned s (φ.imp ψ) ↔ universalSigned (!s) φ ∧ universalSigned s ψ
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_all {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α (n + 1)) :
      universalSigned s φ.all ↔ s = true ∧ universalSigned s φ
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_iSup {L : Language} {α : Type} {n : ℕ} (s : Bool) (φs : ℕ → L.BoundedFormulaω α n) :
      universalSigned s (iSup φs) ↔ ∀ (i : ℕ), universalSigned s (φs i)
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_iInf {L : Language} {α : Type} {n : ℕ} (s : Bool) (φs : ℕ → L.BoundedFormulaω α n) :
      universalSigned s (iInf φs) ↔ ∀ (i : ℕ), universalSigned s (φs i)

      The acceptance equations #

      The derived connectives #

      Stability under the variable operations #

      source
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_mapLanguage {L : Language} {α : Type} {L' : Language} (g : L →ᴸ L') (s : Bool) {k : ℕ} (φ : L.BoundedFormulaω α k) :
      universalSigned s (mapLanguage g φ) ↔ universalSigned s φ

      Quantifier class is invariant under language maps. mapLanguage rewrites terms and symbol tags only; every quantifier node is preserved, so the signed universal class is exact.

      source
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_relabel {L : Language} {α β : Type} {n : ℕ} (s : Bool) (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormulaω α k) :
      universalSigned s (relabel g φ) ↔ universalSigned s φ
      source
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_subst {L : Language} {α β : Type} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) (tf : α → L.Term β) :
      universalSigned s (φ.subst tf) ↔ universalSigned s φ