Documentation

Complexitylib.DescriptiveComplexity.ModelChecking

Computable first-order model checking #

Over a finite structure the quantifiers of first-order logic range over a finite universe, so satisfaction is decidable. This module gives a Bool-valued evaluator Formula.evalB over a decidable structure (DecFinStruct) and proves it agrees with the propositional Sat/Models.

Computable FO model checking is a prerequisite for several roadmap L6 milestones: the ∃SO ⊆ NP direction of Fagin's theorem (an NP machine guesses the witnessing relations and checks the FO matrix in polynomial time), the Immerman–Vardi characterization, and the FO ⊆ AC⁰ bridge.

Main definitions and results #

source
def Complexity.DescriptiveComplexity.Formula.evalB {V : Vocabulary} (A : DecFinStruct V) {n : Nat} :
Env A.card n → Formula V n → Bool

Computable Bool-valued first-order model checking over a decidable finite structure: quantifiers range over the finite universe Fin card via List.finRange.

Equations
Instances For
    source
    theorem Complexity.DescriptiveComplexity.Formula.evalB_eq_sat {V : Vocabulary} (A : DecFinStruct V) {n : Nat} (φ : Formula V n) (σ : Env A.card n) :
    evalB A σ φ = true ↔ Sat A.toFinStruct σ φ

    FO model checking is correct: the Bool evaluator agrees with satisfaction.

    source
    def Complexity.DescriptiveComplexity.Sentence.evalB {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) :
    Bool

    Model checking of a first-order sentence on a decidable structure.

    Equations
    Instances For
      source
      theorem Complexity.DescriptiveComplexity.Sentence.evalB_eq_models {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) :
      evalB A φ = true ↔ Models A.toFinStruct φ

      Sentence model checking is correct.

      source
      @[implicit_reducible]
      instance Complexity.DescriptiveComplexity.decidableModels {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) :
      Decidable (Sentence.Models A.toFinStruct φ)

      First-order truth over a finite structure is decidable (via the correct Bool evaluator).

      Equations