The standard translation for monadic quantified modal logic

[BdRV01] [AvO23]

The standard translation of modal logic into first-order logic ([BdRV01]), for the monadic signature: modal formulas over monadicLang Const Pred translate into plain mathlib first-order formulas over stLang Const Pred — accessibility as a binary relation, predicates world-relativized to binary relations, constants world-indexed to unary functions, and an individual-sort predicate — interpreted on the two-sorted-as-one carrier W ⊕ M. realize_st? is satisfaction preservation; composed with Proposition 4.1, the support relation of NE-free QBSML bottoms out in single-structure mathlib first-order satisfaction (support_singleton_iff_st).

Main declarations

• stLang — the target signature; KripkeStructure.stStructure — the W ⊕ M encoding of a Kripke structure as one mathlib structure.
• ModalFormula.st? — the standard translation, with the current world as the free variable Sum.inr k and box introducing the fresh world variable Sum.inr (k + 1) (partial: embedded classical formulas translate when atomic, which covers all toModal? images).
• realize_st? — satisfaction preservation: Kripke satisfaction at w is first-order realization over stStructure at any sorted valuation pinning Sum.inr k to w.
• support_singleton_iff_st — NE-free QBSML support is first-order realization of the standard translation, via Proposition 4.1.
• stClose — sort-guarded existential closure of the current-world variable, turning translations into sentence candidates.
• support_compactness — compactness transfer: finite team satisfiability of an NE-free family yields one first-order structure satisfying all closed translations.

Implementation notes

• The valuation in realize_st? is an arbitrary val : Var ⊕ ℕ → W ⊕ M constrained only at individual variables and at the current world index — quantifiers in the translation range over the full mixed carrier, with off-sort values discharged by the relational guards, so no Sum.elim-update commutation is needed in the induction.
• Freshness of world variables is by increment: each box shifts the current index from k to k + 1, and the constraint set of the theorem pins only index k, so no freshness side conditions arise.
• The compactness transfer is one-way: recovering a team model from an arbitrary first-order structure would need Finset-branching accessibility and a Fintype domain. freeVarFinset = ∅ side conditions are hypotheses, dischargeable by decide per instance — no generic free-variable bookkeeping for st?.

The target signature and the encoded structure

def Core.Logic.Modal.QBSML.stLang (Const : Type u) (Pred : Type v) : FirstOrder.Language

The standard-translation target signature: world-indexed constants as unary functions, an individual-sort predicate (unary), and world-relativized monadic predicates plus accessibility (binary).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.stConst {Const : Type u_6} {Pred : Type u_7} (c : Const) : (stLang Const Pred).Functions 1

A constant as a unary function symbol of the target signature.

Equations

• Core.Logic.Modal.QBSML.stConst c = c

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.stIndiv {Const : Type u_6} {Pred : Type u_7} : (stLang Const Pred).Relations 1

The individual-sort predicate.

Equations

• Core.Logic.Modal.QBSML.stIndiv = PUnit.unit

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.stRel {Const : Type u_6} {Pred : Type u_7} (P : Pred) : (stLang Const Pred).Relations 2

A predicate as a world-relativized binary relation symbol.

Equations

• Core.Logic.Modal.QBSML.stRel P = Sum.inl P

@[reducible, inline]

abbrev Core.Logic.Modal.QBSML.stAcc {Const : Type u_6} {Pred : Type u_7} : (stLang Const Pred).Relations 2

The accessibility relation symbol.

Equations

• Core.Logic.Modal.QBSML.stAcc = Sum.inr PUnit.unit

@[reducible]

def FirstOrder.Language.KripkeStructure.stStructure {W : Type u_1} {M : Type u_2} {Const : Type u_4} {Pred : Type u_5} (K : (Core.Logic.Modal.QBSML.monadicLang Const Pred).KripkeStructure W M) : (Core.Logic.Modal.QBSML.stLang Const Pred).Structure (W ⊕ M)

