Standard translation of modal logic

InductiveRelation symbols of the modal first-order language#✓fully proved

Relation symbols of the modal first-order language: accessibility R (binary) and a unary predicate P_a for each atom a.

inductive ModalRelations (Atom : Type u) : ℕ → Type u
  /-- Accessibility, binary. -/
  | relR : ModalRelations Atom 2
  /-- The predicate for atom `a`, unary. -/
  | pred : Atom → ModalRelations Atom 1

Used by 4

Used byA Kripke model as a first-order structure · The first-order modal language · Correctness of the standard translation · Standard translation

DefinitionThe first-order modal language#✓fully proved

For a set of atoms, the first-order language of modal logic has no function symbols; its relation symbols are a binary symbol \(R\) (accessibility) and a unary symbol \(P_a\) for each atom \(a\).

def modalLanguage (Atom : Type u) : FirstOrder.Language.{u, u} where
  Functions := fun _ => PEmpty
  Relations := ModalRelations Atom

Uses 1 · Used by 5

Statement usesRelation symbols of the modal first-order language

Used byBisimulation-invariant formulas · Modal formulas are bisimulation-invariant under the standard translation · A Kripke model as a first-order structure · Correctness of the standard translation · Standard translation

InductiveRelation symbols of the frame language#✓fully proved

The relation symbols of the first-order frame language, indexed by arity: a single binary symbol \(R\) for accessibility, and no symbols of any other arity.

inductive FrameRelations : ℕ → Type
  /-- Accessibility, binary. -/
  | relR : FrameRelations 2

Used by 2

Used byFirst-order language of Kripke frames · A frame as a first-order structure

DefinitionFirst-order language of Kripke frames#✓fully proved

The first-order language of frames: no function symbols, one binary relation R.

def frameLanguage : FirstOrder.Language where
  Functions := fun _ => PEmpty
  Relations := FrameRelations

Uses 1 · Used by 1

Statement usesRelation symbols of the frame language

Used byA frame as a first-order structure

DefinitionA Kripke model as a first-order structure#✓fully proved

A Kripke model \(M\) with set of worlds \(W\) makes \(W\) a structure for the modal language: the accessibility symbol \(R\) is interpreted as the accessibility relation of \(M\), and the predicate \(P_a\) for an atom \(a\) holds at exactly the worlds where \(a\) is true under the valuation of \(M\).

@[instance_reducible]
def kripkeStructure {W : Type v} (M : KripkeModel W Atom) :
    (modalLanguage Atom).Structure W where
  funMap f _ := f.elim
  RelMap R ts := match R with
    | .relR => M.rel (ts 0) (ts 1)
    | .pred a => M.valuation (ts 0) a

Uses 3 · Used by 3

Statement usesKripke model · Relation symbols of the modal first-order language · The first-order modal language

Used byBisimulation-invariant formulas · Modal formulas are bisimulation-invariant under the standard translation · Correctness of the standard translation

DefinitionA frame as a first-order structure#✓fully proved

A binary relation \(r\) on a set \(W\) (a bare Kripke frame) makes \(W\) a structure for the frame language, in which the accessibility symbol \(R\) is interpreted as \(r\): \(R(w, w')\) holds if and only if \(r(w, w')\).

@[instance_reducible]
def frameStructure {W : Type v} (rel : W → W → Prop) : frameLanguage.Structure W where
  funMap f _ := f.elim
  RelMap R ts := match R with
    | .relR => rel (ts 0) (ts 1)

Uses 2

Statement usesRelation symbols of the frame language · First-order language of Kripke frames

DefinitionStandard translation#✓fully proved

For \(n\) variables \(x_0, \dots, x_{n-1}\) in scope and a term \(t\) of the modal language for the current world, the standard translation \(ST_t(\varphi)\) of a modal formula \(\varphi\) is the first-order formula over the modal language in these variables defined by recursion on \(\varphi\): \(ST_t(a) = P_a(t)\) for an atom \(a\); \(ST_t(\bot) = \bot\); \(ST_t(\varphi \to \psi) = ST_t(\varphi) \to ST_t(\psi)\); and \(ST_t(\Box \varphi) = \forall x_n \, (R(t, x_n) \to ST_{x_n}(\varphi))\), where \(x_n\) is a fresh variable and \(ST_{x_n}(\varphi)\) is taken with \(n + 1\) variables in scope.

