First-order logic with scoped operators

An operator has finitely many formula bodies, each with its own first-order and relation binders, and a tuple of term arguments. This separates binding from the meaning of an operator: least fixed points, tuple transitive closure, and language quantifiers share the same syntax. Ordinary terms, formulas, and structures are Mathlib's first-order objects.

Formula is raw syntax. An interpretation gives it a total meaning; an operator's formation conditions (such as positive recursion) are a separate layer. In particular, this interface does not assume that every operator is monotone or that every structure is finite or ordered.

Main definitions

• RelVar, RelEnv: scoped, arity-indexed relation variables and their valuations.
• Binder, Shape: the binding and application interface of an operator.
• Formula, Formula.Realize: common syntax and interpretation.
• Formula.relabel, Formula.realize_relabel: capture-avoiding renaming of free variables.

References

• N. Immerman, Descriptive Complexity
• Z. Ésik and K. G. Larsen, Regular Languages Definable by Lindström Quantifiers, Section 2, for multiple scoped bodies in regular-language quantifiers.

inductive Cslib.Logic.FO.Operator.RelVar : List ℕ → ℕ → Type

A relation variable whose arity is recorded in its context. The head is the nearest binder.

• here {Γ : List ℕ} {k : ℕ} : RelVar (k :: Γ) k
• there {Γ : List ℕ} {k l : ℕ} : RelVar Γ k → RelVar (l :: Γ) k

def Cslib.Logic.FO.Operator.RelVar.split {Γ : List ℕ} {k : ℕ} (Δ : List ℕ) : RelVar (Δ ++ Γ) k → RelVar Δ k ⊕ RelVar Γ k

Distinguish a locally bound relation variable from a variable in the outer context.

def Cslib.Logic.FO.Operator.RelVar.lift {Γ : List ℕ} {k : ℕ} (Δ : List ℕ) (r : RelVar Γ k) : RelVar (Δ ++ Γ) k

Lift an outer relation variable through a list of new binders.

@[simp]

theorem Cslib.Logic.FO.Operator.RelVar.split_lift {Γ : List ℕ} {k : ℕ} (Δ : List ℕ) (r : RelVar Γ k) : split Δ (lift Δ r) = Sum.inr r

Splitting a lifted variable recovers the outer variable.

@[reducible, inline]

abbrev Cslib.Logic.FO.Operator.RelEnv (Γ : List ℕ) (M : Type z) : Type z

An interpretation of all relation variables in a context.

def Cslib.Logic.FO.Operator.RelEnv.empty {M : Type z} : RelEnv [] M

The unique valuation of an empty relation context.

def Cslib.Logic.FO.Operator.RelEnv.append {Γ Δ : List ℕ} {M : Type z} (δ : RelEnv Δ M) (outer : RelEnv Γ M) : RelEnv (Δ ++ Γ) M

Extend a relation valuation by local relations, without changing the outer relations.

def Cslib.Logic.FO.Operator.RelEnv.cons {Γ : List ℕ} {M : Type z} {k : ℕ} (R : Set (Fin k → M)) (outer : RelEnv Γ M) : RelEnv (k :: Γ) M

Add one relation as the nearest binder.

@[simp]

theorem Cslib.Logic.FO.Operator.RelEnv.append_empty {Γ : List ℕ} {M : Type z} (outer : RelEnv Γ M) : (@append Γ [] M (@empty M) fun {k : ℕ} => outer) = outer

Extending by an empty context leaves a valuation unchanged.

@[simp]

theorem Cslib.Logic.FO.Operator.RelEnv.append_lift {Γ Δ : List ℕ} {M : Type z} (δ : RelEnv Δ M) (outer : RelEnv Γ M) {k : ℕ} (r : RelVar Γ k) : append (fun {k : ℕ} => δ) (fun {k : ℕ} => outer) (RelVar.lift Δ r) = outer r

Outer relation variables retain their meanings under a binder.

structure Cslib.Logic.FO.Operator.Binder : Type

The local variables available in one body of a logical operator.

• relations : List ℕ

  Arities of locally bound relation variables, nearest first.

• vars : ℕ

  Number of locally bound first-order variables.

structure Cslib.Logic.FO.Operator.Shape : Type

The finite binding interface of a logical operator.

• arity : ℕ

  Number of terms at which the operator's resulting relation is applied.

• slots : ℕ

  Number of formula bodies.

• binder : Fin self.slots → Binder

  Local binding context of each body.

@[reducible, inline]

abbrev Cslib.Logic.FO.Operator.BodyValue (b : Binder) (M : Type z) : Type z

The meaning of a body as a function of its locally bound relations and variables.

@[reducible, inline]

