Uniform definability by first-order formulas with operators

Definable certifies that one well-formed formula defines a Lean predicate across a family of structures. The formula is independent of the family index, structure size, and assignment. This is the semantic interface for formula synthesis: compositional rules construct syntax and prove its formation conditions and meaning together.

The family supplies the interpretations of the operators and free relation variables. Particular logics can therefore register rules about their own semantic operations without extending this interface. A registered rule must produce a well-formed witness, rather than raw syntax alone.

Main definitions

• Definable: uniform definability across an indexed family of structures.
• Definable.of_formula: use a checked formula as a definability certificate.

Main results

• Definable.neg, Definable.conj, Definable.disj, Definable.ex, Definable.all: compositional construction of well-formed formulas.
• Definable.ofFO, Definable.equal, Definable.rel: atomic certificates.

References

• N. Immerman, Descriptive Complexity

def Cslib.Logic.FO.Operator.Definable {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} (P : (i : ι) → (α → M i) → Prop) : Prop

A single well-formed formula defines the predicate in every member of a family of structures. The existential witness is outside the quantification over structures and assignments.

theorem Cslib.Logic.FO.Operator.Definable.of_formula {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} (φ : Formula L shape Γ α) (hφ : Formula.wellFormed policy φ = true) : Definable policy M I ρ fun (i : ι) (v : α → M i) => Formula.Realize (I i) φ (fun {k : ℕ} => ρ i) v

Register an explicit well-formed formula through its semantics.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : Definable policy M I ρ P) (h : ∀ (i : ι) (v : α → M i), P i v ↔ Q i v) : Definable policy M I ρ Q

Replace a predicate by an equivalent one without changing its formula.

theorem Cslib.Logic.FO.Operator.Definable.relabel {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} {P : (i : ι) → (α → M i) → Prop} (hP : Definable policy M I ρ P) (f : α → β) : Definable policy M I ρ fun (i : ι) (v : β → M i) => P i (v ∘ f)

Relabeling free variables composes the predicate with the assignment map.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} (φ : L.Formula α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => φ.Realize v

A native first-order formula has the same meaning in the extended logic.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {P : (i : ι) → (α → M i) → Prop} (hP : Definable policy M I ρ P) : Definable policy M I ρ fun (i : ι) (v : α → M i) => ¬P i v

Negation preserves uniform definability.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : Definable policy M I ρ P) (hQ : Definable policy M I ρ Q) : Definable policy M I ρ fun (i : ι) (v : α → M i) => P i v ∧ Q i v

Conjunction combines the two defining formulas.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : Definable policy M I ρ P) (hQ : Definable policy M I ρ Q) : Definable policy M I ρ fun (i : ι) (v : α → M i) => P i v ∨ Q i v

Disjunction combines the two defining formulas.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {P Q : (i : ι) → (α → M i) → Prop} (hP : Definable policy M I ρ P) (hQ : Definable policy M I ρ Q) : Definable policy M I ρ fun (i : ι) (v : α → M i) => P i v → Q i v

Implication is a derived first-order connective.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {P : (i : ι) → M i → (α → M i) → Prop} (hP : Definable policy M I ρ fun (i : ι) (v : Option α → M i) => P i (v none) fun (a : α) => v (some a)) : Definable policy M I ρ fun (i : ι) (v : α → M i) => ∃ (x : M i), P i x v

Existential quantification is synthesized by adding one scoped first-order variable.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {P : (i : ι) → M i → (α → M i) → Prop} (hP : Definable policy M I ρ fun (i : ι) (v : Option α → M i) => P i (v none) fun (a : α) => v (some a)) : Definable policy M I ρ fun (i : ι) (v : α → M i) => ∀ (x : M i), P i x v

Universal quantification is synthesized from a defining formula with one extra variable.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} : Definable policy M I ρ fun (x : ι) (x_1 : α → M x) => True

The constant true predicate is uniformly definable, including on empty structures.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} : Definable policy M I ρ fun (x : ι) (x_1 : α → M x) => False

The constant false predicate is uniformly definable.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} (a b : L.Term α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Term.realize v a = FirstOrder.Language.Term.realize v b

Equality of two native first-order terms is uniformly definable.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} (a b : α) : Definable policy M I ρ fun (x : ι) (v : α → M x) => v a = v b

Equality of two free variables is an atomic synthesis rule.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {k : ℕ} (r : L.Relations k) (args : Fin k → L.Term α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Structure.RelMap r fun (j : Fin k) => FirstOrder.Language.Term.realize v (args j)

A base-language relation applied to native terms is uniformly definable.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {k : ℕ} (r : L.Relations k) (args : Fin k → α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Structure.RelMap r (v ∘ args)

A base-language relation applied to free variables is an atomic synthesis rule.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} (r : L.Relations 1) (a : α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Structure.RelMap r ![v a]

Unary relation application in the usual vector notation is an atomic synthesis rule.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} (r : L.Relations 2) (a b : α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => FirstOrder.Language.Structure.RelMap r ![v a, v b]

Binary relation application in the usual vector notation is an atomic synthesis rule.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {k : ℕ} (r : RelVar Γ k) (args : Fin k → L.Term α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => (fun (j : Fin k) => FirstOrder.Language.Term.realize v (args j)) ∈ ρ i r

Free relation variables are also available to formula synthesis.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} {k : ℕ} (r : RelVar Γ k) (args : Fin k → α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => v ∘ args ∈ ρ i r

A free relation variable applied to a tuple of free variables is uniformly definable.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} (r : RelVar Γ 1) (a : α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => ![v a] ∈ ρ i r

Unary free-relation application in vector notation is an atomic synthesis rule.

theorem Cslib.Logic.FO.Operator.Definable.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)} {α : Type w} (r : RelVar Γ 2) (a b : α) : Definable policy M I ρ fun (i : ι) (v : α → M i) => ![v a, v b] ∈ ρ i r

Binary free-relation application in vector notation is an atomic synthesis rule.