Documentation

LeanPool.InfinitaryLogic.Lomega1omega.QuantifierOccurrence

Signed quantifier occurrence (issue #15, budget gate 1) #

QuantifierClass.lean answers "is every quantifier of this sign admissible?"; Feferman's separator budgets need the dual, positive question: "does a quantifier of this sign occur?".

Defining occurrence as ¬ IsUniversal / ¬ IsExistential would work extensionally but makes every budget calculation a double-negation exercise. So occurrence is given its own signed recursion, with exact constructor equations, and the two are then related by an exact bridge:

universalSigned s φ ↔ ¬ hasQuantSigned (!s) φ
IsUniversal φ ↔ ¬ HasExistential φ      IsExistential φ ↔ ¬ HasUniversal φ

The sign discipline is the same as in QuantifierClass.lean and Polarity.lean: an antecedent flips, iSup/iInf preserve and are not quantifiers, and all is a universal occurrence at the positive sign only. Nothing here mentions interpolation; the set-level versions at the end are what the separator budgets are stated against.

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

Signed quantifier occurrence. hasQuantSigned true φ says a quantifier occurs universally in φ; hasQuantSigned false φ says one occurs existentially (a negatively occurring all).

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

    An existential quantifier occurs in φ.

    Equations
    Instances For

      Constructor equations #

      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_falsum {L : Language} {α : Type} {n : ℕ} (s : Bool) :
      ¬hasQuantSigned s falsum
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_equal {L : Language} {α : Type} {n : ℕ} (s : Bool) (t₁ t₂ : L.Term (α ⊕ Fin n)) :
      ¬hasQuantSigned s (equal t₁ t₂)
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_rel {L : Language} {α : Type} {n l : ℕ} (s : Bool) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
      ¬hasQuantSigned s (rel R ts)
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_imp {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) :
      hasQuantSigned s (φ.imp ψ) ↔ hasQuantSigned (!s) φ ∨ hasQuantSigned s ψ
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_all {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α (n + 1)) :
      hasQuantSigned s φ.all ↔ s = true ∨ hasQuantSigned s φ
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_iSup {L : Language} {α : Type} {n : ℕ} (s : Bool) (φs : ℕ → L.BoundedFormulaω α n) :
      hasQuantSigned s (iSup φs) ↔ ∃ (i : ℕ), hasQuantSigned s (φs i)
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_iInf {L : Language} {α : Type} {n : ℕ} (s : Bool) (φs : ℕ → L.BoundedFormulaω α n) :
      hasQuantSigned s (iInf φs) ↔ ∃ (i : ℕ), hasQuantSigned s (φs i)
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_not {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α n) :
      hasQuantSigned s φ.not ↔ hasQuantSigned (!s) φ

      Negation exchanges the two occurrence notions.

      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_and {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) :
      hasQuantSigned s (φ.and ψ) ↔ hasQuantSigned s φ ∨ hasQuantSigned s ψ
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_ex {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α (n + 1)) :
      hasQuantSigned s φ.ex ↔ s = false ∨ hasQuantSigned s φ

      The exact bridge to the quantifier classes #

      source
      theorem FirstOrder.Language.BoundedFormulaω.universalSigned_iff_not_hasQuantSigned {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α n) :
      universalSigned s φ ↔ ¬hasQuantSigned (!s) φ

      The bridge. Being of a class is exactly the absence of an occurrence of the opposite sign.

      source
      theorem FirstOrder.Language.BoundedFormulaω.isUniversal_iff_not_hasExistential {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
      φ.IsUniversal ↔ ¬φ.HasExistential

      Stability under the variable operations #

      source
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_relabel {L : Language} {α β : Type} {n : ℕ} (s : Bool) (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormulaω α k) :
      hasQuantSigned s (relabel g φ) ↔ hasQuantSigned s φ
      source
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_subst {L : Language} {α β : Type} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) (tf : α → L.Term β) :
      hasQuantSigned s (φ.subst tf) ↔ hasQuantSigned s φ
      source
      theorem FirstOrder.Language.BoundedFormulaω.hasQuantSigned_openBounds {L : Language} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω Empty n) :
      hasQuantSigned s φ.openBounds ↔ hasQuantSigned s φ

      Set-level occurrence: the budget sources #

      source
      def FirstOrder.Language.Theoryω.HasQuantSigned {L : Language} (s : Bool) (T : Set L.Sentenceω) :
      Prop

      A quantifier of sign s occurs somewhere in the set — the source of a separator budget.

      Equations
      Instances For
        source
        theorem FirstOrder.Language.Theoryω.hasQuantSigned_mono {L : Language} {s : Bool} {T T' : Set L.Sentenceω} (h : T ⊆ T') (hT : HasQuantSigned s T) :
        HasQuantSigned s T'
        source
        theorem FirstOrder.Language.Theoryω.hasQuantSigned_of_mem {L : Language} {s : Bool} {T : Set L.Sentenceω} {σ : L.Sentenceω} (hmem : σ ∈ T) (hq : BoundedFormulaω.hasQuantSigned s σ) :
        HasQuantSigned s T
        source
        @[simp]
        theorem FirstOrder.Language.Theoryω.hasQuantSigned_insert {L : Language} {s : Bool} {T : Set L.Sentenceω} {σ : L.Sentenceω} :
        HasQuantSigned s (insert σ T) ↔ BoundedFormulaω.hasQuantSigned s σ ∨ HasQuantSigned s T
        source
        theorem FirstOrder.Language.Theoryω.hasQuantSigned_insert_of_le {L : Language} {s : Bool} {T : Set L.Sentenceω} {σ : L.Sentenceω} (h : BoundedFormulaω.hasQuantSigned s σ → HasQuantSigned s T) :
        HasQuantSigned s (insert σ T) ↔ HasQuantSigned s T

        Non-growth: inserting a sentence whose s-occurrences are already licensed does not enlarge the budget. This is the shape every consistency-property branch step needs.