def standardTranslation : (n : ℕ) → (modalLanguage Atom).Term (Empty ⊕ Fin n) →
    Formula Atom → (modalLanguage Atom).BoundedFormula Empty n
  | _, t, .atom a => BoundedFormula.rel (.pred a) ![t]
  | _, _, .bot => ⊥
  | _, t, .imp φ ψ => (standardTranslation _ t φ).imp (standardTranslation _ t ψ)
  | n, t, .box φ =>
    ((BoundedFormula.rel ModalRelations.relR ![t.relabel (Sum.map id (Fin.castAdd 1)),
      Term.var (Sum.inr ⟨n, by omega⟩)]).imp
      (standardTranslation (n + 1) (Term.var (Sum.inr ⟨n, by omega⟩)) φ)).all

Uses 3 · Used by 2

Statement usesModal formulas · Relation symbols of the modal first-order language · The first-order modal language

Used byModal formulas are bisimulation-invariant under the standard translation · Correctness of the standard translation

TheoremCorrectness of the standard translation#✓fully proved

Let \(M\) be a Kripke model with set of worlds \(W\), viewed as a structure for the modal language. For every \(n\), every term \(t\) of the modal language in the variables \(x_0, \dots, x_{n-1}\), every modal formula \(\varphi\) and every assignment of worlds in \(W\) to \(x_0, \dots, x_{n-1}\), the standard translation of \(\varphi\) with \(n\) variables in scope and current-world term \(t\) holds in \(M\) under this assignment if and only if \(\varphi\) is satisfied in \(M\) at the world that \(t\) denotes under the assignment.

theorem realize_standardTranslation {W : Type v} (M : KripkeModel W Atom) :
    ∀ (n : ℕ) (t : (modalLanguage Atom).Term (Empty ⊕ Fin n)) (φ : Formula Atom)
      (v : Empty → W) (xs : Fin n → W),
      @BoundedFormula.Realize (modalLanguage Atom) W (kripkeStructure M) Empty n
        (standardTranslation n t φ) v xs ↔
        M.Satisfies (@Term.realize (modalLanguage Atom) W (kripkeStructure M)
          (Empty ⊕ Fin n) (Sum.elim v xs) t) φ

Uses 7 · Used by 1

Statement usesModal formulas · Kripke model · Satisfaction in a Kripke model · A Kripke model as a first-order structure · The first-order modal language · Standard translation

Proof usesRelation symbols of the modal first-order language

Used byModal formulas are bisimulation-invariant under the standard translation

DefinitionBisimulation-invariant formulas#✓fully proved

A first-order formula \(\alpha\) over the modal language, with one variable \(x\) and no other free variables, is bisimulation-invariant if for all Kripke models \(M\) and \(N\) over the same atoms, every bisimulation \(Z\) between \(M\) and \(N\) and all worlds \(w\) of \(M\) and \(v\) of \(N\) with \(Z(w, v)\), the formula \(\alpha\) holds in \(M\) (viewed as a structure for the modal language) at \(x = w\) if and only if it holds in \(N\) at \(x = v\).

def BisimulationInvariant {Atom : Type u}
    (α : (modalLanguage Atom).BoundedFormula Empty 1) : Prop :=
  ∀ {W : Type v} {V : Type w} (M : KripkeModel W Atom) (N : KripkeModel V Atom)
    (R : W → V → Prop), Bisimulation M N R → ∀ (w : W) (v : V), R w v →
      (@BoundedFormula.Realize (modalLanguage Atom) W (kripkeStructure M) Empty 1 α
        (fun x => x.elim) (fun _ => w) ↔
      @BoundedFormula.Realize (modalLanguage Atom) V (kripkeStructure N) Empty 1 α
        (fun x => x.elim) (fun _ => v))

Uses 4 · Used by 1

Statement usesBisimulation · Kripke model · A Kripke model as a first-order structure · The first-order modal language

Used byModal formulas are bisimulation-invariant under the standard translation

TheoremModal formulas are bisimulation-invariant under the standard translation#✓fully proved

For every modal formula \(\varphi\), its standard translation \(ST_x(\varphi)\) (the first-order formula over the modal language whose single variable \(x\) stands for the current world) is bisimulation-invariant: for all Kripke models \(M\) and \(N\), every bisimulation \(Z\) between \(M\) and \(N\) and all worlds \(w\) of \(M\) and \(v\) of \(N\) with \(Z(w, v)\), the formula \(ST_x(\varphi)\) holds in \(M\) at \(x = w\) if and only if it holds in \(N\) at \(x = v\).

theorem bisimulationInvariant_standardTranslation (φ : Formula Atom) :
    BisimulationInvariant (standardTranslation 1 (Term.var (Sum.inr (0 : Fin 1))) φ)

Uses 10

Statement usesBisimulation-invariant formulas · Modal formulas · The first-order modal language · Standard translation

Proof usesBisimulation · Bisimulations preserve modal formulas · Kripke model · Satisfaction in a Kripke model · A Kripke model as a first-order structure · Correctness of the standard translation

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.