The W ⊕ M encoding of a Kripke structure over the monadic signature as a single mathlib structure: worlds and individuals share the carrier, sorted by stIndiv; relational guards make all off-sort atoms false.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Logic.Modal.QBSML.stStructure_relMap_rel {W : Type u_1} {M : Type u_2} {Const : Type u_4} {Pred : Type u_5} (K : (monadicLang Const Pred).KripkeStructure W M) (P : Pred) (z : Fin 2 → W ⊕ M) : FirstOrder.Language.Structure.RelMap (stRel P) z ↔ ∃ (w : W) (d : M), z 0 = Sum.inl w ∧ z 1 = Sum.inr d ∧ K.pInterp P w d

theorem Core.Logic.Modal.QBSML.stStructure_relMap_acc {W : Type u_1} {M : Type u_2} {Const : Type u_4} {Pred : Type u_5} (K : (monadicLang Const Pred).KripkeStructure W M) (z : Fin 2 → W ⊕ M) : FirstOrder.Language.Structure.RelMap stAcc z ↔ ∃ (w₁ : W) (w₂ : W), z 0 = Sum.inl w₁ ∧ z 1 = Sum.inl w₂ ∧ w₂ ∈ K.access w₁

theorem Core.Logic.Modal.QBSML.stStructure_relMap_indiv {W : Type u_1} {M : Type u_2} {Const : Type u_4} {Pred : Type u_5} (K : (monadicLang Const Pred).KripkeStructure W M) (z : Fin 1 → W ⊕ M) : FirstOrder.Language.Structure.RelMap stIndiv z ↔ ∃ (d : M), z 0 = Sum.inr d

theorem Core.Logic.Modal.QBSML.stStructure_funMap_inl {W : Type u_1} {M : Type u_2} {Const : Type u_4} {Pred : Type u_5} (K : (monadicLang Const Pred).KripkeStructure W M) (c : Const) (w : W) (z : Fin 1 → W ⊕ M) (hz : z 0 = Sum.inl w) : FirstOrder.Language.Structure.funMap (stConst c) z = Sum.inr (K.cInterp c w)

The translation

def Core.Logic.Modal.QBSML.stTerm {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} (k : ℕ) : (monadicLang Const Pred).Term (Var ⊕ Fin 0) → (stLang Const Pred).Term (Var ⊕ ℕ)

Translate a monadic term: variables stay, constants become their unary function applied to the current world variable.

Equations

• Core.Logic.Modal.QBSML.stTerm k (FirstOrder.Language.var (Sum.inl x_1)) = FirstOrder.Language.var (Sum.inl x_1)
• Core.Logic.Modal.QBSML.stTerm k (FirstOrder.Language.var (Sum.inr i)) = i.elim0
• Core.Logic.Modal.QBSML.stTerm k (FirstOrder.Language.func c _ts_2) = FirstOrder.Language.func (Core.Logic.Modal.QBSML.stConst c) ![FirstOrder.Language.var (Sum.inr k)]
• Core.Logic.Modal.QBSML.stTerm k (FirstOrder.Language.func f_2 _ts_2) = PEmpty.elim f_2

def Core.Logic.Modal.QBSML.stAtom? {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} (k : ℕ) : (monadicLang Const Pred).Formula Var → Option ((stLang Const Pred).Formula (Var ⊕ ℕ))

Translate an embedded classical formula when it is a monadic atom (none otherwise — which never arises from QBSMLFormula.toModal? images, whose embedded formulas are exactly the atoms).

Equations

• One or more equations did not get rendered due to their size.
• Core.Logic.Modal.QBSML.stAtom? k (FirstOrder.Language.BoundedFormula.rel r x_1) = PEmpty.elim r
• Core.Logic.Modal.QBSML.stAtom? k (FirstOrder.Language.BoundedFormula.rel r x_1) = PEmpty.elim r
• Core.Logic.Modal.QBSML.stAtom? k x✝ = none

def FirstOrder.Language.ModalFormula.st? {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq Var] (k : ℕ) : (Core.Logic.Modal.QBSML.monadicLang Const Pred).ModalFormula Var → Option ((Core.Logic.Modal.QBSML.stLang Const Pred).Formula (Var ⊕ ℕ))

