Second-order definability with bounded alternation

Foundation for defining the levels Σₖ/Πₖ (k ≥ 1) of the polynomial hierarchy logically, by Fagin's (Fagin 1974) and Stockmeyer's (Stockmeyer 1976) theorems: Σₖᵖ consists of the problems definable by a second-order sentence with k alternating blocks of second-order quantifiers starting existentially – on unordered finite structures (the first existential block can guess a linear order, so the order-free definition is equivalent to the classical ordered one).

No object-level second-order syntax is needed: a second-order quantifier block (DescriptiveComplexity.SOBlock) is a finite family of relation variables with given arities, its instantiations are Lean-level (SOBlock.structure turns an assignment of relations into a structure over the block's vocabulary SOBlock.lang), and only the first-order kernel is object-level – a sentence over the base language expanded by all blocks (DescriptiveComplexity.soLang). DescriptiveComplexity.SORealize evaluates the alternating quantification, and DescriptiveComplexity.SigmaSODefinable / DescriptiveComplexity.PiSODefinable state that a decision problem is defined by such a sentence on nonempty finite structures.

This file proves the two structural facts about these notions that do not involve reductions:

• isomorphism-invariance (DescriptiveComplexity.sorealize_iso) – so second-order definable properties are bona fide decision problems;
• the duality Πₖ = co-Σₖ (DescriptiveComplexity.piSODefinable_iff_compl), by negating the kernel and flipping the quantifiers.

The rest of the definitional theory lives in dedicated files: functoriality and padding in DescriptiveComplexity.SecondOrderLift, closure under FO reductions in DescriptiveComplexity.SecondOrderPull, closure under ordered FO reductions in DescriptiveComplexity.SecondOrderOrdered, and the resulting definition of the levels Σₖᵖ/Πₖᵖ for k ≥ 1 in DescriptiveComplexity.Hierarchy.

Second-order quantifier blocks

structure DescriptiveComplexity.SOBlock : Type 1

A second-order quantifier block: finitely many relation variables, with given arities. (The index type is arbitrary rather than an initial segment of ℕ, so that constructions on blocks – e.g. pulling a block back through an interpretation – can build their natural index types directly.)

• ι : Type

  The index type of the relation variables of the block.

• ιFinite : Finite self.ι

  A block has finitely many relation variables.

• arity : self.ι → ℕ

  The arity of each relation variable.

def DescriptiveComplexity.SOBlock.lang (B : SOBlock) : FirstOrder.Language

The (relational) vocabulary of a block: one relation symbol per relation variable.

Equations

• B.lang = { Functions := fun (x : ℕ) => Empty, Relations := fun (n : ℕ) => { i : B.ι // B.arity i = n } }

instance DescriptiveComplexity.instIsRelationalLang (B : SOBlock) : B.lang.IsRelational

noncomputable def DescriptiveComplexity.blockArityBound (B : SOBlock) : ℕ

A bound on the arities of a block: every relation variable of the block has arity at most blockArityBound B. Interpretations encoding the relation variables as tagged tuples use it to size their dimension.

Equations

• DescriptiveComplexity.blockArityBound B = Finset.univ.sup B.arity

theorem DescriptiveComplexity.arity_le_blockArityBound (B : SOBlock) (i : B.ι) : B.arity i ≤ blockArityBound B

def DescriptiveComplexity.SOBlock.Assignment (B : SOBlock) (A : Type) : Type

An assignment of actual relations (on a universe A) to the relation variables of a block.

Equations

• B.Assignment A = ((i : B.ι) → (Fin (B.arity i) → A) → Prop)

@[instance_reducible]

def DescriptiveComplexity.SOBlock.structure (B : SOBlock) {A : Type} (ρ : B.Assignment A) : B.lang.Structure A

The structure over the block's vocabulary determined by an assignment.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.soLang (L : FirstOrder.Language) : List SOBlock → FirstOrder.Language

The base language expanded by the vocabularies of a list of blocks.

Equations

• DescriptiveComplexity.soLang L [] = L
• DescriptiveComplexity.soLang L (B :: Bs) = DescriptiveComplexity.soLang (L.sum B.lang) Bs

def DescriptiveComplexity.SORealize (L : FirstOrder.Language) (A : Type) [inst : L.Structure A] (Bs : List SOBlock) : (soLang L Bs).Sentence → Bool → Prop

Alternating second-order satisfaction: SORealize L A Bs φ pol states that the sentence obtained from the first-order kernel φ by quantifying the blocks Bs alternately – existentially first if pol is true – holds in the L-structure A.

Equations

• DescriptiveComplexity.SORealize L A [] φ x✝ = A ⊨ φ
• DescriptiveComplexity.SORealize L A (B :: Bs) φ true = ∃ (ρ : B.Assignment A), DescriptiveComplexity.SORealize (L.sum B.lang) A Bs φ false
• DescriptiveComplexity.SORealize L A (B :: Bs) φ false = ∀ (ρ : B.Assignment A), DescriptiveComplexity.SORealize (L.sum B.lang) A Bs φ true

def DescriptiveComplexity.SigmaSODefinable {L : FirstOrder.Language} (k : ℕ) (P : DecisionProblem L) : Prop

A decision problem is Σₖ-definable if, on nonempty finite structures, it is defined by a second-order sentence with k alternating blocks of second-order quantifiers, starting existentially. (As everywhere in this development, complexity notions are about nonempty finite structures.)

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.PiSODefinable {L : FirstOrder.Language} (k : ℕ) (P : DecisionProblem L) : Prop

A decision problem is Πₖ-definable if, on nonempty finite structures, it is defined by a second-order sentence with k alternating blocks of second-order quantifiers, starting universally.

Equations

• One or more equations did not get rendered due to their size.

Isomorphism-invariance

def DescriptiveComplexity.SOBlock.mapAssign (B : SOBlock) {A A' : Type} (e : A ≃ A') (ρ : B.Assignment A) : B.Assignment A'

Transport of a block assignment along an equivalence.

Equations

• B.mapAssign e ρ i x = ρ i fun (j : Fin (B.arity i)) => e.symm (x j)

def DescriptiveComplexity.SOBlock.extendEquiv {L : FirstOrder.Language} (B : SOBlock) {A A' : Type} [L.Structure A] [L.Structure A'] (e : L.Equiv A A') (ρ : B.Assignment A) : (L.sum B.lang).Equiv A A'

An L-isomorphism extends to the vocabulary expanded by a block, when the block is interpreted by an assignment on one side and its transport on the other.

Equations

• B.extendEquiv e ρ = { toEquiv := e.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.sorealize_iso {L : FirstOrder.Language} {A A' : Type} [L.Structure A] [L.Structure A'] (e : L.Equiv A A') (Bs : List SOBlock) (φ : (soLang L Bs).Sentence) (pol : Bool) : SORealize L A Bs φ pol ↔ SORealize L A' Bs φ pol

Alternating second-order satisfaction is isomorphism-invariant: what a second-order sentence expresses is a decision problem.

Duality: Πₖ is co-Σₖ

theorem DescriptiveComplexity.piSODefinable_iff_compl {L : FirstOrder.Language} (k : ℕ) (P : DecisionProblem L) : PiSODefinable k P ↔ SigmaSODefinable k Pᶜ

A problem is Πₖ-definable iff its complement is Σₖ-definable.

theorem DescriptiveComplexity.sigmaSODefinable_iff_compl {L : FirstOrder.Language} (k : ℕ) (P : DecisionProblem L) : SigmaSODefinable k P ↔ PiSODefinable k Pᶜ

A problem is Σₖ-definable iff its complement is Πₖ-definable.

Atoms in the relation variables of a block

The clausal fragments of existential second-order logic – SO-Horn (DescriptiveComplexity.SecondOrderHorn) and SO-Krom (DescriptiveComplexity.SecondOrderKrom) – represent their first-order kernel as data: a list of clauses built from atoms in the quantified relation variables, over a shared list of universally quantified first-order variables. The atom type and its semantics are common to both fragments, so they live here.

structure DescriptiveComplexity.SOAtom (B : SOBlock) (k : ℕ) : Type

An atom R i (x_{f 0}, …) in the relation variables of a block, with arguments read from k universally quantified first-order variables.

• idx : B.ι

  The relation variable of the block the atom is about.

• args : Fin (B.arity self.idx) → Fin k

  The arguments, as indices among the k universally quantified variables.

def DescriptiveComplexity.SOAtom.Holds {B : SOBlock} {k : ℕ} {A : Type} (a : SOAtom B k) (ρ : B.Assignment A) (v : Fin k → A) : Prop

The truth value of a second-order atom under an assignment of the block and a valuation of the universally quantified variables.

Equations

• a.Holds ρ v = ρ a.idx fun (j : Fin (B.arity a.idx)) => v (a.args j)

theorem DescriptiveComplexity.SOAtom.holds_equiv {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) (a : SOAtom B k) (ρ : B.Assignment M) (v : Fin k → M) : (a.Holds (B.mapAssign e.toEquiv ρ) fun (j : Fin k) => e (v j)) ↔ a.Holds ρ v

Atoms are insensitive to transporting an assignment along an isomorphism.