First-order formula and sentence combinators

This file provides reusable first-order formula and sentence combinators over FirstOrder.Language:

• universal and existential closure (FO.closeAll, FO.closeEx) over finite free-variable types,
• variable relabeling, equality, and unary/binary relation application (FO.atVar, FO.varEq, FO.rel₁, FO.rel₂),
• order-theoretic formulas (FO.lt, FO.le, FO.isZero, FO.isMax, FO.succ, FO.isFirstOut) with respect to a binary relation symbol interpreted as < on Fin B, and
• finite-domain cardinality sentences (FO.cardEqSentence, built from Sentence.cardGe) and finite Boolean combinations of sentences (FO.truthTableSentence).

Main definitions

• Cslib.Logic.FO.closeAll, Cslib.Logic.FO.closeEx: universal and existential closure of a first-order formula over a finite type of free variables.
• Cslib.Logic.FO.atVar, Cslib.Logic.FO.varEq, Cslib.Logic.FO.rel₁, Cslib.Logic.FO.rel₂: atomic formula combinators.
• Cslib.Logic.FO.lt, Cslib.Logic.FO.le, Cslib.Logic.FO.isZero, Cslib.Logic.FO.isMax, Cslib.Logic.FO.succ, Cslib.Logic.FO.isFirstOut: order formulas on Fin B.
• Cslib.Logic.FO.cardEqSentence: sentence asserting Nat.card M = n on finite structures.
• Cslib.Logic.FO.truthTableSentence: finite Boolean combination of sentences indexed by Fin m.

Main results

• Cslib.Logic.FO.realize_closeAll, Cslib.Logic.FO.realize_closeEx: satisfaction of universal and existential closures.
• Cslib.Logic.FO.realize_isZero, Cslib.Logic.FO.realize_isMax, Cslib.Logic.FO.realize_succ, Cslib.Logic.FO.realize_isFirstOut: satisfaction of order formulas on Fin B.
• Cslib.Logic.FO.realize_cardGe_iff_le_card, Cslib.Logic.FO.realize_cardEqSentence: characterizations of Sentence.cardGe and cardEqSentence via Nat.card on finite structures.
• Cslib.Logic.FO.realize_truthTableSentence: satisfaction of truthTableSentence.
• Cslib.Logic.FO.relMap_pair_equiv, Cslib.Logic.FO.relMap_single_equiv: isomorphisms preserve binary and unary relations.

References

• R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets
• N. Immerman, Descriptive Complexity

Closure and atomic combinators

noncomputable def Cslib.Logic.FO.closeAll {L : FirstOrder.Language} (V : Type) [Finite V] (φ : L.Formula V) : L.Sentence

Universal closure of a formula over a finite type of free variables.

noncomputable def Cslib.Logic.FO.closeEx {L : FirstOrder.Language} (V : Type) [Finite V] (φ : L.Formula V) : L.Sentence

Existential closure of a formula over a finite type of free variables.

@[simp]

theorem Cslib.Logic.FO.realize_closeAll {L : FirstOrder.Language} {M : Type w} [L.Structure M] (V : Type) [Finite V] (φ : L.Formula V) : M ⊨ closeAll V φ ↔ ∀ (v : V → M), φ.Realize v

The universal closure holds exactly when the formula holds under every assignment of its free variables.

@[simp]

theorem Cslib.Logic.FO.realize_closeEx {L : FirstOrder.Language} {M : Type w} [L.Structure M] (V : Type) [Finite V] (φ : L.Formula V) : M ⊨ closeEx V φ ↔ ∃ (v : V → M), φ.Realize v

The existential closure holds exactly when the formula holds under some assignment of its free variables.

def Cslib.Logic.FO.atVar {L : FirstOrder.Language} (φ : L.Formula (Fin 1)) {V : Type u_1} (u : V) : L.Formula V

Relabel a single-variable formula φ : L.Formula (Fin 1) to free variable u : V.

@[simp]

