QBF is second-order definable

The membership half of the completeness of DescriptiveComplexity.QBF: a quantified Boolean formula problem with k alternating blocks is Σₖ-definable when its prefix starts existentially, and Πₖ-definable when it starts universally (DescriptiveComplexity.qbfProblem_sigmaSODefinable, DescriptiveComplexity.qbfProblem_piSODefinable).

The second-order prefix is k monadic blocks (DescriptiveComplexity.unaryBlock: one unary relation variable each), one per quantifier block of the formula, and the first-order kernel simply evaluates the matrix: it says that every clause contains a true literal (or, for a disjunctive matrix, that some term has all its literals true), reading the truth value of a variable off the relation variable of a block marking it. No Tseitin translation is involved here – the matrix is already part of the input structure, so evaluating it is first-order.

The blocks are handled through DescriptiveComplexity.SecondOrderMerge: the kernel is written over the single merged block, where the relation variable of block i is the symbol DescriptiveComplexity.blockSym k i, and DescriptiveComplexity.sorealize_unmerge transports it into the iterated block expansion while turning the alternating second-order quantification into DescriptiveComplexity.altQuant.

The monadic blocks of a quantifier prefix

@[reducible]

def DescriptiveComplexity.unaryBlock : SOBlock

The second-order block of a single propositional quantifier: one unary relation variable, the truth assignment of one block of variables.

Equations

• DescriptiveComplexity.unaryBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.qbfBlocks (k : ℕ) : List SOBlock

The quantifier prefix of QBF k: k monadic blocks.

Equations

• DescriptiveComplexity.qbfBlocks k = List.replicate k DescriptiveComplexity.unaryBlock

@[simp]

theorem DescriptiveComplexity.qbfBlocks_length (k : ℕ) : (qbfBlocks k).length = k

@[reducible, inline]

abbrev DescriptiveComplexity.qbfMergedBlock (k : ℕ) : SOBlock

The single block merging the whole prefix of QBF k.

Equations

• DescriptiveComplexity.qbfMergedBlock k = DescriptiveComplexity.mergeBlocks (DescriptiveComplexity.qbfBlocks k)

def DescriptiveComplexity.blockSym (k : ℕ) : Fin k → (qbfMergedBlock k).lang.Relations 1

The relation symbol of the truth assignment of block i, in the merged block's vocabulary.

Equations

• DescriptiveComplexity.blockSym 0 i = i.elim0
• DescriptiveComplexity.blockSym n.succ ⟨0, isLt⟩ = ⟨Sum.inl (), ⋯⟩
• DescriptiveComplexity.blockSym k.succ ⟨j.succ, hj⟩ = ⟨Sum.inr ↑(DescriptiveComplexity.blockSym k ⟨j, ⋯⟩), ⋯⟩

def DescriptiveComplexity.repAssign (A : Type) (k : ℕ) : (Fin k → A → Prop) → (qbfMergedBlock k).Assignment A

The assignment of the merged block determined by k truth assignments.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.repAssign A 0 x_2 = DescriptiveComplexity.nilAssign A

theorem DescriptiveComplexity.repAssign_blockSym {A : Type} (k : ℕ) (νs : Fin k → A → Prop) (i : Fin k) (x : A) : FirstOrder.Language.Structure.RelMap (blockSym k i) ![x] ↔ νs i x

Reading back the truth assignment of block i from the merged assignment.

The prefix quantifies the components of the merged assignment

theorem DescriptiveComplexity.altAssign_qbfBlocks {A : Type} (k : ℕ) (P : (qbfMergedBlock k).Assignment A → Prop) (pol : Bool) : altAssign A (qbfBlocks k) P pol ↔ altQuant A k (fun (νs : Fin k → A → Prop) => P (repAssign A k νs)) pol

Alternating quantification over the components of the merged assignment of a monadic prefix is alternating quantification over k truth assignments.

The first-order kernel

@[reducible, inline]

abbrev DescriptiveComplexity.qbfSOLang (k : ℕ) : FirstOrder.Language

The vocabulary of the kernel: quantified CNF instances together with the k truth-assignment relation variables.

Equations

