First-order model checking in constant depth

A structure for a relational first-order language L on the universe Fin n is determined by the truth values of its atomic facts R(a₁, …, aₗ) (ModelChecking.Atom, ModelChecking.Model), and every structure with n elements is isomorphic to one of these through an enumeration (ModelChecking.realize_iff_atomsOf). Expanding each universal quantifier into a conjunction over the n elements turns a first-order formula into a formula of negations and unbounded fan-in conjunctions and disjunctions over the atomic facts (ModelChecking.toUnbounded), which computes whether the structure satisfies it (ModelChecking.eval_toUnbounded). Its depth is bounded independently of n (ModelChecking.depth_toUnbounded_le) and its size is polynomial in n (ModelChecking.size_toUnbounded_le). This is the easy, nonuniform half of the characterization of AC⁰ by first-order logic Immerman, Chapter 5, Barrington, Immerman and Straubing, for relational vocabularies and without numerical predicates such as order or BIT; it reads as membership in AC⁰ once the atomic facts are the input bits, which needs a relation symbol of positive arity for the number of facts to grow with n.

Sentences are those of Mathlib's model theory (FirstOrder.Language.Sentence), and the statements are about structures rather than an encoding of structures as bit strings.

Main definitions

• Cslib.Circuits.Boolean.ModelChecking.Atom: the atomic facts of a structure on Fin n.
• Cslib.Circuits.Boolean.ModelChecking.Model: the structure with given true atomic facts.
• Cslib.Circuits.Boolean.ModelChecking.toUnbounded: a first-order formula as a formula over the unbounded fan-in basis.

Main results

• Cslib.Circuits.Boolean.ModelChecking.exists_formula_realize_structure: every first-order sentence is decided on the structures with n elements by unbounded fan-in formulas of constant depth and polynomial size.
• Cslib.Circuits.Boolean.ModelChecking.leafSize_toUnbounded_le: the formulas have polynomially many leaves.

References

• N. Immerman, Descriptive Complexity
• [D. A. M. Barrington, N. Immerman, H. Straubing, On uniformity within NC¹] [BIS90]

def Cslib.Circuits.Boolean.ModelChecking.Atom (L : FirstOrder.Language) (n : ℕ) : Type u_2

The atomic facts of a structure for L on Fin n: a relation symbol and a tuple of elements.

def Cslib.Circuits.Boolean.ModelChecking.Model {L : FirstOrder.Language} {n : ℕ} (_x : Atom L n → Bool) : Type

The universe Fin n with the structure whose true atomic facts are those given by x.

@[instance_reducible]

instance Cslib.Circuits.Boolean.ModelChecking.instStructureModel {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} (x : Atom L n → Bool) : L.Structure (Model x)

@[instance_reducible]

instance Cslib.Circuits.Boolean.ModelChecking.instFintypeAtomOfSigmaNatRelations {L : FirstOrder.Language} {n : ℕ} [Fintype ((l : ℕ) × L.Relations l)] : Fintype (Atom L n)

def Cslib.Circuits.Boolean.ModelChecking.constUnbounded {N : ℕ} (b : Bool) : Formula Unbounded.signature N

The constant b as a formula over the unbounded fan-in basis.

@[simp]

theorem Cslib.Circuits.Boolean.ModelChecking.eval_constUnbounded {N : ℕ} (b : Bool) (y : Fin N → Bool) : (constUnbounded b).eval Unbounded.interpretation y = b

def Cslib.Circuits.Boolean.ModelChecking.toUnbounded {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} (e : Atom L n ≃ Fin N) {k : ℕ} : L.BoundedFormula Empty k → (Fin k → Fin n) → Formula Unbounded.signature N

A first-order formula, with values xs for its bound variables, as a formula over the unbounded fan-in basis reading the atomic facts through e: atomic formulas are inputs or constants, an implication is a disjunction with one negated argument, and a universal quantifier is a conjunction over the n elements. A term of the relational language L is a variable (Cslib.Logic.FO.termVar), here a bound one, with value given by xs.

theorem Cslib.Circuits.Boolean.ModelChecking.eval_toUnbounded {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} (e : Atom L n ≃ Fin N) (x : Atom L n → Bool) {k : ℕ} (φ : L.BoundedFormula Empty k) (xs : Fin k → Model x) : (toUnbounded e φ xs).eval Unbounded.interpretation (x ∘ ⇑e.symm) = true ↔ φ.Realize Empty.elim xs

The formula decides the first-order formula on the structure given by its atomic facts.

def Cslib.Circuits.Boolean.ModelChecking.foDepth {L : FirstOrder.Language} {k : ℕ} : L.BoundedFormula Empty k → ℕ

