Evaluating a formula on a concrete structure is primitive recursive

The engine of the bridge: for every fixed first-order formula φ over a finitely presented relational vocabulary, the function

(concrete structure, valuation) ↦ does φ hold?

is primitive recursive (FirstOrder.Language.FinStruct.primrec_evalBF) and computes satisfaction (FirstOrder.Language.FinStruct.evalBF_iff).

Everything downstream is an application: an ∃SO[new] definition becomes an unbounded search whose test is this evaluation (DescriptiveComplexity.RE_subset_rePred), and a first-order interpretation becomes a computable map of concrete structures, because its image relations are evaluations of fixed formulas.

Why an explicit Boolean evaluator

FirstOrder.Language.BoundedFormula.decidableRealize already decides satisfaction, but Primrec is a statement about a function, not about a Decidable instance, and the quantifier case of that instance goes through Fintype.decidableForallFintype, which is not in a shape any Primrec combinator matches. evalBF is the same recursion written so that each case is a combinator application: a list lookup for an atom, a Boolean combinator for an implication, and a conjunction over List.range for a quantifier.

Valuations are List ℕ – the values of the bound variables, in de Bruijn order – rather than Fin l → Univ: a dependent function type would be encoded, at every recursive call, into exactly this list.

Two primitive recursive helpers

def FirstOrder.Language.andAll (l : List Bool) : Bool

The conjunction of a list of Booleans.

Equations

• FirstOrder.Language.andAll l = List.foldr (fun (x1 x2 : Bool) => x1 && x2) true l

@[simp]

theorem FirstOrder.Language.andAll_nil : andAll [] = true

@[simp]

theorem FirstOrder.Language.andAll_cons (b : Bool) (l : List Bool) : andAll (b :: l) = (b && andAll l)

theorem FirstOrder.Language.andAll_eq_true {l : List Bool} : andAll l = true ↔ ∀ b ∈ l, b = true

theorem FirstOrder.Language.primrec_andAll : Primrec andAll

theorem FirstOrder.Language.tupleIdx_eq_foldr (c : ℕ) (l : List ℕ) : tupleIdx c l = List.foldr (fun (a r : ℕ) => a + c * r) 0 l

theorem FirstOrder.Language.primrec_tupleIdx : Primrec₂ tupleIdx

theorem FirstOrder.Language.primrec_pow_const (j : ℕ) : Primrec fun (c : ℕ) => c ^ j

theorem FirstOrder.Language.primrec_digitAt (j : ℕ) : Primrec₂ fun (c t : ℕ) => digitAt c t j

Valuations as lists

def FirstOrder.Language.FinStruct.valNat {L : Language} {V : L.FinVocab} (s : FinStruct V) (xs : List ℕ) (i : ℕ) : ℕ

The value of the i-th bound variable, as a number: out-of-range variables read 0, and the reduction modulo the size of the universe makes the reading total.

Equations

• s.valNat xs i = xs.getD i 0 % s.card

def FirstOrder.Language.FinStruct.valOf {L : Language} {V : L.FinVocab} (s : FinStruct V) (xs : List ℕ) (i : ℕ) : s.Univ

The value of the i-th bound variable, as an element of the universe.

Equations

• s.valOf xs i = ⟨s.valNat xs i, ⋯⟩

@[simp]

theorem FirstOrder.Language.FinStruct.val_valOf {L : Language} {V : L.FinVocab} (s : FinStruct V) (xs : List ℕ) (i : ℕ) : ↑(s.valOf xs i) = s.valNat xs i

theorem FirstOrder.Language.FinStruct.primrec_valNat {L : Language} (V : L.FinVocab) (k : ℕ) : Primrec fun (p : FinStruct V × List ℕ) => p.1.valNat p.2 k

theorem FirstOrder.Language.FinStruct.valOf_append {L : Language} {V : L.FinVocab} {l : ℕ} (s : FinStruct V) (xs : List ℕ) (hlen : xs.length = l) (y : s.Univ) : (fun (i : Fin (l + 1)) => s.valOf (xs ++ [↑y]) ↑i) = Fin.snoc (fun (i : Fin l) => s.valOf xs ↑i) y

