Documentation

Complexitylib.DescriptiveComplexity.Definable

First-order definable queries #

A Boolean query is first-order definable when some FO sentence defines it. The central fact of descriptive complexity — that a logic can only define "legitimate" (order-independent) queries — is recorded here for first-order logic: every FO-definable query is order-independent (FODefinable.orderIndependent, a packaging of Immerman Proposition 1.16). Since FO has ¬, ∧, ∨, the FO-definable queries are closed under complement, intersection, and union.

This is the template for the logic/complexity correspondences on track L6: a class of logics defines a class of queries, and expressibility questions become lower bounds.

Main definitions and results #

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

A Boolean query is first-order definable if some FO sentence defines it.

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

    FO-definable queries are order-independent (Immerman Proposition 1.16, packaged): a query defined by an FO sentence cannot distinguish isomorphic structures.

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

    FO-definable queries are closed under complement (via ¬).

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

    FO-definable queries are closed under intersection (via ∧).

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

    FO-definable queries are closed under union (via ∨).

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

    FO-definability is closed under first-order reductions. If Q₁ reduces to an FO-definable query Q₂, translating a sentence for Q₂ along the reduction interpretation gives a sentence for Q₁.

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

    FO-definability is closed under first-order projections.

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

    FO ⊆ SO at the query level: every first-order definable query is second-order definable, via the truth-preserving FO embedding into SO.