The standard translation ST_k ([BdRV01]): the current world is the free variable Sum.inr k; box relativizes a fresh world variable Sum.inr (k + 1) along accessibility; quantifiers relativize to the individual sort.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.ModalFormula.st? k (FirstOrder.Language.ModalFormula.ofFormula χ) = Core.Logic.Modal.QBSML.stAtom? k χ
• FirstOrder.Language.ModalFormula.st? k φ.not = Option.map (fun (x : (Core.Logic.Modal.QBSML.stLang Const Pred).Formula (Var ⊕ ℕ)) => x.not) (FirstOrder.Language.ModalFormula.st? k φ)

Satisfaction preservation

theorem Core.Logic.Modal.QBSML.realize_st? {W : Type u_1} {M : Type u_2} {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq Var] (K : (monadicLang Const Pred).KripkeStructure W M) {φ : (monadicLang Const Pred).ModalFormula Var} {k : ℕ} {ψ : (stLang Const Pred).Formula (Var ⊕ ℕ)} : FirstOrder.Language.ModalFormula.st? k φ = some ψ → ∀ {val : Var ⊕ ℕ → W ⊕ M} {w : W} {v : Var → M}, (∀ (x : Var), val (Sum.inl x) = Sum.inr (v x)) → val (Sum.inr k) = Sum.inl w → (FirstOrder.Language.ModalFormula.Realize K w φ v ↔ ψ.Realize val)

Satisfaction preservation for the standard translation: Kripke satisfaction at w is first-order realization over stStructure, for any valuation that is individual-sorted on Var and pins the current world variable Sum.inr k to w. Off-sort quantifier instances are discharged by the relational guards, and box's fresh world variable k + 1 leaves the pinned index untouched.

Sort-guarded sentence closure

def Core.Logic.Modal.QBSML.stClose {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq Var] (k : ℕ) (ψ : (stLang Const Pred).Formula (Var ⊕ ℕ)) : (stLang Const Pred).Formula (Var ⊕ ℕ)

Sort-guarded existential closure of the current-world variable Sum.inr k: ∃z(¬IsIndiv(z) ∧ ψ). The guard is load-bearing on the mixed carrier — a bare ex₁ could be witnessed by a junk individual-as-world, which satisfies □⊥ vacuously.

Equations

• Core.Logic.Modal.QBSML.stClose k ψ = FirstOrder.Language.Formula.ex₁ (Sum.inr k) ((Core.Logic.Modal.QBSML.stIndiv.formula₁ (FirstOrder.Language.var (Sum.inr k))).not ⊓ ψ)

theorem Core.Logic.Modal.QBSML.realize_stClose {W : Type u_1} {M : Type u_2} {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq Var] (K : (monadicLang Const Pred).KripkeStructure W M) (k : ℕ) (ψ : (stLang Const Pred).Formula (Var ⊕ ℕ)) (val : Var ⊕ ℕ → W ⊕ M) : (stClose k ψ).Realize val ↔ ∃ (w : W), ψ.Realize (Function.update val (Sum.inr k) (Sum.inl w))

Over stStructure, the guarded witness of stClose is exactly a world.

Proposition 4.1, composed: QBSML support is first-order realization

theorem Core.Logic.Modal.QBSML.support_singleton_iff_st {W : Type u_1} {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq Var] {Domain : Type u_6} [DecidableEq W] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) {φ : QBSMLFormula Var Const Pred} {τ : (monadicLang Const Pred).ModalFormula Var} {k : ℕ} {ψ : (stLang Const Pred).Formula (Var ⊕ ℕ)} (hτ : φ.toModal? = some τ) (hψ : FirstOrder.Language.ModalFormula.st? k τ = some ψ) {i : Index W Var Domain} {v : Var → Domain} (u : ℕ → W) (hv : ∀ (y : Var), i.assign y = some (v y)) (hu : u k = i.world) : support M φ {i} ↔ ψ.Realize (Sum.elim (Sum.inr ∘ v) (Sum.inl ∘ u))

NE-free QBSML support is single-structure first-order satisfaction: [AvO23] Proposition 4.1 composed with the standard translation. Support at a singleton state is mathlib Formula.Realize of the standard translation over stStructure — the link along which classical model theory (compactness, Löwenheim–Skolem) transfers to the NE-free fragment.

