Variance and formation rules for first-order operators

Operator bodies may be monotone, antitone, or arbitrary. Positivity propagates through this variance, not just through negations: an arbitrary operator (for example, a parity quantifier) must not introduce a hidden negative dependency into a least fixed point.

Formula.checkPolarity is a decidable syntactic check. Formula.realize_checkPolarity proves its semantic guarantee from the operator interpretation's variance law. Policy separately specifies which locally bound relations must occur positively; Formula.wellFormed checks this condition at every nested operator. Raw interpretation itself does not assume well-formedness.

Main definitions

• Variance, Interpretation.Respects: the semantic extension contract.
• Policy, Formula.wellFormed, CheckedFormula: formation rules and checked formulas.
• Formula.checkPolarity: syntactic dependence on a marked set of relation variables.

Main results

• Formula.realize_checkPolarity: syntactic polarity implies semantic monotonicity or antitonicity.
• Formula.wellFormed_relabel: free-variable renaming preserves formation conditions.

inductive Cslib.Logic.FO.Operator.Variance : Type

The variance of an operator in one of its body predicates.

• positive : Variance
• negative : Variance
• arbitrary : Variance

@[instance_reducible]

instance Cslib.Logic.FO.Operator.instDecidableEqVariance : DecidableEq Variance

def Cslib.Logic.FO.Operator.Variance.Relates : Variance → Prop → Prop → Prop

The pointwise relation on body predicates required by a variance annotation.

@[reducible, inline]

abbrev Cslib.Logic.FO.Operator.Marking (Γ : List ℕ) : Type

A Boolean marking of relation variables.

def Cslib.Logic.FO.Operator.Marking.outer {Γ : List ℕ} (Δ : List ℕ) (mark : Marking Γ) : Marking (Δ ++ Γ)

Mark only outer variables when passing under a binder.

def Cslib.Logic.FO.Operator.Marking.inner {Γ Δ : List ℕ} (mark : Marking Δ) : Marking (Δ ++ Γ)

Mark only the selected locally bound variables.

@[simp]

theorem Cslib.Logic.FO.Operator.Marking.outer_false {Γ : List ℕ} (Δ : List ℕ) : (@outer Γ Δ fun {x : ℕ} (x_1 : RelVar Γ x) => false) = fun {x : ℕ} (x_1 : RelVar (Δ ++ Γ) x) => false

An empty marking stays empty under any number of relation binders.

@[reducible, inline]

abbrev Cslib.Logic.FO.Operator.Variances {O : Type s} (shape : O → Shape) : Type s

The declared variance of every body of every operator.

def Cslib.Logic.FO.Operator.Interpretation.Respects {O : Type s} {shape : O → Shape} {M : Type z} (I : Interpretation shape M) (variance : Variances shape) : Prop

An interpretation obeys the declared body variances. Arbitrary bodies must be equivalent.

structure Cslib.Logic.FO.Operator.Policy {O : Type s} (shape : O → Shape) : Type s

Operator-specific formation conditions, separate from binding and interpretation.

• variance : Variances shape

  How an operator depends on each body.

• positive (o : O) (i : Fin (shape o).slots) : Marking ((shape o).binder i).relations

  Locally bound relations required to occur positively in each body.

def Cslib.Logic.FO.Operator.Formula.checkPolarity {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} (variance : Variances shape) {Γ : List ℕ} {α : Type w} : Formula L shape Γ α → Bool → Marking Γ → Bool

Check positive (true) or negative (false) dependence on the marked relations. Arbitrary operator slots require both checks, conservatively excluding marked dependencies.

def Cslib.Logic.FO.Operator.Formula.wellFormed {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} (policy : Policy shape) {Γ : List ℕ} {α : Type w} : Formula L shape Γ α → Bool

Check the local positivity requirements and recursively check all nested bodies.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.checkPolarity_false {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (variance : Variances shape) (φ : Formula L shape Γ α) (sign : Bool) : (checkPolarity variance φ sign fun {x : ℕ} (x_1 : RelVar Γ x) => false) = true

Every formula has both polarities when no relation variable is marked.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.checkPolarity_relabel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α β : Type w} (variance : Variances shape) (φ : Formula L shape Γ α) (f : α → β) (sign : Bool) (mark : Marking Γ) : (checkPolarity variance (relabel f φ) sign fun {k : ℕ} => mark) = checkPolarity variance φ sign fun {k : ℕ} => mark

A checker's result does not depend on the names of free first-order variables.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.wellFormed_relabel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α β : Type w} (policy : Policy shape) (φ : Formula L shape Γ α) (f : α → β) : wellFormed policy (relabel f φ) = wellFormed policy φ

Renaming free first-order variables preserves operator formation conditions.

@[reducible, inline]

abbrev Cslib.Logic.FO.Operator.CheckedFormula (L : FirstOrder.Language) {O : Type s} {shape : O → Shape} (policy : Policy shape) (Γ : List ℕ) (α : Type w) : Type (max 0 (max (max s u) v) (w + 1))

A formula together with its checked operator formation conditions.

def Cslib.Logic.FO.Operator.RelEnv.LeOn {Γ : List ℕ} {M : Type z} (mark : Marking Γ) (ρ σ : RelEnv Γ M) : Prop

Increase marked relations, keeping every unmarked relation fixed.

theorem Cslib.Logic.FO.Operator.RelEnv.LeOn.append {Γ Δ : List ℕ} {M : Type z} {mark : Marking Γ} {ρ σ : RelEnv Γ M} (h : LeOn (fun {k : ℕ} => mark) (fun {k : ℕ} => ρ) fun {k : ℕ} => σ) (δ : RelEnv Δ M) : LeOn (fun {k : ℕ} => Marking.outer Δ mark) (fun {k : ℕ} => δ.append fun {k : ℕ} => ρ) fun {k : ℕ} => δ.append fun {k : ℕ} => σ

Equal local valuations preserve the comparison of the outer valuations.

def Cslib.Logic.FO.Operator.Directed : Bool → Prop → Prop → Prop

The implication direction selected by a polarity.

theorem Cslib.Logic.FO.Operator.Formula.realize_checkPolarity {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] {variance : Variances shape} (I : Interpretation shape M) (hI : I.Respects variance) (φ : Formula L shape Γ α) {sign : Bool} {mark : Marking Γ} {ρ σ : RelEnv Γ M} (hφ : (checkPolarity variance φ sign fun {k : ℕ} => mark) = true) (hρ : RelEnv.LeOn (fun {k : ℕ} => mark) (fun {k : ℕ} => ρ) fun {k : ℕ} => σ) (v : α → M) : Directed sign (Realize I φ (fun {k : ℕ} => ρ) v) (Realize I φ (fun {k : ℕ} => σ) v)

The syntactic polarity check implies the corresponding semantic implication. This includes nested operators and does not assume that raw syntax is well-formed.