Boolean relation environments and FO-matrix evaluation

Existential SO witnesses supply relation tables. DecREnv presents those tables as Boolean functions, while toREnv gives their propositional meaning. A matrix evaluator reads both the vocabulary relations and these supplied relations; first-order quantifiers enumerate the finite universe.

The evaluator requires an IsFOMatrix certificate, so its interface excludes second-order quantifiers. This is the verification step in Immerman's Descriptive Complexity, Section 7.1, Proposition 7.6. SecondOrder.Certificate supplies the binary certificate format; SecondOrder.PolynomialTime proves polynomial-time checking against the machine definitions.

def Complexity.DescriptiveComplexity.DecREnv (card : Nat) (rctx : List Nat) : Type

Boolean truth tables for the relation variables in a fixed arity context.

Equations

• Complexity.DescriptiveComplexity.DecREnv card rctx = ((r : Fin rctx.length) → (Fin (rctx.get r) → Fin card) → Bool)

def Complexity.DescriptiveComplexity.DecREnv.toREnv {card : Nat} {rctx : List Nat} (ρ : DecREnv card rctx) : REnv card rctx

Interpret the supplied Boolean tables as propositional relations.

Equations

• ρ.toREnv r args = (ρ r args = true)

def Complexity.DescriptiveComplexity.DecREnv.empty (card : Nat) : DecREnv card []

The unique Boolean relation environment for an empty context.

Equations

• Complexity.DescriptiveComplexity.DecREnv.empty card r = r.elim0

def Complexity.DescriptiveComplexity.DecREnv.cons {card k : Nat} {rctx : List Nat} (S : (Fin k → Fin card) → Bool) (ρ : DecREnv card rctx) : DecREnv card (k :: rctx)

Supply a fresh Boolean relation at de Bruijn index zero.

Equations

• Complexity.DescriptiveComplexity.DecREnv.cons S ρ ⟨0, isLt⟩ = S
• Complexity.DescriptiveComplexity.DecREnv.cons S ρ ⟨i.succ, h⟩ = ρ ⟨i, ⋯⟩

def Complexity.DescriptiveComplexity.SOFormula.evalMatrixB {V : Vocabulary} (A : DecFinStruct V) {rctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) : φ.IsFOMatrix → Env A.card n → DecREnv A.card rctx → Bool

Evaluate an FO matrix with supplied Boolean relation tables and element values.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A φ.neg h x_2 x_3 = !Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A φ h x_2 x_3
• Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A (Complexity.DescriptiveComplexity.SOFormula.soExist k a) h x_2 x_3 = False.elim h
• Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A (Complexity.DescriptiveComplexity.SOFormula.soAll k a) h x_2 x_3 = False.elim h