abbrev Cslib.Logic.FO.Operator.Interpretation {O : Type s} (shape : O → Shape) (M : Type z) : Type (max s z)

An operator interpretation. It may use additional structure on M supplied by its caller.

inductive Cslib.Logic.FO.Operator.Formula (L : FirstOrder.Language) {O : Type s} (shape : O → Shape) : List ℕ → Type w → Type (max u v (w + 1) s)

First-order syntax extended by an arbitrary family of scoped logical operators.

• ofFO {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} : L.Formula α → Formula L shape Γ α
• rel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {k : ℕ} : RelVar Γ k → (Fin k → L.Term α) → Formula L shape Γ α
• neg {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} : Formula L shape Γ α → Formula L shape Γ α
• conj {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} : Formula L shape Γ α → Formula L shape Γ α → Formula L shape Γ α
• ex {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} : Formula L shape Γ (Option α) → Formula L shape Γ α
• op {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (o : O) (body : (i : Fin (shape o).slots) → Formula L shape (((shape o).binder i).relations ++ Γ) (α ⊕ Fin ((shape o).binder i).vars)) (args : Fin (shape o).arity → L.Term α) : Formula L shape Γ α

def Cslib.Logic.FO.Operator.Formula.Realize {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {M : Type z} [L.Structure M] (I : Interpretation shape M) {Γ : List ℕ} {α : Type w} : Formula L shape Γ α → RelEnv Γ M → (α → M) → Prop

Interpret a formula, capturing the ambient free-variable assignment in every operator body.

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

Capture-avoiding relabeling of free first-order variables.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_ofFO {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ : L.Formula α) (ρ : RelEnv Γ M) (v : α → M) : Realize I (ofFO φ) (fun {k : ℕ} => ρ) v ↔ φ.Realize v

Embedded first-order formulas keep their original semantics.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_rel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) {k : ℕ} (r : RelVar Γ k) (args : Fin k → L.Term α) (ρ : RelEnv Γ M) (v : α → M) : Realize I (rel r args) (fun {k : ℕ} => ρ) v ↔ (fun (i : Fin k) => FirstOrder.Language.Term.realize v (args i)) ∈ ρ r

Relation variables are applied to the interpreted term arguments.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_neg {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ : Formula L shape Γ α) (ρ : RelEnv Γ M) (v : α → M) : Realize I φ.neg (fun {k : ℕ} => ρ) v ↔ ¬Realize I φ (fun {k : ℕ} => ρ) v

Semantic negation.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_conj {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ ψ : Formula L shape Γ α) (ρ : RelEnv Γ M) (v : α → M) : Realize I (φ.conj ψ) (fun {k : ℕ} => ρ) v ↔ Realize I φ (fun {k : ℕ} => ρ) v ∧ Realize I ψ (fun {k : ℕ} => ρ) v

Semantic conjunction.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_ex {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ : Formula L shape Γ (Option α)) (ρ : RelEnv Γ M) (v : α → M) : Realize I φ.ex (fun {k : ℕ} => ρ) v ↔ ∃ (x : M), Realize I φ (fun {k : ℕ} => ρ) fun (x_1 : Option α) => x_1.elim x v

Existential binding changes only the new variable.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_relabel {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α β : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ : Formula L shape Γ α) (f : α → β) (ρ : RelEnv Γ M) (v : β → M) : Realize I (relabel f φ) (fun {k : ℕ} => ρ) v ↔ Realize I φ (fun {k : ℕ} => ρ) (v ∘ f)

Relabeling is interpreted by precomposing the free-variable assignment.

def Cslib.Logic.FO.Operator.Formula.disj {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (φ ψ : Formula L shape Γ α) : Formula L shape Γ α

Disjunction as a derived connective.

def Cslib.Logic.FO.Operator.Formula.all {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} (φ : Formula L shape Γ (Option α)) : Formula L shape Γ α

Universal quantification as a derived connective.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_disj {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ ψ : Formula L shape Γ α) (ρ : RelEnv Γ M) (v : α → M) : Realize I (φ.disj ψ) (fun {k : ℕ} => ρ) v ↔ Realize I φ (fun {k : ℕ} => ρ) v ∨ Realize I ψ (fun {k : ℕ} => ρ) v

Derived disjunction has the usual classical semantics.

@[simp]

theorem Cslib.Logic.FO.Operator.Formula.realize_all {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] (I : Interpretation shape M) (φ : Formula L shape Γ (Option α)) (ρ : RelEnv Γ M) (v : α → M) : Realize I φ.all (fun {k : ℕ} => ρ) v ↔ ∀ (x : M), Realize I φ (fun {k : ℕ} => ρ) fun (x_1 : Option α) => x_1.elim x v

Derived universal quantification has the usual classical semantics.