theorem Cslib.Logic.FO.realize_atVar {L : FirstOrder.Language} {M : Type w} [L.Structure M] (φ : L.Formula (Fin 1)) {V : Type u_1} (v : V → M) (u : V) : (atVar φ u).Realize v ↔ φ.Realize ![v u]

def Cslib.Logic.FO.varEq {L : FirstOrder.Language} {V : Type u_1} (u w : V) : L.Formula V

Equality of two free variables as a formula.

def Cslib.Logic.FO.rel₁ {L : FirstOrder.Language} {V : Type u_1} (r : L.Relations 1) (u : V) : L.Formula V

Application of a unary relation symbol to a free variable.

def Cslib.Logic.FO.rel₂ {L : FirstOrder.Language} {V : Type u_1} (r : L.Relations 2) (u w : V) : L.Formula V

Application of a binary relation symbol to two free variables.

@[simp]

theorem Cslib.Logic.FO.realize_varEq {L : FirstOrder.Language} {M : Type w} [L.Structure M] {V : Type u_1} (v : V → M) (u w : V) : (varEq u w).Realize v ↔ v u = v w

@[simp]

theorem Cslib.Logic.FO.realize_rel₁ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {V : Type u_1} (v : V → M) (r : L.Relations 1) (u : V) : (rel₁ r u).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v u]

@[simp]

theorem Cslib.Logic.FO.realize_rel₂ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {V : Type u_1} (v : V → M) (r : L.Relations 2) (u w : V) : (rel₂ r u w).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v u, v w]

theorem Cslib.Logic.FO.formula_realize_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] {V : Type u_1} {v : V → M} : ⊤.Realize v

The formula ⊤ holds, as a term.

theorem Cslib.Logic.FO.relMap_pair_equiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (R : L.Relations 2) (a b : M) : FirstOrder.Language.Structure.RelMap R ![e a, e b] ↔ FirstOrder.Language.Structure.RelMap R ![a, b]

An isomorphism preserves a binary relation on pairs.

