Constant-domain Kripke semantics

[UPSTREAM] candidates for Mathlib/ModelTheory, which is classical: one structure, no accessibility. A ModalStructure L W M — the modal analogue of L.Structure — is a W-indexed family of L-structures on a constant domain M together with Finset-valued accessibility; ModalFormula L α is the quantified modal language in BoundedFormula's basis, and ModalFormula.Realize is Kripke satisfaction K, w ⊨_v φ.

Main declarations

• ModalStructure — accessibility plus a world-indexed family of first-order structures on a constant domain, so that terms and plain formulas realize at a world by Term.realizeAt and Formula.RealizeAt.
• ModalFormula.Realize — Kripke satisfaction for the modal language of Syntax.lean, with the realize_* simp set and the Barcan laws.

Implementation notes

• Accessibility is Finset-valued (computability-first, matching the team-semantics consumers); generalize to a Prop-valued relation when a consumer needs infinite branching.
• ModalFormula quantifiers bind named variables with Function.update semantics (the Formula.all₁ / ex₁ convention of Core/ModelTheory/Binders.lean), not de Bruijn indices: the modal layer's consumers carry named variables.

References

• [FM23] — constant-domain models, world-relative interpretation, the Barcan formulas

structure FirstOrder.Language.ModalStructure (L : Language) (W : Type u_4) (M : Type u_5) : Type (max (max (max u_4 u_5) u_6) u_7)

A structure for the quantified modal language — the model object of constant-domain Kripke semantics: Finset-valued accessibility plus a W-indexed family of L-structures on the domain M.

• access : W → Finset W

  Accessibility relation (per-world set of accessible worlds).

• interp : W → L.Structure M

  World-indexed interpretation of the signature.

World-relative interpretation

The interpretation function I(w)(·) of first-order modal semantics ([FM23] Definition 8.6.2): what a symbol denotes at a world, read off the world's structure.

def FirstOrder.Language.ModalStructure.relInterp {L : Language} {W : Type u_1} {M : Type u_2} (K : L.ModalStructure W M) {n : ℕ} (R : L.Relations n) (w : W) : (Fin n → M) → Prop

The relation a relation symbol denotes at a world.

Equations

• K.relInterp R w = FirstOrder.Language.Structure.RelMap R

def FirstOrder.Language.ModalStructure.funInterp {L : Language} {W : Type u_1} {M : Type u_2} (K : L.ModalStructure W M) {n : ℕ} (f : L.Functions n) (w : W) : (Fin n → M) → M

The function a function symbol denotes at a world.

Equations

• K.funInterp f w = FirstOrder.Language.Structure.funMap f

def FirstOrder.Language.ModalStructure.relInterp₁ {L : Language} {W : Type u_1} {M : Type u_2} (K : L.ModalStructure W M) (R : L.Relations 1) (w : W) (d : M) : Prop

The relation a unary relation symbol denotes at a world, curried.

Equations

• K.relInterp₁ R w d = K.relInterp R w fun (x : Fin 1) => d

def FirstOrder.Language.ModalStructure.constInterp {L : Language} {W : Type u_1} {M : Type u_2} (K : L.ModalStructure W M) (c : L.Constants) (w : W) : M

The element a constant denotes at a world.

Equations

• K.constInterp c w = K.funInterp c w default

theorem FirstOrder.Language.ModalStructure.realizeAt_constants {L : Language} {W : Type u_1} {M : Type u_2} (K : L.ModalStructure W M) {α : Type u_4} (w : W) (v : α → M) (c : L.Constants) : c.term.realizeAt K.interp w v = K.constInterp c w

A constant term's value at a world is its constInterp denotation.

theorem FirstOrder.Language.ModalStructure.realizeAt_rel₁ {L : Language} {W : Type u_1} {M : Type u_2} (K : L.ModalStructure W M) {α : Type u_4} (w : W) (v : α → M) (R : L.Relations 1) (t : L.Term α) : (R.formula₁ t).RealizeAt K.interp w v ↔ K.relInterp₁ R w (t.realizeAt K.interp w v)

A unary atom of a plain formula holds at a world when the symbol's denotation there holds of the term's value.

def FirstOrder.Language.ModalFormula.Realize {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) : W → L.ModalFormula α → (α → M) → Prop

Kripke satisfaction K, w ⊨_v φ, under which atoms evaluate at the world's structure, □ quantifies over accessible worlds, and named quantifiers update the valuation.

