Binary witness checking for existential second-order formulas

A certificate lists the truth tables of the leading existential relation quantifiers, in outermost-first order. Each quantifier reads exactly its table; the remaining FO matrix is checked only after all certificate bits are consumed. Both missing bits and trailing data are rejected. Free element values and free Boolean relation tables are also supported.

This implements the witness-checking algorithm of Immerman, Section 7.1, Proposition 7.6. Correctness and polynomial certificate length are proved in the surface module. SecondOrder.PolynomialTime supplies the polynomial-time machine bound by proving agreement with an arithmetic verifier.

def Complexity.DescriptiveComplexity.SOFormula.witnessArities {V : Vocabulary} {rctx : List ℕ} {n : ℕ} : SOFormula V rctx n → List ℕ

Arities of the leading existential relation quantifiers, outermost first.

Equations

• (Complexity.DescriptiveComplexity.SOFormula.soExist k φ).witnessArities = k :: φ.witnessArities
• x✝.witnessArities = []

noncomputable def Complexity.DescriptiveComplexity.SOFormula.witnessPolynomial {V : Vocabulary} {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) : Polynomial ℕ

The exact certificate length as a polynomial in the universe cardinality.

Equations

• φ.witnessPolynomial = Complexity.DescriptiveComplexity.DecREnv.encodingPolynomial φ.witnessArities

def Complexity.DescriptiveComplexity.SOFormula.checkCertificate {V : Vocabulary} (A : DecFinStruct V) {rctx : List ℕ} {n : ℕ} (φ : SOFormula V rctx n) : φ.IsExistSO → Env A.card n → DecREnv A.card rctx → List Bool → Bool

Check supplied truth tables for the existential prefix, then evaluate its matrix.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.SOFormula.checkCertificate A a.neg h x_2 x_3 x_4 = (x_4.isEmpty && Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A a.neg ⋯ x_2 x_3)
• Complexity.DescriptiveComplexity.SOFormula.checkCertificate A (a.conj a_1) h x_2 x_3 x_4 = (x_4.isEmpty && Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A (a.conj a_1) ⋯ x_2 x_3)
• Complexity.DescriptiveComplexity.SOFormula.checkCertificate A (a.disj a_1) h x_2 x_3 x_4 = (x_4.isEmpty && Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A (a.disj a_1) ⋯ x_2 x_3)
• Complexity.DescriptiveComplexity.SOFormula.checkCertificate A a.exist h x_2 x_3 x_4 = (x_4.isEmpty && Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A a.exist ⋯ x_2 x_3)
• Complexity.DescriptiveComplexity.SOFormula.checkCertificate A a.all h x_2 x_3 x_4 = (x_4.isEmpty && Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A a.all ⋯ x_2 x_3)
• Complexity.DescriptiveComplexity.SOFormula.checkCertificate A (Complexity.DescriptiveComplexity.SOFormula.soAll k a) h x_2 x_3 x_4 = False.elim h

def Complexity.DescriptiveComplexity.SOSentence.checkEncoded {V : Vocabulary} (φ : SOSentence V) (h : SOFormula.IsExistSO φ) (input certificate : List Bool) : Bool

Check an existential-SO sentence's binary certificate on an encoded structure.

Equations

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