Documentation

CslibFrontier.Logics.FirstOrder.Operator.Quantifiers

Blocks of quantifiers in operator formulas #

Formula.exs binds a finite tuple of fresh first-order variables. Its semantics, formation check, and polarity check reduce to those of its body. This supplies the quantifier blocks needed when pulling fixed-point formulas back along tuple interpretations.

source
def Cslib.Logic.FO.Operator.Formula.exs {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (n : ℕ) :
Formula L shape Γ (α ⊕ Fin n) → Formula L shape Γ α

Bind all variables in the right summand, in increasing coordinate order.

Instances For
    source
    @[simp]
    theorem Cslib.Logic.FO.Operator.Formula.realize_exs {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (n : ℕ) (φ : Formula L shape Γ (α ⊕ Fin n)) (ρ : RelEnv Γ M) (v : α → M) :
    Realize I (exs n φ) (fun {k : ℕ} => ρ) v ↔ ∃ (xs : Fin n → M), Realize I φ (fun {k : ℕ} => ρ) (Sum.elim v xs)

    A block of existential quantifiers chooses one complete tuple.

    source
    @[simp]
    theorem Cslib.Logic.FO.Operator.Formula.wellFormed_exs {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (policy : Policy shape) (n : ℕ) (φ : Formula L shape Γ (α ⊕ Fin n)) :
    wellFormed policy (exs n φ) = wellFormed policy φ

    Quantifying a tuple leaves the formation check unchanged.

    source
    @[simp]
    theorem Cslib.Logic.FO.Operator.Formula.checkPolarity_exs {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (variance : Variances shape) (n : ℕ) (φ : Formula L shape Γ (α ⊕ Fin n)) (sign : Bool) (mark : Marking Γ) :
    (checkPolarity variance (exs n φ) sign fun {k : ℕ} => mark) = checkPolarity variance φ sign fun {k : ℕ} => mark

    Quantifying a tuple leaves dependence on scoped relations unchanged.