Verified checking of first-order matrices with relation witnesses

Boolean relation environments represent exactly the propositional relation environments. The computable matrix evaluator agrees with SO satisfaction and with the existing FO evaluator on embedded formulas. Existence of semantic relation witnesses is equivalent to existence of Boolean tables accepted by the evaluator, including nullary relations and empty contexts.

This supplies the logical verification interface for Immerman, Proposition 7.6. SecondOrder.Certificate extends it to binary witnesses with exact length bounds. SecondOrder.PolynomialTime gives arithmetic evaluation with the same verdict and proves its polynomial-time machine bound on encoded tables.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.toREnv_empty (card : Nat) : (empty card).toREnv = emptyREnv card

Converting the empty Boolean environment gives the empty semantic environment.

@[simp]

theorem Complexity.DescriptiveComplexity.DecREnv.toREnv_cons {card k : Nat} {rctx : List Nat} (S : (Fin k → Fin card) → Bool) (ρ : DecREnv card rctx) : (cons S ρ).toREnv = rCons (fun (args : Fin k → Fin card) => S args = true) ρ.toREnv

Boolean environment extension represents semantic environment extension.

theorem Complexity.DescriptiveComplexity.DecREnv.toREnv_injective (card : Nat) (rctx : List Nat) : Function.Injective toREnv

Distinct Boolean relation environments have distinct propositional meanings.

theorem Complexity.DescriptiveComplexity.DecREnv.toREnv_surjective (card : Nat) (rctx : List Nat) : Function.Surjective toREnv

Every semantic relation environment has a Boolean representation.

theorem Complexity.DescriptiveComplexity.SOFormula.evalMatrixB_eq_sat {V : Vocabulary} {rctx : List Nat} {n : Nat} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (σ : Env A.card n) (ρ : DecREnv A.card rctx) : evalMatrixB A φ h σ ρ = true ↔ Sat A.toFinStruct σ ρ.toREnv φ

Matrix evaluation agrees with satisfaction under the represented relation tables.

theorem Complexity.DescriptiveComplexity.SOFormula.evalMatrixB_ofFormula {V : Vocabulary} {rctx : List Nat} {n : Nat} (A : DecFinStruct V) (φ : Formula V n) (σ : Env A.card n) (ρ : DecREnv A.card rctx) : evalMatrixB A (ofFormula φ rctx) ⋯ σ ρ = Formula.evalB A σ φ

Matrix evaluation extends the existing FO evaluator exactly.

def Complexity.DescriptiveComplexity.SOFormula.decidableMatrixSat {V : Vocabulary} {rctx : List Nat} {n : Nat} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (σ : Env A.card n) (ρ : DecREnv A.card rctx) : Decidable (Sat A.toFinStruct σ ρ.toREnv φ)

Checking an FO matrix with supplied Boolean tables is decidable without classical choice.

Equations

• Complexity.DescriptiveComplexity.SOFormula.decidableMatrixSat A φ h σ ρ = decidable_of_iff (Complexity.DescriptiveComplexity.SOFormula.evalMatrixB A φ h σ ρ = true) ⋯

theorem Complexity.DescriptiveComplexity.SOFormula.exists_evalMatrixB_iff {V : Vocabulary} {rctx : List Nat} {n : Nat} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (σ : Env A.card n) : (∃ (ρ : DecREnv A.card rctx), evalMatrixB A φ h σ ρ = true) ↔ ∃ (ρ : REnv A.card rctx), Sat A.toFinStruct σ ρ φ

Boolean tables are complete existential witnesses for an FO matrix.

theorem Complexity.DescriptiveComplexity.SOFormula.forall_evalMatrixB_iff {V : Vocabulary} {rctx : List Nat} {n : Nat} (A : DecFinStruct V) (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (σ : Env A.card n) : (∀ (ρ : DecREnv A.card rctx), evalMatrixB A φ h σ ρ = true) ↔ ∀ (ρ : REnv A.card rctx), Sat A.toFinStruct σ ρ φ

Universal matrix truth can also be checked over Boolean relation assignments.