Existential second-order definable classes reduce to SAT by order-free interpretations

The reductions in this module use order-free first-order interpretations. Input structures have no built-in order or numeric predicates; these results are order-free variants of the standard ones.

Every existential second-order definable class of finite structures that contains every empty structure is order-free reducible to the class cnf.SAT of satisfiable CNF structures (Cslib.Logic.ESO.Definable.reduces_SAT). With Fagin's theorem this gives the NP-completeness of SAT under order-free reductions, for classes containing every empty structure; see Complexity.Computability.Complexity.Fagin.SAT. This is an adaptation of the descriptive form of the Cook–Levin theorem Immerman, Chapter 7: Immerman's structures are ordered and have at least two elements, and his reductions are first-order projections, while this module uses first-order interpretations, with quantifiers, of unordered structures. Neither statement implies the other.

The reduction grounds the sentence. Let Φ = ∃ R₁ … Rₖ, φ and let M be a finite structure. For every subformula ψ of φ with k bound variables and every tuple a ∈ Mᵏ there is a propositional variable X(ψ, a), read as "ψ holds of a", and for every relation variable R of arity m and every b ∈ Mᵐ a propositional variable V(R, b), read as "R holds of b". Clauses force each X(ψ, a) to agree with the meaning of ψ, in the manner of Tseitin's encoding: X(⊥, a) is false, an equation or an atom of the input language is decided by M, an atom R(t) is equivalent to V(R, t(a)), X(ψ → χ, a) is equivalent to X(ψ, a) → X(χ, a), and X(∀x ψ, a) is equivalent to the conjunction of the X(ψ, a b); a last clause asserts X(φ, ()). Each satisfying assignment then defines relations Rᵢ making φ true, and conversely.

The propositional variables and clauses are of finitely many kinds, which are the tags of a tagged interpretation (Cslib.Logic.ESO.Sentence.groundInterpretation) whose literals are defined by templates. On structures with at most one element, where tags cannot be told apart, the reduction evaluates Φ directly: every relation is empty or full, so a finite disjunction of first-order sentences decides it (Cslib.Logic.ESO.Sentence.subsingletonSentence). Every empty structure is mapped to the empty CNF structure, which is satisfiable; this is why the class must contain every empty structure.

Main definitions

• Cslib.Logic.ESO.Sentence.GroundTag, Cslib.Logic.ESO.Sentence.groundInterpretation: the grounding of an existential second-order sentence, a tagged interpretation in CNF structures.
• Cslib.Logic.ESO.Sentence.subsingletonSentence: a first-order sentence equivalent to Φ on structures with at most one element.

Main results

• Cslib.Logic.ESO.Sentence.satisfiable_groundInterpretation_iff: the grounding of Φ in a nonempty structure M is satisfiable exactly when Φ holds in M.
• Cslib.Logic.ESO.Sentence.realize_subsingletonSentence: correctness of the sentence on structures with at most one element.
• Cslib.Logic.ESO.Definable.reduces_SAT: every existential second-order definable class containing every empty structure is order-free reducible to SAT.
• Cslib.Logic.ESO.definable_iff_reduces_SAT: for classes containing every empty structure, existential second-order definability is order-free reducibility to SAT.
• Cslib.Logic.ESO.Definable.exists_interpretation_SAT_of_nonempty: every existential second-order definable class is order-free reducible to SAT on the nonempty finite structures.

References

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

The grounding

@[reducible, inline]

abbrev Cslib.Logic.ESO.Sentence.Subformula {L : FirstOrder.Language} (Φ : Sentence L) : Type (max u v)

The subformulas of the first-order part of Φ.

instance Cslib.Logic.ESO.Sentence.instFiniteSubformula {L : FirstOrder.Language} (Φ : Sentence L) : Finite Φ.Subformula

inductive Cslib.Logic.ESO.Sentence.GroundTag {L : FirstOrder.Language} (Φ : Sentence L) : Type (max u v)

The kinds of propositional variables and clauses of the grounding of Φ: a variable for each subformula and each relation variable, the clause asserting the first-order part, and up to three clauses for each subformula.

• var {L : FirstOrder.Language} {Φ : Sentence L} (s : Φ.Subformula) : Φ.GroundTag

  The variables X(ψ, a): the subformula ψ holds of the tuple a.

• relVar {L : FirstOrder.Language} {Φ : Sentence L} (r : Φ.Var) : Φ.GroundTag

  The variables V(R, b): the relation variable R holds of the tuple b.

• top {L : FirstOrder.Language} {Φ : Sentence L} : Φ.GroundTag

  The clause X(φ, ()).

• clause {L : FirstOrder.Language} {Φ : Sentence L} (s : Φ.Subformula) (i : Fin 3) : Φ.GroundTag

  The clauses defining X(ψ, a).

instance Cslib.Logic.ESO.Sentence.instFiniteGroundTag {L : FirstOrder.Language} (Φ : Sentence L) : Finite Φ.GroundTag

def Cslib.Logic.ESO.Sentence.GroundTag.Coord {L : FirstOrder.Language} {Φ : Sentence L} : Φ.GroundTag → Type

The coordinates of the elements of each kind: those of X(ψ, a) are the bound variables of ψ, those of V(R, b) the arguments of R, and those of a clause defining X(ψ, a) are the bound variables of ψ and one more, the value of the quantified variable when ψ = ∀x χ.

instance Cslib.Logic.ESO.Sentence.instFiniteGroundTagCoord {L : FirstOrder.Language} {Φ : Sentence L} (t : Φ.GroundTag) : Finite t.Coord