Appending a value to a valuation is Fin.snoc on the elements it denotes.

Terms

Over a relational vocabulary a term is a variable, so its value is the value of a bound variable whose number is fixed by the term: nothing about a term has to be computed at run time.

def FirstOrder.Language.FinStruct.termIdx {L : Language} [L.IsRelational] {l : ℕ} : L.Term (Empty ⊕ Fin l) → ℕ

The number of the bound variable a term is.

Equations

• FirstOrder.Language.FinStruct.termIdx (FirstOrder.Language.var (Sum.inl e)) = e.elim
• FirstOrder.Language.FinStruct.termIdx (FirstOrder.Language.var (Sum.inr i)) = ↑i
• FirstOrder.Language.FinStruct.termIdx (FirstOrder.Language.func f _ts) = isEmptyElim f

theorem FirstOrder.Language.FinStruct.realize_term {L : Language} [L.IsRelational] {V : L.FinVocab} {l : ℕ} (s : FinStruct V) (xs : List ℕ) (t : L.Term (Empty ⊕ Fin l)) : Term.realize (Sum.elim Empty.elim fun (i : Fin l) => s.valOf xs ↑i) t = s.valOf xs (termIdx t)

The evaluator

def FirstOrder.Language.FinStruct.evalBF {L : Language} [L.IsRelational] (V : L.FinVocab) {l : ℕ} : L.BoundedFormula Empty l → FinStruct V → List ℕ → Bool

The Boolean evaluator: the recursion on the formula that FirstOrder.Language.FinStruct.primrec_evalBF shows to be primitive recursive and FirstOrder.Language.FinStruct.evalBF_iff shows to compute satisfaction.

An atom is a lookup in the table of the instance, at the number of the tuple of values; a quantifier is a conjunction over List.range card, the values a variable can take.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.FinStruct.evalBF V FirstOrder.Language.BoundedFormula.falsum x✝¹ x✝ = false
• FirstOrder.Language.FinStruct.evalBF V (φ.imp ψ) x✝¹ x✝ = (!FirstOrder.Language.FinStruct.evalBF V φ x✝¹ x✝ || FirstOrder.Language.FinStruct.evalBF V ψ x✝¹ x✝)
• FirstOrder.Language.FinStruct.evalBF V φ.all x✝¹ x✝ = FirstOrder.Language.andAll (List.map (fun (x : ℕ) => FirstOrder.Language.FinStruct.evalBF V φ x✝¹ (x✝ ++ [x])) (List.range x✝¹.card))

theorem FirstOrder.Language.FinStruct.evalBF_iff {L : Language} [L.IsRelational] (V : L.FinVocab) {l : ℕ} (φ : L.BoundedFormula Empty l) (s : FinStruct V) (xs : List ℕ) : xs.length = l → (evalBF V φ s xs = true ↔ φ.Realize Empty.elim fun (i : Fin l) => s.valOf xs ↑i)

The evaluator computes satisfaction.

theorem FirstOrder.Language.FinStruct.primrec_evalBF {L : Language} [L.IsRelational] (V : L.FinVocab) {l : ℕ} (φ : L.BoundedFormula Empty l) : Primrec fun (p : FinStruct V × List ℕ) => evalBF V φ p.1 p.2

The evaluator is primitive recursive, uniformly in the instance and the valuation, for each fixed formula.

Sentences

A sentence is the case l = 0 of the evaluator, with the empty valuation.

theorem FirstOrder.Language.FinStruct.primrec_evalSentence {L : Language} [L.IsRelational] (V : L.FinVocab) (φ : L.Sentence) : Primrec fun (s : FinStruct V) => evalBF V φ s []

Deciding a fixed sentence on a concrete structure is primitive recursive.

theorem FirstOrder.Language.FinStruct.evalSentence_iff {L : Language} [L.IsRelational] (V : L.FinVocab) (φ : L.Sentence) (s : FinStruct V) : evalBF V φ s [] = true ↔ s.Univ ⊨ φ

The evaluator decides a sentence.