Documentation

Complexitylib.DescriptiveComplexity.SecondOrder.Definable

Existential second-order definability #

ExistSODefinable retains a syntactic existential SO witness for a query. It is closed under intersection, union, and universe-preserving FO reductions, includes FO definability, and implies isomorphism invariance. Its induced languages have verified binary certificate checkers and polynomial witness bounds. The downstream SecondOrder.PolynomialTime module proves their membership in the machine class Complexity.NP, the upper direction of Fagin's theorem (Fagin, 1974).

The separation of a definability witness from reduction transport follows the organization of Senellart and Gnatenko (2026), Sections 3--4, https://arxiv.org/abs/2609.18261, specialized to our existing interpretations.

source
def Complexity.DescriptiveComplexity.ExistSODefinable {V : Vocabulary} (Q : BooleanQuery V) :
Prop

A query defined by an existential SO prefix followed by an FO matrix.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.DescriptiveComplexity.ExistSODefinable.toSODefinable {V : Vocabulary} {Q : BooleanQuery V} (hQ : ExistSODefinable Q) :
    SODefinable Q

    An existential SO witness is in particular a second-order witness.

    source
    theorem Complexity.DescriptiveComplexity.ExistSODefinable.orderIndependent {V : Vocabulary} {Q : BooleanQuery V} (hQ : ExistSODefinable Q) :
    Q.IsOrderIndependent

    Existential SO definability implies invariance under isomorphism.

    source
    theorem Complexity.DescriptiveComplexity.FODefinable.toExistSODefinable {V : Vocabulary} {Q : BooleanQuery V} (hQ : FODefinable Q) :
    ExistSODefinable Q

    A first-order witness is an existential SO witness with an empty prefix.

    source
    theorem Complexity.DescriptiveComplexity.ExistSODefinable.inter {V : Vocabulary} {Q₁ Q₂ : BooleanQuery V} (h₁ : ExistSODefinable Q₁) (h₂ : ExistSODefinable Q₂) :
    ExistSODefinable (Q₁.inter Q₂)

    Existential SO queries are closed under intersection by merging their witness prefixes.

    source
    theorem Complexity.DescriptiveComplexity.ExistSODefinable.union {V : Vocabulary} {Q₁ Q₂ : BooleanQuery V} (h₁ : ExistSODefinable Q₁) (h₂ : ExistSODefinable Q₂) :
    ExistSODefinable (Q₁.union Q₂)

    Existential SO queries are closed under union by merging their witness prefixes.

    source
    theorem Complexity.DescriptiveComplexity.ExistSODefinable.exists_bounded_certificate {V : Vocabulary} {Q : BooleanQuery V} (hQ : ExistSODefinable Q) :
    ∃ (φ : SOSentence V) (h : SOFormula.IsExistSO φ), ∀ (input : List Bool), input ∈ queryLanguage Q ↔ ∃ (certificate : List Bool), certificate.length ≤ Polynomial.eval input.length (SOFormula.witnessPolynomial φ) ∧ φ.checkEncoded h input certificate = true

    An existential SO query has an exact binary verifier with polynomially bounded certificates.

    source
    theorem Complexity.DescriptiveComplexity.ExistSODefinable.of_reduces {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (hQ₂ : ExistSODefinable Q₂) (hred : FOReduces Q₁ Q₂) :
    ExistSODefinable Q₁

    Existential SO definability travels backward through FO reductions.

    source
    theorem Complexity.DescriptiveComplexity.ExistSODefinable.of_projReduces {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (hQ₂ : ExistSODefinable Q₂) (hred : FOProjReduces Q₁ Q₂) :
    ExistSODefinable Q₁

    Existential SO definability also travels backward through quantifier-free reductions.

    source
    theorem Complexity.DescriptiveComplexity.not_foReduces_of_not_existSODefinable {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (hQ₁ : ¬ExistSODefinable Q₁) (hQ₂ : ExistSODefinable Q₂) :
    ¬FOReduces Q₁ Q₂

    An inexpressibility result rules out every FO reduction to an existential SO query.