Documentation

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ω.HasUniversal {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
    Prop

    A universal quantifier occurs in φ.

    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_bot {L : Language} {α : Type} {n : ℕ} (s : Bool) :
        ¬hasQuantSigned s ⊥
        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_top {L : Language} {α : Type} {n : ℕ} (s : Bool) :
        ¬hasQuantSigned s ⊤
        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_or {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) :
        hasQuantSigned s (φ.or ψ) ↔ 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
        source
        theorem FirstOrder.Language.BoundedFormulaω.isExistential_iff_not_hasUniversal {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
        φ.IsExistential ↔ ¬φ.HasUniversal

        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
          @[reducible, inline]
          abbrev FirstOrder.Language.Theoryω.HasUniversal {L : Language} (T : Set L.Sentenceω) :
          Prop

          A universal quantifier occurs somewhere in T.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev FirstOrder.Language.Theoryω.HasExistential {L : Language} (T : Set L.Sentenceω) :
            Prop

            An existential quantifier occurs somewhere in T.

            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.