theorem Core.Logic.Modal.QBSML.models_toSentence_of_support {W : Type u_1} {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq Var] {Domain : Type u_6} [DecidableEq W] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : QBSMLModel W Domain Const Pred) {φ : QBSMLFormula Var Const Pred} {τ : (monadicLang Const Pred).ModalFormula Var} {ψ : (stLang Const Pred).Formula (Var ⊕ ℕ)} (hτ : φ.toModal? = some τ) (hψ : FirstOrder.Language.ModalFormula.st? 0 τ = some ψ) (hcl : FirstOrder.Language.BoundedFormula.freeVarFinset (stClose 0 ψ) = ∅) {i : Index W Var Domain} {v : Var → Domain} (hv : ∀ (y : Var), i.assign y = some (v y)) (hsupp : support M φ {i}) : (W ⊕ Domain) ⊨ (stClose 0 ψ).toSentence hcl

Support at a singleton state forces the closed standard translation, as a sentence of stStructure.

theorem Core.Logic.Modal.QBSML.exists_support_of_models_toSentence {W : Type u_1} {Var : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq Var] {Domain : Type u_6} [DecidableEq W] [Fintype Var] [DecidableEq Domain] [Fintype Domain] [Nonempty Domain] (M : QBSMLModel W Domain Const Pred) {φ : QBSMLFormula Var Const Pred} {τ : (monadicLang Const Pred).ModalFormula Var} {ψ : (stLang Const Pred).Formula (Var ⊕ ℕ)} (hτ : φ.toModal? = some τ) (hψ : FirstOrder.Language.ModalFormula.st? 0 τ = some ψ) (hcl : FirstOrder.Language.BoundedFormula.freeVarFinset (stClose 0 ψ) = ∅) (h : (W ⊕ Domain) ⊨ (stClose 0 ψ).toSentence hcl) : ∃ (i : Index W Var Domain) (v : Var → Domain), (∀ (y : Var), i.assign y = some (v y)) ∧ support M φ {i}

Conversely, the closed standard translation as a sentence of stStructure yields support at some singleton state.

Compactness for the NE-free fragment

theorem Core.Logic.Modal.QBSML.support_compactness {Var : Type u_1} [DecidableEq Var] [Fintype Var] {Const : Type u} {Pred : Type v} {ι : Type u_2} {φs : ι → QBSMLFormula Var Const Pred} {τs : ι → (monadicLang Const Pred).ModalFormula Var} {ψs : ι → (stLang Const Pred).Formula (Var ⊕ ℕ)} (hτ : ∀ (i : ι), (φs i).toModal? = some (τs i)) (hψ : ∀ (i : ι), FirstOrder.Language.ModalFormula.st? 0 (τs i) = some (ψs i)) (hcl : ∀ (i : ι), FirstOrder.Language.BoundedFormula.freeVarFinset (stClose 0 (ψs i)) = ∅) (hfin : ∀ (s : Finset ι), ∃ (W : Type (max u v)) (Domain : Type (max u v)) (x : DecidableEq W) (x_1 : DecidableEq Domain) (x_2 : Fintype Domain) (M : QBSMLModel W Domain Const Pred) (i : Index W Var Domain) (v : Var → Domain), (∀ (y : Var), i.assign y = some (v y)) ∧ ∀ j ∈ s, support M (φs j) {i}) : FirstOrder.Language.Theory.IsSatisfiable (Set.range fun (i : ι) => (stClose 0 (ψs i)).toSentence ⋯)

Compactness transfer for NE-free QBSML ([AvO23] Proposition 4.1, the standard translation, and mathlib's Theory.isSatisfiable_iff_isFinitelySatisfiable): if every finite subfamily of a family of NE-free formulas is supported at a singleton state of some model, the family's closed standard translations are jointly satisfiable in a single first-order structure.

The converse recovery of a team model from that structure would need Finset-branching accessibility and a Fintype domain, which an arbitrary first-order structure does not supply, so the transfer is stated one-way. Compactness for team-semantic consequence is proved directly (ultraproducts and saturation, without translation) by [PQ24], who also separate satisfiability- from entailment-compactness in team logics.