Formula synthesis with certified polarity

PolarityDefinable strengthens uniform definability by requiring a syntactic polarity certificate for the same defining formula. This lets a fixed-point synthesis rule construct its body from a Lean predicate while checking that recursive relation occurrences are positive. Monotonicity is never assumed in place of this syntactic check.

The compositional rules are registered in FODefinable, so fo_definable handles these goals as well as ordinary Definable goals. Negation reverses the requested polarity; marked relation atoms are available only positively. Unmarked relation atoms are available with either sign.

Main definitions

• PolarityDefinable: one well-formed, polarity-checked formula for a family of predicates.

Main results

• PolarityDefinable.toDefinable: forget the additional polarity certificate.
• PolarityDefinable.neg, PolarityDefinable.conj, PolarityDefinable.disj, PolarityDefinable.ex, PolarityDefinable.all: compositional synthesis rules.
• PolarityDefinable.head_vars: a positive recursive atom in the nearest relation binder.

def Cslib.Logic.FO.Operator.PolarityDefinable {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} (policy : Policy shape) {Γ : List ℕ} (mark : Marking Γ) (sign : Bool) {ι : Type t} (M : ι → Type z) [(i : ι) → L.Structure (M i)] (I : (i : ι) → Interpretation shape (M i)) (ρ : (i : ι) → RelEnv Γ (M i)) {α : Type w} (P : (i : ι) → (α → M i) → Prop) : Prop

Uniform definability with a syntactic polarity check on the defining formula itself.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.toDefinable {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P : (i : ι) → (α → M i) → Prop} (h : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ P) : Definable policy M I ρ P

Forget the polarity requirement while retaining the well-formed defining formula.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.congr {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ P) (h : ∀ (i : ι) (v : α → M i), P i v ↔ Q i v) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ Q

Equivalent semantic presentations use the same syntax and polarity certificate.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.ofFO {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} (φ : L.Formula α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => φ.Realize v

Native first-order formulas are independent of all scoped relation variables.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.neg {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P : (i : ι) → (α → M i) → Prop} (hP : PolarityDefinable policy (fun {k : ℕ} => mark) (!sign) M I ρ P) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => ¬P i v

Negation reverses the required polarity of its body.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.conj {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ P) (hQ : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ Q) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => P i v ∧ Q i v

Conjunction preserves the polarity of both bodies.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.disj {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ P) (hQ : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ Q) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => P i v ∨ Q i v

Derived disjunction preserves the polarity of both bodies.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.imp {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : PolarityDefinable policy (fun {k : ℕ} => mark) (!sign) M I ρ P) (hQ : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ Q) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => P i v → Q i v

Implication reverses polarity in its antecedent and preserves it in its consequent.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.ex {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P : (i : ι) → M i → (α → M i) → Prop} (hP : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : Option α → M i) => P i (v none) fun (a : α) => v (some a)) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => ∃ (x : M i), P i x v

Existential quantification preserves polarity while binding a fresh first-order variable.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.all {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {P : (i : ι) → M i → (α → M i) → Prop} (hP : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : Option α → M i) => P i (v none) fun (a : α) => v (some a)) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => ∀ (x : M i), P i x v

Universal quantification preserves polarity while binding a fresh first-order variable.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.truth {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (x : ι) (x_1 : α → M x) => True

The constant true predicate has either polarity.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.falsity {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (x : ι) (x_1 : α → M x) => False

The constant false predicate has either polarity.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.equal {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} (a b : L.Term α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Term.realize v a = FirstOrder.Language.Term.realize v b

Equality of native terms has either polarity.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.var_eq {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} (a b : α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (x : ι) (v : α → M x) => v a = v b

Equality of variables is an atomic polarity-aware synthesis rule.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.relation {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {k : ℕ} (r : L.Relations k) (args : Fin k → L.Term α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Structure.RelMap r fun (j : Fin k) => FirstOrder.Language.Term.realize v (args j)

Native vocabulary relations have either polarity in scoped relation variables.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.relation_vars {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {k : ℕ} (r : L.Relations k) (args : Fin k → α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Structure.RelMap r (v ∘ args)

Native vocabulary relations applied to variable tuples have either polarity.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.relation₂ {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} (r : L.Relations 2) (a b : α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Structure.RelMap r ![v a, v b]

Binary vocabulary relations in vector notation are atomic synthesis rules.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.rel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {α : Type w} {k : ℕ} (r : RelVar Γ k) (args : Fin k → L.Term α) : PolarityDefinable policy (fun {k : ℕ} => mark) true M I ρ fun (i : ι) (v : α → M i) => (fun (j : Fin k) => FirstOrder.Language.Term.realize v (args j)) ∈ ρ i r

A scoped relation atom is positive in every marked relation.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.rel_unmarked {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {k : ℕ} (r : RelVar Γ k) (hm : mark r = false) (args : Fin k → L.Term α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => (fun (j : Fin k) => FirstOrder.Language.Term.realize v (args j)) ∈ ρ i r

An unmarked relation atom has either polarity.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.rel_vars {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {α : Type w} {k : ℕ} (r : RelVar Γ k) (args : Fin k → α) : PolarityDefinable policy (fun {k : ℕ} => mark) true M I ρ fun (i : ι) (v : α → M i) => v ∘ args ∈ ρ i r

Variable arguments give the usual positive relation application.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.rel_vars_unmarked {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {mark : Marking Γ} {sign : Bool} {α : Type w} {k : ℕ} (r : RelVar Γ k) (hm : mark r = false) (args : Fin k → α) : PolarityDefinable policy (fun {k : ℕ} => mark) sign M I ρ fun (i : ι) (v : α → M i) => v ∘ args ∈ ρ i r

Unmarked relation variables can be applied to variables at either polarity.

theorem Cslib.Logic.FO.Operator.PolarityDefinable.head_vars {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {policy : Policy shape} {ι : Type t} {M : ι → Type z} [(i : ι) → L.Structure (M i)] {I : (i : ι) → Interpretation shape (M i)} {Γ : List ℕ} {ρ : (i : ι) → RelEnv Γ (M i)} {α : Type w} {k : ℕ} (mark : Marking (k :: Γ)) (R : (i : ι) → Set (Fin k → M i)) (args : Fin k → α) : PolarityDefinable policy (fun {k : ℕ} => mark) true M I (fun (i : ι) {k_1 : ℕ} => RelEnv.cons (R i) fun {k : ℕ} => ρ i) fun (i : ι) (v : α → M i) => v ∘ args ∈ R i

Direct membership in the nearest bound relation is a positive atom. This form lets synthesis start from the ordinary relation predicate, without reconstructing a relation index.