Deciding first-order satisfaction on a finite structure

The first step of the bridge to Mathlib's computability layer: on a finite structure whose relations are decidable and whose equality is decidable, FirstOrder.Language.BoundedFormula.Realize is decidable, by recursion on the formula – quantifiers going through Fintype.decidableForallFintype.

Mathlib has no such instance (Realize is a Prop-valued recursion, and Mathlib's model theory never needs to run it), so it is supplied here. It is the first formal justification of the claim, elsewhere by inspection, that first-order interpretations are effective: everything a reduction of this library computes is an evaluation of a fixed formula in a finite structure.

The instance is deliberately independent of the rest of the bridge: it mentions no encoding of structures, and it is useful on its own wherever a first-order condition has to be checked by decide.

@[instance_reducible]

instance FirstOrder.Language.BoundedFormula.decidableRealize {L : Language} {α : Type u_1} {M : Type u_2} [L.Structure M] [DecidableEq M] [Fintype M] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → M) → Decidable (Structure.RelMap R x)] {l : ℕ} (φ : L.BoundedFormula α l) (v : α → M) (xs : Fin l → M) : Decidable (φ.Realize v xs)

Satisfaction is decidable on a finite structure whose relations and whose equality are decidable: a recursion on the formula, the quantifier case being a decidable quantification over a Fintype.

The realization of a term needs no hypothesis: it is an ordinary function into the universe, and only the equality test it feeds needs DecidableEq M.

Equations

• FirstOrder.Language.BoundedFormula.falsum.decidableRealize x✝¹ x✝ = { decide := false, reflects_decide := ⋯ }
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).decidableRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decidableRealize._aux_2 x✝² t₁ t₂ x✝¹ x✝
• (FirstOrder.Language.BoundedFormula.rel R ts).decidableRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decidableRealize._aux_4 x✝² l R ts x✝¹ x✝
• (φ₁.imp φ₂).decidableRealize x✝¹ x✝ = { decide := if h : φ₁.Realize x✝¹ x✝ then decide ((fun (a : φ₁.Realize x✝¹ x✝) => φ₂.Realize x✝¹ x✝) h) else true, reflects_decide := ⋯ }
• φ.all.decidableRealize x✝¹ x✝ = { decide := decide (∀ a ∈ Finset.univ, (fun (_x : M) => φ.Realize x✝¹ (Fin.snoc x✝ _x)) a), reflects_decide := ⋯ }

@[instance_reducible]

instance FirstOrder.Language.Formula.decidableRealize {L : Language} {α : Type u_1} {M : Type u_2} [L.Structure M] [DecidableEq M] [Fintype M] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → M) → Decidable (Structure.RelMap R x)] (φ : L.Formula α) (v : α → M) : Decidable (φ.Realize v)

Satisfaction of a formula (no bound variables left) is decidable on a finite structure with decidable relations.

Equations

• φ.decidableRealize v = FirstOrder.Language.Formula.decidableRealize._aux_1 φ v

@[instance_reducible]

instance FirstOrder.Language.Sentence.decidableRealize {L : Language} {M : Type u_1} [L.Structure M] [DecidableEq M] [Fintype M] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → M) → Decidable (Structure.RelMap R x)] (φ : L.Sentence) : Decidable (M ⊨ φ)

Satisfaction of a sentence is decidable on a finite structure with decidable relations.

Equations

• φ.decidableRealize = FirstOrder.Language.Sentence.decidableRealize._aux_1 φ