Equations

• FirstOrder.Language.ModalFormula.Realize K x✝¹ (FirstOrder.Language.ModalFormula.equal t₁ t₂) x✝ = (t₁.realizeAt K.interp x✝¹ x✝ = t₂.realizeAt K.interp x✝¹ x✝)
• FirstOrder.Language.ModalFormula.Realize K x✝¹ (FirstOrder.Language.ModalFormula.rel R ts) x✝ = K.relInterp R x✝¹ fun (i : Fin n) => (ts i).realizeAt K.interp x✝¹ x✝
• FirstOrder.Language.ModalFormula.Realize K x✝¹ FirstOrder.Language.ModalFormula.falsum x✝ = False
• FirstOrder.Language.ModalFormula.Realize K x✝¹ (φ.imp ψ) x✝ = (FirstOrder.Language.ModalFormula.Realize K x✝¹ φ x✝ → FirstOrder.Language.ModalFormula.Realize K x✝¹ ψ x✝)
• FirstOrder.Language.ModalFormula.Realize K x✝¹ φ.box x✝ = ∀ w' ∈ K.access x✝¹, FirstOrder.Language.ModalFormula.Realize K w' φ x✝
• FirstOrder.Language.ModalFormula.Realize K x✝¹ (FirstOrder.Language.ModalFormula.all x_3 φ) x✝ = ∀ (d : M), FirstOrder.Language.ModalFormula.Realize K x✝¹ φ (Function.update x✝ x_3 d)

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_equal {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (t₁ t₂ : L.Term α) : Realize K w (equal t₁ t₂) v ↔ t₁.realizeAt K.interp w v = t₂.realizeAt K.interp w v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_rel {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) {n : ℕ} (R : L.Relations n) (ts : Fin n → L.Term α) : Realize K w (rel R ts) v ↔ K.relInterp R w fun (i : Fin n) => (ts i).realizeAt K.interp w v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_bot {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) : Realize K w ⊥ v ↔ False

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_imp {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (φ ψ : L.ModalFormula α) : Realize K w (φ.imp ψ) v ↔ Realize K w φ v → Realize K w ψ v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_not {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (φ : L.ModalFormula α) : Realize K w φ.not v ↔ ¬Realize K w φ v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_top {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) : Realize K w ⊤ v ↔ True

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_inf {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (φ ψ : L.ModalFormula α) : Realize K w (φ ⊓ ψ) v ↔ Realize K w φ v ∧ Realize K w ψ v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_sup {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (φ ψ : L.ModalFormula α) : Realize K w (φ ⊔ ψ) v ↔ Realize K w φ v ∨ Realize K w ψ v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_box {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (φ : L.ModalFormula α) : Realize K w φ.box v ↔ ∀ w' ∈ K.access w, Realize K w' φ v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_all {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (x : α) (φ : L.ModalFormula α) : Realize K w (all x φ) v ↔ ∀ (d : M), Realize K w φ (Function.update v x d)

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_ex {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (x : α) (φ : L.ModalFormula α) : Realize K w (ModalFormula.ex x φ) v ↔ ∃ (d : M), Realize K w φ (Function.update v x d)

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_diamond {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (φ : L.ModalFormula α) : Realize K w φ.diamond v ↔ ∃ w' ∈ K.access w, Realize K w' φ v

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_rel₁ {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (R : L.Relations 1) (t : L.Term α) : Realize K w (R.modalFormula₁ t) v ↔ K.relInterp₁ R w (t.realizeAt K.interp w v)

A unary atom holds at a world when the symbol's denotation there holds of the term's value.

The Barcan laws

Constant domains validate the Barcan formula and its converse: □ and ∀ are both world-independent universal quantifiers, so they commute.

theorem FirstOrder.Language.ModalFormula.realize_barcan {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (x : α) (φ : L.ModalFormula α) : Realize K w (all x φ.box) v → Realize K w (all x φ).box v

The Barcan formula ∀x □φ → □ ∀x φ.

theorem FirstOrder.Language.ModalFormula.realize_converseBarcan {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.ModalStructure W M) (w : W) (v : α → M) (x : α) (φ : L.ModalFormula α) : Realize K w (all x φ).box v → Realize K w (all x φ.box) v

The converse Barcan formula □ ∀x φ → ∀x □φ.