Constant-domain first-order Kripke structures and modal formulas

Mathlib's ModelTheory is classical: one structure, no accessibility. A KripkeStructure L W M is a W-indexed family of L-structures on a constant domain M together with Finset-valued accessibility — the shape Semantics/Composition/Model.lean (without accessibility) and Core/Logic/Modal/QBSML/Defs.lean already instantiate. On top, ModalFormula L α layers □ and named quantifiers over embedded classical L.Formulas, and ModalFormula.Realize is Kripke satisfaction K, w ⊨_v φ. Upstream candidates.

Main declarations

• KripkeStructure — accessibility plus a world-indexed family of first-order structures on a constant domain.
• KripkeStructure.RealizeAt — classical satisfaction at a world, with the transported Formula.realize_* simp set.
• ModalFormula, ModalFormula.Realize — modal formulas over embedded classical formulas, and Kripke satisfaction; ModalFormula.dia is the derived ◇ := ¬□¬.

Implementation notes

• Structures are carried as terms, not instances — a world-indexed family cannot be instance-based — so interfacing with instance-based mathlib API (Formula.Realize) threads letI := K.interp w.
• 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/Logic/FirstOrder/Binders.lean), not de Bruijn indices: the modal layer's consumers carry named variables, and the embedding of classical formulas via ofFormula makes satisfaction commute by construction (ModalFormula.realize_ofFormula is Iff.rfl).

structure FirstOrder.Language.KripkeStructure (L : Language) (W : Type u_4) (M : Type u_5) : Type (max (max (max u u_4) u_5) v)

A constant-domain first-order Kripke structure: 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.

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

Classical first-order satisfaction at a world — K, w ⊨_v ψ, mathlib's Formula.Realize in the structure the Kripke structure carries at w.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.KripkeStructure.realizeAt_all₁ {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.KripkeStructure W M) (w : W) (x : α) (ψ : L.Formula α) (v : α → M) : K.RealizeAt w (Formula.all₁ x ψ) v ↔ ∀ (d : M), K.RealizeAt w ψ (Function.update v x d)

@[simp]

theorem FirstOrder.Language.KripkeStructure.realizeAt_ex₁ {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.KripkeStructure W M) (w : W) (x : α) (ψ : L.Formula α) (v : α → M) : K.RealizeAt w (Formula.ex₁ x ψ) v ↔ ∃ (d : M), K.RealizeAt w ψ (Function.update v x d)

inductive FirstOrder.Language.ModalFormula (L : Language) (α : Type u_4) : Type (max (max u u_4) v)

Modal formulas over L with named free variables α: classical L.Formulas embedded wholesale via ofFormula, closed under the connectives, □, and named quantifiers (◇ is derived — ModalFormula.dia).

• ofFormula {L : Language} {α : Type u_4} : L.Formula α → L.ModalFormula α

  An embedded classical (modal-free) formula.

• not {L : Language} {α : Type u_4} : L.ModalFormula α → L.ModalFormula α

  Negation.

• inf {L : Language} {α : Type u_4} : L.ModalFormula α → L.ModalFormula α → L.ModalFormula α

  Conjunction.

• sup {L : Language} {α : Type u_4} : L.ModalFormula α → L.ModalFormula α → L.ModalFormula α

  Disjunction.

• box {L : Language} {α : Type u_4} : L.ModalFormula α → L.ModalFormula α

  Necessity.

• all {L : Language} {α : Type u_4} : α → L.ModalFormula α → L.ModalFormula α

  Universal quantification of a named variable.

• ex {L : Language} {α : Type u_4} : α → L.ModalFormula α → L.ModalFormula α

  Existential quantification of a named variable.

def FirstOrder.Language.ModalFormula.dia {L : Language} {α : Type u_3} (φ : L.ModalFormula α) : L.ModalFormula α

Possibility, derived: ◇φ := ¬□¬φ.

Equations

• φ.dia = φ.not.box.not

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

Kripke satisfaction K, w ⊨_v φ: classical formulas 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.ofFormula ψ) x✝ = K.RealizeAt x✝¹ ψ x✝
• FirstOrder.Language.ModalFormula.Realize K x✝¹ φ.not x✝ = ¬FirstOrder.Language.ModalFormula.Realize K x✝¹ φ x✝
• FirstOrder.Language.ModalFormula.Realize K x✝¹ (φ.inf ψ) x✝ = (FirstOrder.Language.ModalFormula.Realize K x✝¹ φ x✝ ∧ FirstOrder.Language.ModalFormula.Realize K x✝¹ ψ x✝)
• FirstOrder.Language.ModalFormula.Realize K x✝¹ (φ.sup ψ) 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)
• FirstOrder.Language.ModalFormula.Realize K x✝¹ (FirstOrder.Language.ModalFormula.ex x_3 φ) x✝ = ∃ (d : M), FirstOrder.Language.ModalFormula.Realize K x✝¹ φ (Function.update x✝ x_3 d)

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_ofFormula {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.KripkeStructure W M) (w : W) (v : α → M) (ψ : L.Formula α) : Realize K w (ofFormula ψ) v ↔ K.RealizeAt w ψ v

Embedded classical formulas realize classically — by construction.

@[simp]

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

@[simp]

theorem FirstOrder.Language.ModalFormula.realize_inf {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} [DecidableEq α] (K : L.KripkeStructure W M) (w : W) (v : α → M) (φ ψ : L.ModalFormula α) : Realize K w (φ.inf ψ) 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.KripkeStructure W M) (w : W) (v : α → M) (φ ψ : L.ModalFormula α) : Realize K w (φ.sup ψ) 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.KripkeStructure 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.KripkeStructure 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.KripkeStructure W M) (w : W) (v : α → M) (x : α) (φ : L.ModalFormula α) : Realize K w (ex x φ) v ↔ ∃ (d : M), Realize K w φ (Function.update v x d)

@[simp]

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