def Cslib.Logic.ESO.Sentence.termCoord {L : FirstOrder.Language} [L.IsRelational] {Φ : Sentence L} {k : ℕ} (t : (L.sum (varLanguage Φ.arity)).Term (Empty ⊕ Fin k)) : Fin (k + 1)

The coordinate of a clause holding the value of a term, a variable of the subformula.

def Cslib.Logic.ESO.Sentence.selfVar {L : FirstOrder.Language} {Φ : Sentence L} (s : Φ.Subformula) (i : Fin 3) (guard : L.Formula (Fin ((↑s).fst + 1))) : FO.TaggedInterpretation.Template L GroundTag.Coord (GroundTag.clause s i)

The template relating a clause to the variable X(ψ, a) of its subformula.

def Cslib.Logic.ESO.Sentence.clauseTemplates {L : FirstOrder.Language} [L.IsRelational] {Φ : Sentence L} (s : Φ.Subformula) (i : Fin 3) : Bool → List (FO.TaggedInterpretation.Template L GroundTag.Coord (GroundTag.clause s i))

The templates of the literals of polarity b of the clauses i of a subformula.

def Cslib.Logic.ESO.Sentence.groundTemplates {L : FirstOrder.Language} [L.IsRelational] (Φ : Sentence L) (t : Φ.GroundTag) : Bool → List (FO.TaggedInterpretation.Template L GroundTag.Coord t)

The templates of the literals of polarity b of the elements of each kind. A variable names the tautology x ∨ ¬x of itself.

noncomputable def Cslib.Logic.ESO.Sentence.groundInterpretation {L : FirstOrder.Language} [L.IsRelational] (Φ : Sentence L) : FO.TaggedInterpretation L FO.cnf Φ.GroundTag GroundTag.Coord

The grounding of Φ, a tagged interpretation in CNF structures. A clause kind without templates has no elements.

Correctness of the clauses

Correctness of the grounding

theorem Cslib.Logic.ESO.Sentence.satisfiable_groundInterpretation_iff {L : FirstOrder.Language} [L.IsRelational] {Φ : Sentence L} {M : Type w} [L.Structure M] [Nonempty M] : FO.cnf.Satisfiable (Φ.groundInterpretation.Model M) ↔ Φ.Realize M

The grounding is correct: the grounding of Φ in a nonempty structure M is satisfiable exactly when Φ holds in M.

Structures with at most one element

def Cslib.Logic.ESO.Sentence.constInterpretation {L : FirstOrder.Language} (Φ : Sentence L) (s : Φ.Var → Bool) : FO.Interpretation L (L.sum (varLanguage Φ.arity)) Unit

The interpretation substituting ⊤ or ⊥ for each relation variable, according to s.

noncomputable def Cslib.Logic.ESO.Sentence.subsingletonSentence {L : FirstOrder.Language} [L.IsRelational] (Φ : Sentence L) : L.Sentence

On structures with at most one element, every relation is empty or full: the first-order sentence that Φ holds for some choice of empty and full relations.

theorem Cslib.Logic.ESO.Sentence.realize_subsingletonSentence {L : FirstOrder.Language} [L.IsRelational] {Φ : Sentence L} {M : Type w} [L.Structure M] [Subsingleton M] : M ⊨ Φ.subsingletonSentence ↔ Φ.Realize M

Correctness of the sentence for small structures.

noncomputable def Cslib.Logic.ESO.Sentence.subsingletonInterpretation {L : FirstOrder.Language} [L.IsRelational] (Φ : Sentence L) : FO.Interpretation L FO.cnf Unit

The reduction on structures with at most one element: a single element naming the clause x if Φ holds and the empty clause otherwise.

SAT is complete for existential second-order logic under order-free reductions

theorem Cslib.Logic.ESO.Definable.reduces_SAT {L : FirstOrder.Language} [L.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} (hK : Definable K) (hempty : ∀ (M : CategoryTheory.Bundled L.Structure), IsEmpty ↑M → M ∈ K) : FO.Reduces K FO.cnf.SAT

Every existential second-order definable class containing every empty structure is order-free reducible to SAT Immerman, Chapter 7. The reduction grounds the defining sentence (Cslib.Logic.ESO.Sentence.groundInterpretation). The empty-structure hypothesis cannot be dropped in general: an interpretation of positive dimension maps every empty input to the empty CNF structure, which is satisfiable.

theorem Cslib.Logic.ESO.definable_iff_reduces_SAT {L : FirstOrder.Language} [L.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} (hempty : ∀ (M : CategoryTheory.Bundled L.Structure), IsEmpty ↑M → M ∈ K) : Definable K ↔ FO.Reduces K FO.cnf.SAT

SAT is complete for existential second-order logic under order-free reductions: a class containing every empty structure is existential second-order definable exactly when it is order-free reducible to SAT.

theorem Cslib.Logic.ESO.Definable.exists_interpretation_SAT_of_nonempty {L : FirstOrder.Language} [L.IsRelational] {K : Set (CategoryTheory.Bundled L.Structure)} (hK : Definable K) : ∃ (ι : Type) (_ : Finite ι) (I : FO.Interpretation L FO.cnf ι), ∀ (M : CategoryTheory.Bundled L.Structure) [Finite ↑M] [Nonempty ↑M], M ∈ K ↔ CategoryTheory.Bundled.of (I.Model ↑M) ∈ FO.cnf.SAT

Every existential second-order definable class is order-free reducible to SAT on the nonempty structures: some first-order interpretation maps every nonempty finite structure inside SAT exactly when it is in the class. This is an order-free variant of Immerman, Chapter 7, whose structures are ordered and have at least two elements. The construction reduces the class with every empty structure added.