Satisfaction: dependence, decidability, and families of structures

This file shows that the value of a term depends only on its variables, and that first-order satisfaction is decidable on a finite structure with decidable equality and decidable relations, so that decide checks Realize facts on concrete finite models. It also realizes terms and formulas at an index of a family interp : W → L.Structure M of structures on one carrier, such as the world-indexed interpretation of a constant-domain Kripke model, where mathlib's instance-based realize needs the instance chosen at each index.

Main definitions

• FirstOrder.Language.BoundedFormula.decidableRealize decides BoundedFormula.Realize by recursion on the formula, and FirstOrder.Language.Formula.decidableRealize is the same for formulas.
• FirstOrder.Language.Term.realizeAt, FirstOrder.Language.Formula.RealizeAt: realization in the structure a family carries at an index.

Main results

• FirstOrder.Language.Term.dependsOn_realize: a term's value depends only on its variables.

theorem FirstOrder.Language.Term.dependsOn_realize {L : Language} {M : Type u_1} [L.Structure M] {α : Type u_2} [DecidableEq α] (t : L.Term α) : DependsOn (fun (v : α → M) => realize v t) ↑t.varFinset

[UPSTREAM] The value of a term depends only on the values of its variables.

@[instance_reducible]

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

Satisfaction on a finite structure with decidable equality and decidable relations is decidable, by recursion on the formula; decide reduces through it on concrete models.

Equations

• FirstOrder.Language.BoundedFormula.falsum.decidableRealize x✝¹ x✝ = isFalse ⋯
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).decidableRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decidableRealize._aux_1 x✝² t₁ t₂ x✝¹ x✝
• (FirstOrder.Language.BoundedFormula.rel R ts).decidableRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decidableRealize._aux_3 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 (a : M) => φ.Realize x✝¹ (Fin.snoc x✝ a)) a), reflects_decide := ⋯ }

@[instance_reducible]

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

Equations

• φ.decidableRealize v = FirstOrder.Language.BoundedFormula.decidableRealize φ v default

Realization in a family of structures

def FirstOrder.Language.Term.realizeAt {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (t : L.Term α) (interp : W → L.Structure M) (w : W) (v : α → M) : M

[UPSTREAM] The value of a term in the structure the family carries at w.

Equations

• t.realizeAt interp w v = FirstOrder.Language.Term.realize v t

def FirstOrder.Language.Formula.RealizeAt {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (ψ : L.Formula α) (interp : W → L.Structure M) (w : W) (v : α → M) : Prop

[UPSTREAM] Satisfaction in the structure the family carries at w.

Equations

• ψ.RealizeAt interp w v = ψ.Realize v

@[simp]

theorem FirstOrder.Language.Term.realizeAt_var {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (a : α) : (var a).realizeAt interp w v = v a

@[simp]

theorem FirstOrder.Language.Term.realizeAt_constants {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (c : L.Constants) : c.term.realizeAt interp w v = Structure.funMap c default

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_not {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (ψ : L.Formula α) : ψ.not.RealizeAt interp w v ↔ ¬ψ.RealizeAt interp w v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_inf {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (ψ₁ ψ₂ : L.Formula α) : (ψ₁ ⊓ ψ₂).RealizeAt interp w v ↔ ψ₁.RealizeAt interp w v ∧ ψ₂.RealizeAt interp w v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_sup {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (ψ₁ ψ₂ : L.Formula α) : (ψ₁ ⊔ ψ₂).RealizeAt interp w v ↔ ψ₁.RealizeAt interp w v ∨ ψ₂.RealizeAt interp w v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_imp {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (ψ₁ ψ₂ : L.Formula α) : (ψ₁.imp ψ₂).RealizeAt interp w v ↔ ψ₁.RealizeAt interp w v → ψ₂.RealizeAt interp w v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_rel₁ {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (R : L.Relations 1) (t : L.Term α) : (R.formula₁ t).RealizeAt interp w v ↔ Structure.RelMap R ![t.realizeAt interp w v]

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_rel₂ {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (R : L.Relations 2) (t₁ t₂ : L.Term α) : (R.formula₂ t₁ t₂).RealizeAt interp w v ↔ Structure.RelMap R ![t₁.realizeAt interp w v, t₂.realizeAt interp w v]