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

The prefix quantifies the components of the merged assignment

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.

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.