A measure of the depth of a first-order formula: atomic formulas count one, an implication two more than its arguments, and a quantifier one more than its body.

def Cslib.Circuits.Boolean.ModelChecking.foSize {L : FirstOrder.Language} {k : ℕ} : L.BoundedFormula Empty k → ℕ

The number of nodes of a first-order formula.

theorem Cslib.Circuits.Boolean.ModelChecking.foSize_pos {L : FirstOrder.Language} {k : ℕ} (φ : L.BoundedFormula Empty k) : 0 < foSize φ

theorem Cslib.Circuits.Boolean.ModelChecking.depth_toUnbounded_le {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} (e : Atom L n ≃ Fin N) {k : ℕ} (φ : L.BoundedFormula Empty k) (xs : Fin k → Fin n) : (toUnbounded e φ xs).depth ≤ foDepth φ

The depth does not depend on the universe.

theorem Cslib.Circuits.Boolean.ModelChecking.size_toUnbounded_le {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} (e : Atom L n ≃ Fin N) {k : ℕ} (φ : L.BoundedFormula Empty k) (xs : Fin k → Fin n) : (toUnbounded e φ xs).size ≤ foSize φ * (n + 2) ^ foSize φ

The size is polynomial in the universe.

theorem Cslib.Circuits.Boolean.ModelChecking.leafSize_toUnbounded_le {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} (e : Atom L n ≃ Fin N) {k : ℕ} (φ : L.BoundedFormula Empty k) (xs : Fin k → Fin n) : (toUnbounded e φ xs).leafSize ≤ (n + 2) ^ foSize φ

The number of leaves is polynomial in the universe.

Arbitrary finite structures

noncomputable def Cslib.Circuits.Boolean.ModelChecking.atomsOf {L : FirstOrder.Language} {n : ℕ} {M : Type u_1} [L.Structure M] (e : M ≃ Fin n) : Atom L n → Bool

The atomic facts of a structure on M, read through an enumeration e of M by Fin n.

def Cslib.Circuits.Boolean.ModelChecking.equivModel {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} {M : Type u_1} [L.Structure M] (e : M ≃ Fin n) : L.Equiv M (Model (atomsOf e))

An enumeration of M is an isomorphism onto the structure with the atomic facts of M.

theorem Cslib.Circuits.Boolean.ModelChecking.realize_iff_atomsOf {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} {M : Type u_1} [L.Structure M] (e : M ≃ Fin n) (φ : L.Sentence) : M ⊨ φ ↔ Model (atomsOf e) ⊨ φ

A structure satisfies a sentence exactly when the structure with its atomic facts does.

theorem Cslib.Circuits.Boolean.ModelChecking.eval_toUnbounded_atomsOf {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} {M : Type u_1} [L.Structure M] (e : Atom L n ≃ Fin N) (eM : M ≃ Fin n) (φ : L.Sentence) : (toUnbounded e φ Fin.elim0).eval Unbounded.interpretation (atomsOf eM ∘ ⇑e.symm) = true ↔ M ⊨ φ

The translation of a sentence decides it on every structure, through its atomic facts.

theorem Cslib.Circuits.Boolean.ModelChecking.exists_formula_realize {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} (φ : L.Sentence) (e : Atom L n ≃ Fin N) : ∃ (F : Formula Unbounded.signature N), (∀ (x : Atom L n → Bool), F.eval Unbounded.interpretation (x ∘ ⇑e.symm) = true ↔ Model x ⊨ φ) ∧ F.depth ≤ foDepth φ ∧ F.size ≤ foSize φ * (n + 2) ^ foSize φ

First-order sentences are decided in constant depth: for a relational language, every sentence is decided on the structures with n elements, given by their atomic facts, by a formula of negations and unbounded fan-in conjunctions and disjunctions whose depth does not depend on n and whose size is polynomial in n.

theorem Cslib.Circuits.Boolean.ModelChecking.exists_formula_realize_structure {L : FirstOrder.Language} [L.IsRelational] {n N : ℕ} (φ : L.Sentence) (e : Atom L n ≃ Fin N) : ∃ (F : Formula Unbounded.signature N), (∀ (M : Type) [inst : L.Structure M] (eM : M ≃ Fin n), F.eval Unbounded.interpretation (atomsOf eM ∘ ⇑e.symm) = true ↔ M ⊨ φ) ∧ F.depth ≤ foDepth φ ∧ F.size ≤ foSize φ * (n + 2) ^ foSize φ

The same formula decides the sentence on every structure with n elements, through any enumeration of it.