Documentation

LeanPool.InfinitaryLogic.Lomega1omega.Polarity

Polarity of relation-symbol occurrences (issue #14, Unit 0 layer 1) #

The signed occurrence traversal underlying Lyndon interpolation: relationsInSigned s φ collects the relation symbols occurring in φ with sign s, where

positiveRelationsIn and negativeRelationsIn are the two instances. Negation needs no clause of its own: φ.not = φ.imp ⊥, so the swap laws positiveRelationsIn φ.not = negativeRelationsIn φ and its dual fall out of the imp clause, and the same computation gives and, or, ex, ⊤, einf, esup.

This file is deliberately syntax only and sits in the Lomega1omega layer: it mentions no occurrence machinery from Methods/ (in particular not relationsIn, baseRelationsIn, or the constant-expansion calculus). The bridge relationsIn = positive ∪ negative and the signed twins of the Methods-level calculus live in Methods/PolarityCalculus.lean.

Simp discipline #

Only the generic relationsInSigned equations are @[simp]; the positiveRelationsIn / negativeRelationsIn forms are reducible abbreviations of those, so no derived rewrite is installed alongside them and nothing can loop through not, and, or, or ex.

source
def FirstOrder.Language.BoundedFormulaω.relationsInSigned {L : Language} {α : Type} {n : ℕ} :
Bool → L.BoundedFormulaω α n → Set ((n : ℕ) × L.Relations n)

The signed occurrence traversal. relationsInSigned true φ is the set of relation symbols with a positive occurrence in φ, and relationsInSigned false φ those with a negative occurrence: antecedents flip the sign, quantifiers and the countable connectives preserve it, and equality contributes nothing.

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

    The relation symbols occurring positively in φ.

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

      The relation symbols occurring negatively in φ.

      Equations
      Instances For

        Constructor equations #

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_falsum {L : Language} {α : Type} {n : ℕ} (s : Bool) :
        relationsInSigned s falsum = ∅
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_equal {L : Language} {α : Type} {n : ℕ} (s : Bool) (t₁ t₂ : L.Term (α ⊕ Fin n)) :
        relationsInSigned s (equal t₁ t₂) = ∅
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_rel {L : Language} {α : Type} {n l : ℕ} (s : Bool) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
        relationsInSigned s (rel R ts) = if s = true then {⟨l, R⟩} else ∅
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_imp {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) :
        relationsInSigned s (φ.imp ψ) = relationsInSigned (!s) φ ∪ relationsInSigned s ψ
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_all {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α (n + 1)) :
        relationsInSigned s φ.all = relationsInSigned s φ
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_iSup {L : Language} {α : Type} {n : ℕ} (s : Bool) (φs : ℕ → L.BoundedFormulaω α n) :
        relationsInSigned s (iSup φs) = ⋃ (i : ℕ), relationsInSigned s (φs i)
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_iInf {L : Language} {α : Type} {n : ℕ} (s : Bool) (φs : ℕ → L.BoundedFormulaω α n) :
        relationsInSigned s (iInf φs) = ⋃ (i : ℕ), relationsInSigned s (φs i)

        Negation swaps and the derived connectives #

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_not {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α n) :
        relationsInSigned s φ.not = relationsInSigned (!s) φ

        Negation swaps the signs (the acceptance gate, generic form).

        source
        theorem FirstOrder.Language.BoundedFormulaω.positiveRelationsIn_not {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
        φ.not.positiveRelationsIn = φ.negativeRelationsIn

        Acceptance gate: positive occurrences of ¬φ are the negative occurrences of φ.

        source
        theorem FirstOrder.Language.BoundedFormulaω.negativeRelationsIn_not {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :
        φ.not.negativeRelationsIn = φ.positiveRelationsIn

        Acceptance gate: negative occurrences of ¬φ are the positive occurrences of φ.

        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_top {L : Language} {α : Type} {n : ℕ} (s : Bool) :
        relationsInSigned s ⊤ = ∅
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_and {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ ψ : L.BoundedFormulaω α n) :
        relationsInSigned s (φ.and ψ) = relationsInSigned s φ ∪ relationsInSigned s ψ
        source
        @[simp]
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_ex {L : Language} {α : Type} {n : ℕ} (s : Bool) (φ : L.BoundedFormulaω α (n + 1)) :
        relationsInSigned s φ.ex = relationsInSigned s φ

        Existential quantification preserves the signs (two flips cancel).

        source
        theorem FirstOrder.Language.BoundedFormulaω.relationsInSigned_einf {L : Language} {α : Type} {ι : Type u_1} [Encodable ι] {n : ℕ} (s : Bool) (φs : ι → L.BoundedFormulaω α n) :
        relationsInSigned s (einf φs) = ⋃ (i : ι), relationsInSigned s (φs i)

        An Encodable-indexed conjunction collects the branches' signed occurrences (the ⊤ padding of undecodable indices contributes nothing).

        Countability #