• DescriptiveComplexity.qbfSOLang k = (FirstOrder.Language.qbf k).sum (DescriptiveComplexity.qbfMergedBlock k).lang

@[reducible, inline]

abbrev DescriptiveComplexity.qIsClSym (k : ℕ) : (qbfSOLang k).Relations 1

The symbol for “is a clause” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.qIsClSym k = Sum.inl FirstOrder.Language.qbfIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.qPosSym (k : ℕ) : (qbfSOLang k).Relations 2

The symbol for “occurs positively in” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.qPosSym k = Sum.inl FirstOrder.Language.qbfPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.qNegSym (k : ℕ) : (qbfSOLang k).Relations 2

The symbol for “occurs negatively in” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.qNegSym k = Sum.inl FirstOrder.Language.qbfNegIn

@[reducible, inline]

abbrev DescriptiveComplexity.qBlkSym {k : ℕ} (i : Fin k) : (qbfSOLang k).Relations 1

The block mark of block i in the kernel's vocabulary.

Equations

• DescriptiveComplexity.qBlkSym i = Sum.inl (FirstOrder.Language.qbfBlock i)

@[reducible, inline]

abbrev DescriptiveComplexity.qNuSym {k : ℕ} (i : Fin k) : (qbfSOLang k).Relations 1

The truth-assignment variable of block i in the kernel's vocabulary.

Equations

• DescriptiveComplexity.qNuSym i = Sum.inr (DescriptiveComplexity.blockSym k i)

noncomputable def DescriptiveComplexity.qbfValF (k : ℕ) {γ : Type} (x : γ) : (qbfSOLang k).Formula γ

The truth value of the variable x, as a formula: some block marking x assigns it the value true.

Equations

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

@[instance_reducible]

def DescriptiveComplexity.qbfSOStructure {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) : (qbfSOLang k).Structure A

The interpretation of the kernel's vocabulary determined by k truth assignments.

Equations

• DescriptiveComplexity.qbfSOStructure νs = inferInstance

theorem DescriptiveComplexity.relMap_qNuSym {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) (i : Fin k) (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap (qNuSym i) w ↔ νs i (w 0)

The truth-assignment variables are read as the truth assignments.

theorem DescriptiveComplexity.realize_qbfValF {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) {γ : Type} (x : γ) (v : γ → A) : (qbfValF k x).Realize v ↔ qbfVal νs (v x)

noncomputable def DescriptiveComplexity.qbfCnfKernel (k : ℕ) : (qbfSOLang k).Sentence

The kernel for a conjunctive matrix: every clause contains a true literal.

Equations

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

noncomputable def DescriptiveComplexity.qbfDnfKernel (k : ℕ) : (qbfSOLang k).Sentence

The kernel for a disjunctive matrix: some term has all its literals true.

Equations

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

noncomputable def DescriptiveComplexity.qbfKernel (k : ℕ) (cnf : Bool) : (qbfSOLang k).Sentence

The kernel of the Σₖ/Πₖ definition of a quantified Boolean formula problem, for either shape of matrix.

Equations

• DescriptiveComplexity.qbfKernel k true = DescriptiveComplexity.qbfCnfKernel k
• DescriptiveComplexity.qbfKernel k false = DescriptiveComplexity.qbfDnfKernel k

theorem DescriptiveComplexity.realize_qbfKernel (k : ℕ) (cnf : Bool) {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) : A ⊨ qbfKernel k cnf ↔ QbfMatrix cnf νs

The kernel defines the matrix: under the interpretation of the relation variables by k truth assignments, the kernel says exactly that the matrix is satisfied.

Membership

theorem DescriptiveComplexity.qbfProblem_sigmaSODefinable (k : ℕ) (cnf : Bool) : SigmaSODefinable k (QbfProblem k true cnf)

QBF with an existential outermost block is Σₖ-definable: quantify the k truth assignments as monadic second-order variables, and evaluate the matrix in first-order logic.

theorem DescriptiveComplexity.qbfProblem_piSODefinable (k : ℕ) (cnf : Bool) : PiSODefinable k (QbfProblem k false cnf)

QBF with a universal outermost block is Πₖ-definable.