theorem Cslib.Logic.FO.relMap_single_equiv {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (R : L.Relations 1) (a : M) : FirstOrder.Language.Structure.RelMap R ![e a] ↔ FirstOrder.Language.Structure.RelMap R ![a]

An isomorphism preserves a unary relation.

Order combinators on Fin B

def Cslib.Logic.FO.lt {L : FirstOrder.Language} (r : L.Relations 2) {V : Type u_1} (u w : V) : L.Formula V

The strict order formula u < w with respect to a binary relation symbol r.

def Cslib.Logic.FO.le {L : FirstOrder.Language} (r : L.Relations 2) {V : Type u_1} (u w : V) : L.Formula V

The weak order formula u ≤ w (¬ (w < u)) with respect to r.

def Cslib.Logic.FO.isZero {L : FirstOrder.Language} (r : L.Relations 2) {V : Type u_1} (u : V) : L.Formula V

The formula ∀ z, ¬ (z < u), characterizing the minimum element 0 of Fin B.

def Cslib.Logic.FO.isMax {L : FirstOrder.Language} (r : L.Relations 2) {V : Type u_1} (u : V) : L.Formula V

The formula ∀ z, ¬ (u < z), characterizing the maximum element B - 1 of Fin B.

def Cslib.Logic.FO.succ {L : FirstOrder.Language} (r : L.Relations 2) {V : Type u_1} (u w : V) : L.Formula V

The successor formula u < w ∧ ∀ z, ¬ (u < z) ∨ ¬ (z < w), characterizing (w : ℕ) = (u : ℕ) + 1 on Fin B.

noncomputable def Cslib.Logic.FO.isFirstOut {L : FirstOrder.Language} (r : L.Relations 2) (inDom : L.Formula (Fin 1)) {V : Type u_1} (u : V) : L.Formula V

Given a domain formula inDom : L.Formula (Fin 1) holding of < M, the formula isFirstOut r inDom u asserts ¬ inDom(u) ∧ ∀ k < u, inDom(k), holding solely of M.

theorem Cslib.Logic.FO.realize_lt {L : FirstOrder.Language} {B : ℕ} [L.Structure (Fin B)] {r : L.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {V : Type u_1} (v : V → Fin B) (u w : V) : (lt r u w).Realize v ↔ v u < v w

theorem Cslib.Logic.FO.realize_le {L : FirstOrder.Language} {B : ℕ} [L.Structure (Fin B)] {r : L.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {V : Type u_1} (v : V → Fin B) (u w : V) : (le r u w).Realize v ↔ v u ≤ v w

theorem Cslib.Logic.FO.realize_isZero {L : FirstOrder.Language} {B : ℕ} [L.Structure (Fin B)] {r : L.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {V : Type u_1} (v : V → Fin B) (u : V) : (isZero r u).Realize v ↔ ↑(v u) = 0

On Fin B, with r read as <, isZero r u holds exactly when u is assigned 0.

theorem Cslib.Logic.FO.realize_isMax {L : FirstOrder.Language} {B : ℕ} [L.Structure (Fin B)] {r : L.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {V : Type u_1} (v : V → Fin B) (u : V) : (isMax r u).Realize v ↔ ↑(v u) = B - 1

On Fin B, with r read as <, isMax r u holds exactly when u is assigned B - 1.

theorem Cslib.Logic.FO.realize_succ {L : FirstOrder.Language} {B : ℕ} [L.Structure (Fin B)] {r : L.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {V : Type u_1} (v : V → Fin B) (u w : V) : (succ r u w).Realize v ↔ ↑(v w) = ↑(v u) + 1

On Fin B, with r read as <, succ r u w holds exactly when w is assigned the successor of the value of u.

theorem Cslib.Logic.FO.realize_isFirstOut {L : FirstOrder.Language} {B : ℕ} [L.Structure (Fin B)] {r : L.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {inDom : L.Formula (Fin 1)} {M : ℕ} (hMB : M < B) (hdom : ∀ (j : Fin B), inDom.Realize ![j] ↔ ↑j < M) {V : Type u_1} (v : V → Fin B) (u : V) : (isFirstOut r inDom u).Realize v ↔ ↑(v u) = M

On Fin B, with r read as < and a domain formula holding exactly below M < B, isFirstOut r inDom u holds exactly when u is assigned M.

Finite-domain cardinality and truth-table sentences

theorem Cslib.Logic.FO.realize_cardGe_iff_le_card {L : FirstOrder.Language} {M : Type w} [L.Structure M] [Finite M] (n : ℕ) : M ⊨ FirstOrder.Language.Sentence.cardGe L n ↔ n ≤ Nat.card M

On a finite structure M, Mathlib's Sentence.cardGe L n holds iff n ≤ Nat.card M.

def Cslib.Logic.FO.cardEqSentence (L : FirstOrder.Language) (n : ℕ) : L.Sentence

The first-order sentence Sentence.cardGe L n ⊓ ∼(Sentence.cardGe L (n + 1)), which holds on a finite structure M iff Nat.card M = n.

@[simp]

theorem Cslib.Logic.FO.realize_cardEqSentence {L : FirstOrder.Language} {M : Type w} [L.Structure M] [Finite M] (n : ℕ) : M ⊨ cardEqSentence L n ↔ Nat.card M = n

On a finite structure, cardEqSentence L n holds exactly when the structure has n elements.

noncomputable def Cslib.Logic.FO.truthTableSentence {L : FirstOrder.Language} {m : ℕ} (φ : Fin m → L.Sentence) (P : (Fin m → Bool) → Prop) : L.Sentence

Given m sentences φ and a predicate P on bit vectors Fin m → Bool, the first-order sentence asserting that the truth values i ↦ (M ⊨ φ i) satisfy P.

@[simp]

theorem Cslib.Logic.FO.realize_truthTableSentence {L : FirstOrder.Language} {M : Type w} [L.Structure M] {m : ℕ} (φ : Fin m → L.Sentence) (P : (Fin m → Bool) → Prop) : M ⊨ truthTableSentence φ P ↔ P fun (i : Fin m) => decide (M ⊨ φ i)

truthTableSentence φ P holds exactly when the truth values of the sentences φ i satisfy P.