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:

• atomic formulas lie in both classes (they have no quantifier);
• an antecedent flips the class — ¬φ is universal exactly when φ is existential;
• countable conjunctions and disjunctions preserve the class and are not counted as quantifiers (the source's clause 3, which is what distinguishes ∀n/∃n from Πn/Σn);
• ∀ is universal only: in this syntax ex φ = (φ.not.all).not, so an existential quantifier is an all occurring negatively.

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.

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

• FirstOrder.Language.BoundedFormulaω.universalSigned x✝ FirstOrder.Language.BoundedFormulaω.falsum = True
• FirstOrder.Language.BoundedFormulaω.universalSigned x✝ (FirstOrder.Language.BoundedFormulaω.equal t₁ t₂) = True
• FirstOrder.Language.BoundedFormulaω.universalSigned x✝ (FirstOrder.Language.BoundedFormulaω.rel R ts) = True
• FirstOrder.Language.BoundedFormulaω.universalSigned x✝ (φ.imp ψ) = (FirstOrder.Language.BoundedFormulaω.universalSigned (!x✝) φ ∧ FirstOrder.Language.BoundedFormulaω.universalSigned x✝ ψ)
• FirstOrder.Language.BoundedFormulaω.universalSigned x✝ φ.all = (x✝ = true ∧ FirstOrder.Language.BoundedFormulaω.universalSigned x✝ φ)
• FirstOrder.Language.BoundedFormulaω.universalSigned x✝ (FirstOrder.Language.BoundedFormulaω.iSup φs) = ∀ (i : ℕ), FirstOrder.Language.BoundedFormulaω.universalSigned x✝ (φs i)
• FirstOrder.Language.BoundedFormulaω.universalSigned x✝ (FirstOrder.Language.BoundedFormulaω.iInf φs) = ∀ (i : ℕ), FirstOrder.Language.BoundedFormulaω.universalSigned x✝ (φs i)

@[reducible, inline]

abbrev FirstOrder.Language.BoundedFormulaω.IsUniversal {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : Prop

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

Equations

• φ.IsUniversal = FirstOrder.Language.BoundedFormulaω.universalSigned true φ

@[reducible, inline]

abbrev FirstOrder.Language.BoundedFormulaω.IsExistential {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : Prop

φ is existential (∃₁): no quantifier occurrence is a positive ∀, i.e. every one is an existential.

Equations

• φ.IsExistential = FirstOrder.Language.BoundedFormulaω.universalSigned false φ

Constructor equations

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_falsum {L : Language} {α : Type} {n : ℕ} (s : Bool) : universalSigned s falsum

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_bot {L : Language} {α : Type} {n : ℕ} (s : Bool) : universalSigned s ⊥

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_equal {L : Language} {α : Type} {n : ℕ} (s : Bool) (t₁ t₂ : L.Term (α ⊕ Fin n)) : universalSigned s (equal t₁ t₂)

@[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)

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_imp {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) : universalSigned s (φ.imp ψ) ↔ universalSigned (!s) φ ∧ universalSigned s ψ

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_all {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α (n + 1)) : universalSigned s φ.all ↔ s = true ∧ universalSigned s φ

@[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)

@[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

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_not {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α n) : universalSigned s φ.not ↔ universalSigned (!s) φ

Negation exchanges the two classes.

theorem FirstOrder.Language.BoundedFormulaω.isUniversal_imp {L : Language} {α : Type} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : (φ.imp ψ).IsUniversal ↔ φ.IsExistential ∧ ψ.IsUniversal

theorem FirstOrder.Language.BoundedFormulaω.isExistential_imp {L : Language} {α : Type} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : (φ.imp ψ).IsExistential ↔ φ.IsUniversal ∧ ψ.IsExistential

theorem FirstOrder.Language.BoundedFormulaω.isUniversal_not {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.not.IsUniversal ↔ φ.IsExistential

theorem FirstOrder.Language.BoundedFormulaω.isExistential_not {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.not.IsExistential ↔ φ.IsUniversal

theorem FirstOrder.Language.BoundedFormulaω.isUniversal_all {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : φ.all.IsUniversal ↔ φ.IsUniversal

theorem FirstOrder.Language.BoundedFormulaω.not_isExistential_all {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : ¬φ.all.IsExistential

theorem FirstOrder.Language.BoundedFormulaω.isExistential_ex {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : φ.ex.IsExistential ↔ φ.IsExistential

Dually to not_isExistential_all: an existential quantifier is a negative all, so ∃x φ is existential exactly when φ is, and never universal (unless it is vacuous, which this syntax does not distinguish).

theorem FirstOrder.Language.BoundedFormulaω.not_isUniversal_ex {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : ¬φ.ex.IsUniversal

The derived connectives

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_top {L : Language} {α : Type} {n : ℕ} (s : Bool) : universalSigned s ⊤

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_and {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) : universalSigned s (φ.and ψ) ↔ universalSigned s φ ∧ universalSigned s ψ

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_or {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) : universalSigned s (φ.or ψ) ↔ universalSigned s φ ∧ universalSigned s ψ

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_einf {L : Language} {α : Type} {ι : Type u_1} [Encodable ι] {n : ℕ} (s : Bool) (φs : ι → L.BoundedFormulaω α n) (h : ∀ (i : ι), universalSigned s (φs i)) : universalSigned s (einf φs)

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_esup {L : Language} {α : Type} {ι : Type u_1} [Encodable ι] {n : ℕ} (s : Bool) (φs : ι → L.BoundedFormulaω α n) (h : ∀ (i : ι), universalSigned s (φs i)) : universalSigned s (esup φs)

Stability under the variable operations

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_castLE {L : Language} {α : Type} (s : Bool) {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaω α m) : universalSigned s (castLE h φ) ↔ universalSigned s φ

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.

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 φ

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_subst {L : Language} {α β : Type} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) (tf : α → L.Term β) : universalSigned s (φ.subst tf) ↔ universalSigned s φ