Kripke semantics

29 fully proved

Modal

InductiveModal formulas#✓fully proved

For a type \(\alpha\) of atoms, the formulas of basic modal logic over \(\alpha\) are generated as follows: every atom \(p \in \alpha\) is a formula; falsity \(\bot\) is a formula; if \(\varphi\) and \(\psi\) are formulas then so is the implication \(\varphi \to \psi\); and if \(\varphi\) is a formula then so is the necessity formula \(\Box\varphi\).

inductive Formula (α : Type u) : Type u where
  | atom : α → Formula α
  | bot : Formula α
  | imp : Formula α → Formula α → Formula α
  | box : Formula α → Formula α
  deriving DecidableEq, Repr

Used by 148

Used byBisimulations preserve modal formulas · Bisimilar worlds are modally equivalent · Finite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Boolean evaluation in a finite model · Finite model property of K · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Completeness of K, countermodel form · Filtration worlds are realized types · Smallest filtration of a Kripke model · Smallest filtration relation · Worlds of the filtration · Finite Kripke model on sets of formulas · Reflexivity on a finite set of worlds · Filtrations of reflexive models are reflexive · Symmetry on a finite set of worlds · Transitivity on a finite set of worlds · Finite validity check for K · Finite validity check for a frame condition · The finite check covers the filtration worlds · Filtration relations · The smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · The S5 relation is a filtration of an equivalence model · Lemmon filtration relation · A filtration refutes what the model refutes · S5 filtration relation · Filtration lemma for the smallest filtration · Filtration lemma · Worlds of the same type agree on subformulas · Subformulas · The subformula relation is transitive · Type of a world · Conjunction · Axiom B · Axiom D · Axiom 5 · Axiom 4 · Axiom K · Axiom T · The possibility operator · Negation of modal formulas · Falsity is valid in no Kripke model · Disjunction of modal formulas · Satisfaction in a Kripke model · Semantics of possibility · Invariance of modal satisfaction under bounded morphisms · The truth constant · Global validity in a Kripke model · Axiom B is valid on symmetric Kripke models · Axiom D is valid on serial Kripke models · Axiom 5 is valid on euclidean Kripke models · Axiom 4 is valid on transitive Kripke models · Validity of axiom K on Kripke models · Axiom T is valid on reflexive Kripke models · Surjective bounded morphisms preserve and reflect validity · Contradiction yields falsity · The monotonicity rule for necessity · Local consequence in a normal modal logic · Consequences of no hypotheses are the theorems · The deduction theorem for local modal consequence · Theorems of a normal modal logic · Compactness of local modal consequence · The deduction theorem for local modal consequence, forward direction · Self-implication is a theorem · Hypothetical syllogism · Extra axioms of the modal logic K · Monotonicity of theorems in the extra axioms · Monotonicity of local consequence in the hypotheses · Double-negation introduction · Negation introduction · Consistency of normal modal logics · Consistency of K · Consistency of S4 · Consistency of S5 · Consistency of T · Ex falso quodlibet · Local consequences of theorems are theorems · Proof by contradiction · Extra axioms of S4 · Extra axioms of S5 · Local soundness · Extra axioms of T · Transitivity of local consequence · Soundness of modal Hilbert systems for Kripke models · Soundness of K for Kripke models · Soundness of S4 for reflexive transitive Kripke models · Soundness of S5 for Kripke models with an equivalence relation · Soundness of T for reflexive Kripke models · Atoms of a modal formula · Iterated box · Negative modal formulas · Positive modal formulas · Sahlqvist formulas · Sahlqvist antecedents · The B axiom is a Sahlqvist formula · Sahlqvist implications · Boxing an implication chain · The canonical model as a CSLib model · The canonical model · Worlds of the canonical model · Strong completeness of K · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Consistency relative to a normal modal logic · Consistency is of finite character · Strong soundness and completeness of K · Strong soundness and completeness of S4 · Strong soundness and completeness of S5 · Strong soundness and completeness of T · Double-negation introduction under a box · Soundness and completeness of K · Validity in a class containing the canonical model gives derivability · Completeness for CSLib's S4 · Completeness for CSLib's S5 · Completeness for CSLib's T · Soundness and completeness of S4 · Soundness and completeness of S5 · Soundness and completeness of T · Lindenbaum's lemma for normal modal logics · Existence lemma · Discharging a list of hypotheses · Local semantic consequence over a class of Kripke models · Maximal consistent sets of modal formulas are deductively closed · Iterated modus ponens in maximal consistent sets · Deducibility from maximal consistent extensions · Completeness relative to the canonical model · Translation of CSLib's modal propositions · The canonical accessibility relation · Model existence for K · Model existence from the canonical model · Model existence for S4 · Model existence for S5 · Model existence for T · Truth lemma · The translation preserves satisfaction · The reverse translation preserves satisfaction · Translation of modal formulas into CSLib propositions · Validity agrees with its CSLib translation · Modal formulas are bisimulation-invariant under the standard translation · Correctness of the standard translation · Standard translation

Formula

DefinitionNegation of modal formulas#✓fully proved

The negation of a modal formula \(\varphi\) is the formula \(\neg\varphi := \varphi \to \bot\).

def neg (phi : Formula Atom) : Formula Atom := .imp phi .bot

Uses 1 · Used by 23

Statement usesModal formulas

Used byConjunction · The possibility operator · Disjunction of modal formulas · The truth constant · Contradiction yields falsity · Theorems of a normal modal logic · Monotonicity of theorems in the extra axioms · Double-negation introduction · Negation introduction · Ex falso quodlibet · Proof by contradiction · Soundness of modal Hilbert systems for Kripke models · The B axiom is a Sahlqvist formula · Strong completeness of S5 · Double-negation introduction under a box · Completeness for CSLib's S5 · Existence lemma · Maximal consistent sets of modal formulas are deductively closed · Deducibility from maximal consistent extensions · Translation of CSLib's modal propositions · Model existence for S5 · Truth lemma · The translation preserves satisfaction

DefinitionThe possibility operator#✓fully proved

For a modal formula \(\varphi\), the formula \(\Diamond\varphi\) ("possibly \(\varphi\)") is \(\neg\Box\neg\varphi\), where \(\neg\chi\) stands for \(\chi \to \bot\).

def dia (phi : Formula Atom) : Formula Atom := neg (.box (neg phi))

Uses 2 · Used by 14

Statement usesModal formulas · Negation of modal formulas

Used byAxiom B · Axiom D · Axiom 5 · Semantics of possibility · Axiom B is valid on symmetric Kripke models · Axiom D is valid on serial Kripke models · Axiom 5 is valid on euclidean Kripke models · Sahlqvist antecedents · The B axiom is a Sahlqvist formula · Strong completeness of S5 · Completeness for CSLib's S5 · Translation of CSLib's modal propositions · Model existence for S5 · The translation preserves satisfaction

DefinitionThe truth constant#✓fully proved

The formula \(\top\) is the negation \(\neg\bot\) of falsity, that is, the implication \(\bot \to \bot\).

def top : Formula Atom := neg .bot

Uses 2

Statement usesModal formulas · Negation of modal formulas

DefinitionConjunction#✓fully proved

For modal formulas \(\varphi\) and \(\psi\), the conjunction \(\varphi \wedge \psi\) is the formula \(\neg(\varphi \to \neg\psi)\), where \(\neg\chi\) stands for \(\chi \to \bot\).

def and (phi psi : Formula Atom) : Formula Atom := neg (.imp phi (neg psi))

Uses 2 · Used by 2

Statement usesModal formulas · Negation of modal formulas

Used bySahlqvist formulas · Sahlqvist antecedents

DefinitionDisjunction of modal formulas#✓fully proved

The disjunction of modal formulas \(\varphi\) and \(\psi\) is the formula \(\varphi \lor \psi := \neg\varphi \to \psi\), where \(\neg\varphi\) is \(\varphi \to \bot\).

def or (phi psi : Formula Atom) : Formula Atom := .imp (neg phi) psi

Uses 2 · Used by 4

Statement usesModal formulas · Negation of modal formulas

Used bySahlqvist formulas · Sahlqvist antecedents · Translation of CSLib's modal propositions · The translation preserves satisfaction

DefinitionAxiom K#✓fully proved

For modal formulas \(\varphi\) and \(\psi\), the distribution axiom K is the formula \(\Box(\varphi \to \psi) \to (\Box\varphi \to \Box\psi)\).

def axiomK (phi psi : Formula Atom) : Formula Atom :=
  .imp (.box (.imp phi psi)) (.imp (.box phi) (.box psi))

Uses 1 · Used by 6

Statement usesModal formulas

Used byValidity of axiom K on Kripke models · The monotonicity rule for necessity · Theorems of a normal modal logic · Monotonicity of theorems in the extra axioms · Soundness of modal Hilbert systems for Kripke models · Boxing an implication chain

DefinitionAxiom T#✓fully proved

For a modal formula \(\varphi\), the reflexivity axiom T is the formula \(\Box\varphi \to \varphi\).

def axiomT (phi : Formula Atom) : Formula Atom := .imp (.box phi) phi

Uses 1 · Used by 19

Statement usesModal formulas

Used byAxiom T is valid on reflexive Kripke models · Extra axioms of S4 · Extra axioms of S5 · Extra axioms of T · Soundness of S4 for reflexive transitive Kripke models · Soundness of S5 for Kripke models with an equivalence relation · Soundness of T for reflexive Kripke models · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Strong soundness and completeness of S4 · Strong soundness and completeness of S5 · Strong soundness and completeness of T · Completeness for CSLib's S4 · Completeness for CSLib's S5 · Completeness for CSLib's T · Model existence for S4 · Model existence for S5 · Model existence for T

DefinitionAxiom 4#✓fully proved

For a modal formula \(\varphi\), the transitivity axiom 4 is the formula \(\Box\varphi \to \Box\Box\varphi\).

def axiomFour (phi : Formula Atom) : Formula Atom := .imp (.box phi) (.box (.box phi))

Uses 1 · Used by 7

Statement usesModal formulas

Used byAxiom 4 is valid on transitive Kripke models · Extra axioms of S4 · Soundness of S4 for reflexive transitive Kripke models · Strong completeness of S4 · Strong soundness and completeness of S4 · Completeness for CSLib's S4 · Model existence for S4

DefinitionAxiom D#✓fully proved

For a modal formula \(\varphi\), the seriality axiom D is the formula \(\Box\varphi \to \Diamond\varphi\), where \(\Diamond\psi\) is \(\neg\Box\neg\psi\) and \(\neg\chi\) stands for \(\chi \to \bot\).

def axiomD (phi : Formula Atom) : Formula Atom := .imp (.box phi) (dia phi)

Uses 2 · Used by 1

Statement usesModal formulas · The possibility operator

Used byAxiom D is valid on serial Kripke models

DefinitionAxiom B#✓fully proved

For a modal formula \(\varphi\), the symmetry axiom B is the formula \(\varphi \to \Box\Diamond\varphi\), where \(\Diamond\psi\) is \(\neg\Box\neg\psi\) and \(\neg\chi\) stands for \(\chi \to \bot\).

def axiomB (phi : Formula Atom) : Formula Atom := .imp phi (.box (dia phi))

Uses 2 · Used by 2

Statement usesModal formulas · The possibility operator

Used byAxiom B is valid on symmetric Kripke models · The B axiom is a Sahlqvist formula

DefinitionAxiom 5#✓fully proved

For a modal formula \(\varphi\), the euclidean axiom 5 is the formula \(\Diamond\varphi \to \Box\Diamond\varphi\), where \(\Diamond\psi\) is \(\neg\Box\neg\psi\) and \(\neg\chi\) stands for \(\chi \to \bot\).

def axiomFive (phi : Formula Atom) : Formula Atom := .imp (dia phi) (.box (dia phi))

Uses 2 · Used by 7

Statement usesModal formulas · The possibility operator

Used byAxiom 5 is valid on euclidean Kripke models · Extra axioms of S5 · Soundness of S5 for Kripke models with an equivalence relation · Strong completeness of S5 · Strong soundness and completeness of S5 · Completeness for CSLib's S5 · Model existence for S5

Modal

StructureKripke model#✓fully proved

A Kripke model consists of a nonempty collection of worlds, an accessibility relation, and an atom valuation.

structure KripkeModel (World : Type u) (Atom : Type v) where
  /-- There is at least one world. -/
  nonempty_world : Nonempty World
  /-- The accessibility relation. -/
  rel : World → World → Prop
  /-- The atoms true at each world. -/
  valuation : World → Atom → Prop

Used by 162

Used byBisimilar worlds · Bisimulation · Bisimulations preserve modal formulas · Bisimilar worlds are modally equivalent · Finite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of K · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Completeness of K, countermodel form · Filtration worlds are realized types · Smallest filtration of a Kripke model · Smallest filtration relation · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtrations of reflexive models are reflexive · The finite check covers the filtration worlds · Filtration relations · The smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · The S5 relation is a filtration of an equivalence model · Lemmon filtration relation · A filtration refutes what the model refutes · S5 filtration relation · Filtration lemma for the smallest filtration · Filtration lemma · Worlds of the same type agree on subformulas · Type of a world · Bounded morphism · Composition of bounded morphisms · Extensionality for bounded morphisms · Identity bounded morphism · Falsity is valid in no Kripke model · Satisfaction in a Kripke model · Semantics of possibility · Invariance of modal satisfaction under bounded morphisms · Global validity in a Kripke model · Axiom B is valid on symmetric Kripke models · Axiom D is valid on serial Kripke models · Axiom 5 is valid on euclidean Kripke models · Axiom 4 is valid on transitive Kripke models · Validity of axiom K on Kripke models · Axiom T is valid on reflexive Kripke models · Surjective bounded morphisms preserve and reflect validity · \(\mathsf{AG}\) is universal reachability · \(\mathsf{EF}\) is reachability · Park induction · The least fixed point is contained in its unfolding · The formula \(\mu X.\, \mu Y.\, X\) is false everywhere · The fixed-point operator of a formula · The least fixed point is a pre-fixed point · Coinduction for the greatest fixed point · The greatest fixed point is a pre-fixed point · The formula \(\nu X.\, \nu Y.\, X\) is true everywhere · The greatest fixed point is a post-fixed point · Satisfaction in the modal μ-calculus · Denotation of a closed μ-calculus formula is environment-independent · Satisfaction is monotone in the environment · Monotonicity in the bound variable · The μ formula denotes the least fixed point · The μ unfolding · Duality · The ν formula denotes the greatest fixed point · The ν unfolding · Canonical next move induced by a bespoke strategy · Verifier's positional strategies make a game move at Verifier positions that have one · The canonical move follows the bespoke strategy at Verifier positions with a move · Segments of canonical plays through fragment positions are bespoke plays · The regression play is a play · The one-world reflexive Kripke model · \(\mu X.\, \nu Y.\, X\) is false in the one-world model · Moves from a diamond position · Moves of the totalized fragment game · Moves of the totalized fragment game, by cases · Plays of the totalized fragment game stay at the losing state · Plays of the totalized fragment game stay at the winning state · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Fragment parity game · Wins is the winning region of the fragment game · The losing state is absorbing · Moves of the μ-calculus model-checking game · Fragment moves decrease the formula size · Finite plays are nonempty · No infinite play from a fragment position · Positions with no moves · Inversion for disjunction moves · Finite plays consistent with a strategy · Fragment moves between embedded positions are game moves · Moves to the losing state come from terminal losing positions · Moves to the winning state come from terminal winning positions · Closed formulas are environment-independent · Satisfaction depends only on the environment below the closure depth · Verifier strategy · Winning strategy from a position · Winning strategies stay winning along consistent moves · Winner at a terminal position · Verifier has a winning strategy · Game-vs-satisfaction, converse direction · The absorbing win state · Backward-induction winning region of the fixpoint-free fragment · Backward-induction winning equals satisfaction on the fixpoint-free fragment · Backward-induction winning equals game winning on the fixpoint-free fragment · Game-vs-satisfaction, strategy direction · Wins-guided move · The Wins-guided move at a diamond · The Wins-guided move is legal · The Wins-guided move at a disjunction · Wins-guided strategy · Wins-guided strategy wins every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction) · Sequences that stay at the win state are won by the even player · Sequences that stay at the lose state are won by the odd player · Consistency of S4 · Local soundness · The one-world Kripke model · The one-world model has an equivalence relation · Soundness of modal Hilbert systems for Kripke models · Soundness of K for Kripke models · Soundness of S4 for reflexive transitive Kripke models · Soundness of S5 for Kripke models with an equivalence relation · Soundness of T for reflexive Kripke models · The canonical model · Strong completeness of K · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Strong soundness and completeness of K · Strong soundness and completeness of S4 · Strong soundness and completeness of S5 · Strong soundness and completeness of T · Soundness and completeness of K · Validity in a class containing the canonical model gives derivability · Soundness and completeness of S4 · Soundness and completeness of S5 · Soundness and completeness of T · Local semantic consequence over a class of Kripke models · Soundness for CSLib's S4 · Soundness for CSLib's S5 · Kripke model of a CSLib model · Kripke to CSLib and back is the identity · Model existence for K · Model existence from the canonical model · Model existence for S4 · Model existence for S5 · Model existence for T · Truth lemma · The translation preserves satisfaction · The reverse translation preserves satisfaction · The CSLib unimodal model of a Kripke model · Validity agrees with its CSLib translation · Bisimulation-invariant formulas · Modal formulas are bisimulation-invariant under the standard translation · A Kripke model as a first-order structure · Correctness of the standard translation · Satisfiability of a closed modal μ-calculus formula

Kripke Model

DefinitionSatisfaction in a Kripke model#✓fully proved

Let \(M\) be a Kripke model with accessibility relation \(R\). Satisfaction of a modal formula at a world \(w\) of \(M\) is defined by recursion on the formula: \(w\) satisfies an atom \(p\) if and only if the valuation of \(M\) makes \(p\) true at \(w\); \(w\) never satisfies \(\bot\); \(w\) satisfies \(\varphi \to \psi\) if and only if \(w\) satisfies \(\psi\) whenever it satisfies \(\varphi\); and \(w\) satisfies \(\Box\varphi\) if and only if every world \(v\) with \(w \mathrel{R} v\) satisfies \(\varphi\).

def Satisfies (model : KripkeModel World Atom) (world : World) : Formula Atom → Prop
  | .atom atom => model.valuation world atom
  | .bot => False
  | .imp phi psi => Satisfies model world phi → Satisfies model world psi
  | .box phi => ∀ next, model.rel world next → Satisfies model next phi

Uses 2 · Used by 63

Statement usesModal formulas · Kripke model

Used byBisimulations preserve modal formulas · Bisimilar worlds are modally equivalent · Finite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of K · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Completeness of K, countermodel form · Smallest filtration of a Kripke model · The finite check covers the filtration worlds · Filtration relations · The smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · The S5 relation is a filtration of an equivalence model · A filtration refutes what the model refutes · Filtration lemma for the smallest filtration · Filtration lemma · Worlds of the same type agree on subformulas · Type of a world · Falsity is valid in no Kripke model · Semantics of possibility · Invariance of modal satisfaction under bounded morphisms · Global validity in a Kripke model · Axiom B is valid on symmetric Kripke models · Axiom D is valid on serial Kripke models · Axiom 5 is valid on euclidean Kripke models · Axiom 4 is valid on transitive Kripke models · Validity of axiom K on Kripke models · Axiom T is valid on reflexive Kripke models · Surjective bounded morphisms preserve and reflect validity · Local soundness · Soundness of modal Hilbert systems for Kripke models · Strong completeness of K · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Strong soundness and completeness of K · Strong soundness and completeness of S4 · Strong soundness and completeness of S5 · Strong soundness and completeness of T · Soundness and completeness of K · Validity in a class containing the canonical model gives derivability · Soundness and completeness of S4 · Soundness and completeness of S5 · Soundness and completeness of T · Local semantic consequence over a class of Kripke models · Validity of the translation gives membership in CSLib's logic · Completeness relative to the canonical model · Model existence for K · Model existence from the canonical model · Model existence for S4 · Model existence for S5 · Model existence for T · Truth lemma · The translation preserves satisfaction · The reverse translation preserves satisfaction · Validity agrees with its CSLib translation · Modal formulas are bisimulation-invariant under the standard translation · Correctness of the standard translation

DefinitionGlobal validity in a Kripke model#✓fully proved

A formula \(\varphi\) is globally valid in a Kripke model \(M\) when \(\varphi\) is satisfied at every world of \(M\).

def Valid (model : KripkeModel World Atom) (phi : Formula Atom) : Prop :=
  ∀ world, model.Satisfies world phi

Uses 3 · Used by 36

Statement usesModal formulas · Kripke model · Satisfaction in a Kripke model

Used byK-theorems via finite models on sets of subformulas · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of K · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Completeness of K, countermodel form · The finite check covers the filtration worlds · A filtration refutes what the model refutes · Falsity is valid in no Kripke model · Axiom B is valid on symmetric Kripke models · Axiom D is valid on serial Kripke models · Axiom 5 is valid on euclidean Kripke models · Axiom 4 is valid on transitive Kripke models · Validity of axiom K on Kripke models · Axiom T is valid on reflexive Kripke models · Surjective bounded morphisms preserve and reflect validity · Consistency of normal modal logics · Local soundness · Soundness of modal Hilbert systems for Kripke models · Soundness of K for Kripke models · Soundness of S4 for reflexive transitive Kripke models · Soundness of S5 for Kripke models with an equivalence relation · Soundness of T for reflexive Kripke models · Strong soundness and completeness of K · Strong soundness and completeness of S4 · Strong soundness and completeness of S5 · Strong soundness and completeness of T · Soundness and completeness of K · Soundness and completeness of S4 · Soundness and completeness of S5 · Soundness and completeness of T · Validity of the translation gives membership in CSLib's logic · Validity agrees with its CSLib translation

TheoremFalsity is valid in no Kripke model#✓fully proved

For every Kripke model \(M\), the formula \(\bot\) is not valid in \(M\): since \(M\) has at least one world and no world satisfies \(\bot\), some world of \(M\) fails to satisfy \(\bot\).

@[simp] theorem not_valid_bot (model : KripkeModel World Atom) :
    ¬model.Valid (.bot : Formula Atom)

Uses 4

Statement usesModal formulas · Kripke model · Global validity in a Kripke model

Proof usesSatisfaction in a Kripke model

TheoremSemantics of possibility#✓fully proved

Let \(M\) be a Kripke model with accessibility relation \(R\), and let \(\Diamond\varphi\) denote the formula \(\neg\Box\neg\varphi\), where \(\neg\chi\) is \(\chi \to \bot\). For every world \(w\) and modal formula \(\varphi\), \(w\) satisfies \(\Diamond\varphi\) in \(M\) if and only if there is a world \(v\) with \(w \mathrel{R} v\) such that \(v\) satisfies \(\varphi\) in \(M\).

theorem satisfies_dia (model : KripkeModel World Atom) (world : World)
    (phi : Formula Atom) :
    model.Satisfies world phi.dia ↔
      ∃ next, model.rel world next ∧ model.Satisfies next phi

Uses 4 · Used by 4

Statement usesModal formulas · The possibility operator · Kripke model · Satisfaction in a Kripke model

Used byAxiom B is valid on symmetric Kripke models · Axiom D is valid on serial Kripke models · Axiom 5 is valid on euclidean Kripke models · The translation preserves satisfaction

TheoremValidity of axiom K on Kripke models#✓fully proved

The K axiom is valid on every Kripke model.

theorem valid_axiomK (model : KripkeModel World Atom) (phi psi : Formula Atom) :
    model.Valid (Formula.axiomK phi psi)

Uses 5 · Used by 1

Statement usesModal formulas · Axiom K · Kripke model · Global validity in a Kripke model

Proof usesSatisfaction in a Kripke model

Used bySoundness of modal Hilbert systems for Kripke models

TheoremAxiom T is valid on reflexive Kripke models#✓fully proved

Let \(M\) be a Kripke model whose accessibility relation \(R\) is reflexive: \(R\,w\,w\) for every world \(w\). Then for every formula \(\varphi\) the T axiom \(\Box\varphi \to \varphi\) is globally valid in \(M\).

theorem valid_axiomT (model : KripkeModel World Atom)
    (reflexive : ∀ world, model.rel world world) (phi : Formula Atom) :
    model.Valid (Formula.axiomT phi)

Uses 5 · Used by 6

Statement usesModal formulas · Axiom T · Kripke model · Global validity in a Kripke model

Proof usesSatisfaction in a Kripke model

Used bySoundness of S4 for reflexive transitive Kripke models · Soundness of S5 for Kripke models with an equivalence relation · Soundness of T for reflexive Kripke models · Strong soundness and completeness of S4 · Strong soundness and completeness of S5 · Strong soundness and completeness of T

TheoremAxiom 4 is valid on transitive Kripke models#✓fully proved

Let \(M\) be a Kripke model whose accessibility relation \(R\) is transitive: \(R\,u\,v\) and \(R\,v\,w\) imply \(R\,u\,w\) for all worlds \(u, v, w\). Then for every formula \(\varphi\) the 4 axiom \(\Box\varphi \to \Box\Box\varphi\) is globally valid in \(M\).

theorem valid_axiomFour (model : KripkeModel World Atom)
    (transitive : ∀ {first second third},
      model.rel first second → model.rel second third → model.rel first third)
    (phi : Formula Atom) : model.Valid (Formula.axiomFour phi)

Uses 5 · Used by 2

Statement usesModal formulas · Axiom 4 · Kripke model · Global validity in a Kripke model

Proof usesSatisfaction in a Kripke model

Used bySoundness of S4 for reflexive transitive Kripke models · Strong soundness and completeness of S4

TheoremAxiom D is valid on serial Kripke models#✓fully proved

Let \(M\) be a Kripke model whose accessibility relation \(R\) is serial: every world \(w\) has some world \(v\) with \(R\,w\,v\). Then for every formula \(\varphi\) the D axiom \(\Box\varphi \to \Diamond\varphi\), where \(\Diamond\varphi\) abbreviates \(\neg\Box\neg\varphi\), is globally valid in \(M\).

theorem valid_axiomD (model : KripkeModel World Atom)
    (serial : ∀ world, ∃ next, model.rel world next) (phi : Formula Atom) :
    model.Valid (Formula.axiomD phi)

Uses 7

Statement usesModal formulas · Axiom D · Kripke model · Global validity in a Kripke model

Proof usesThe possibility operator · Satisfaction in a Kripke model · Semantics of possibility

TheoremAxiom B is valid on symmetric Kripke models#✓fully proved

Let \(M\) be a Kripke model whose accessibility relation \(R\) is symmetric: \(R\,u\,v\) implies \(R\,v\,u\) for all worlds \(u, v\). Then for every formula \(\varphi\) the B axiom \(\varphi \to \Box\Diamond\varphi\), where \(\Diamond\varphi\) abbreviates \(\neg\Box\neg\varphi\), is globally valid in \(M\).

theorem valid_axiomB (model : KripkeModel World Atom)
    (symmetric : ∀ {first second}, model.rel first second → model.rel second first)
    (phi : Formula Atom) : model.Valid (Formula.axiomB phi)

Uses 7

Statement usesModal formulas · Axiom B · Kripke model · Global validity in a Kripke model

Proof usesThe possibility operator · Satisfaction in a Kripke model · Semantics of possibility

TheoremAxiom 5 is valid on euclidean Kripke models#✓fully proved

Let \(M\) be a Kripke model whose accessibility relation \(R\) is euclidean: \(R\,u\,v\) and \(R\,u\,w\) imply \(R\,v\,w\) for all worlds \(u, v, w\). Then for every formula \(\varphi\) the 5 axiom \(\Diamond\varphi \to \Box\Diamond\varphi\), where \(\Diamond\varphi\) abbreviates \(\neg\Box\neg\varphi\), is globally valid in \(M\).

theorem valid_axiomFive (model : KripkeModel World Atom)
    (euclidean : ∀ {first second third}, model.rel first second → model.rel first third →
      model.rel second third)
    (phi : Formula Atom) : model.Valid (Formula.axiomFive phi)

Uses 7 · Used by 2

Statement usesModal formulas · Axiom 5 · Kripke model · Global validity in a Kripke model

Proof usesThe possibility operator · Satisfaction in a Kripke model · Semantics of possibility

Used bySoundness of S5 for Kripke models with an equivalence relation · Strong soundness and completeness of S5

Modal

StructureBounded morphism#✓fully proved

Let \(M\) and \(N\) be Kripke models over the same atoms, with sets of worlds \(W\) and \(V\) and accessibility relations \(R_M\) and \(R_N\). A bounded morphism from \(M\) to \(N\) is a map \(f : W \to V\) such that every atom holds at a world \(w\) in \(M\) if and only if it holds at \(f(w)\) in \(N\); whenever \(w \mathrel{R_M} w'\), also \(f(w) \mathrel{R_N} f(w')\) (forth); and whenever \(f(w) \mathrel{R_N} v'\), there is a world \(w'\) with \(w \mathrel{R_M} w'\) and \(f(w') = v'\) (back).

Bounded morphisms are also called p-morphisms.

structure BoundedMorphism (source : KripkeModel W Atom) (target : KripkeModel V Atom) where
  /-- The underlying map on worlds. -/
  toFun : W → V
  atom_iff : ∀ world atom,
    source.valuation world atom ↔ target.valuation (toFun world) atom
  forth : ∀ {world next}, source.rel world next → target.rel (toFun world) (toFun next)
  back : ∀ {world imageNext}, target.rel (toFun world) imageNext →
    ∃ next, source.rel world next ∧ toFun next = imageNext

Uses 1 · Used by 5

Statement usesKripke model

Used byComposition of bounded morphisms · Extensionality for bounded morphisms · Identity bounded morphism · Invariance of modal satisfaction under bounded morphisms · Surjective bounded morphisms preserve and reflect validity

Bounded Morphism

TheoremExtensionality for bounded morphisms#✓fully proved

Two bounded morphisms \(f\) and \(g\) between the same Kripke models are equal if \(f(w) = g(w)\) for every world \(w\).

@[ext]
theorem ext (first second : BoundedMorphism source middle)
    (maps_eq : ∀ world, first world = second world) : first = second

Uses 2

Statement usesBounded morphism · Kripke model

DefinitionIdentity bounded morphism#✓fully proved

For every Kripke model \(M\), the identity map on the worlds of \(M\) is a bounded morphism from \(M\) to itself.

def id (model : KripkeModel W Atom) : BoundedMorphism model model where
  toFun := _root_.id
  atom_iff := by simp
  forth := fun h => h
  back := by
    intro world next h
    exact ⟨next, h, rfl⟩

Uses 2

Statement usesBounded morphism · Kripke model

DefinitionComposition of bounded morphisms#✓fully proved

Let \(M_1\), \(M_2\), \(M_3\) be Kripke models over the same atoms. If \(f\) is a bounded morphism from \(M_1\) to \(M_2\) and \(g\) is a bounded morphism from \(M_2\) to \(M_3\), then the composite map \(g \circ f\) on worlds is a bounded morphism from \(M_1\) to \(M_3\).

def comp (second : BoundedMorphism middle target)
    (first : BoundedMorphism source middle) : BoundedMorphism source target where
  toFun := second ∘ first
  atom_iff := by
    intro world atom
    exact (first.atom_iff world atom).trans (second.atom_iff (first world) atom)
  forth := fun h => second.forth (first.forth h)
  back := by
    intro world imageNext h
    obtain ⟨middleNext, hMiddle, rfl⟩ := second.back h
    obtain ⟨sourceNext, hSource, rfl⟩ := first.back hMiddle
    exact ⟨sourceNext, hSource, rfl⟩

Uses 2

Statement usesBounded morphism · Kripke model

TheoremInvariance of modal satisfaction under bounded morphisms#✓fully proved

Let \(f\) be a bounded morphism from a Kripke model \(M\) to a Kripke model \(N\) over the same atoms. Then for every modal formula \(\varphi\) and every world \(w\) of \(M\), \(w\) satisfies \(\varphi\) in \(M\) if and only if \(f(w)\) satisfies \(\varphi\) in \(N\).

theorem satisfies_iff (morphism : BoundedMorphism source middle)
    (phi : Formula Atom) (world : W) :
    source.Satisfies world phi ↔ middle.Satisfies (morphism world) phi

Uses 4 · Used by 1

Statement usesBounded morphism · Modal formulas · Kripke model · Satisfaction in a Kripke model

Used bySurjective bounded morphisms preserve and reflect validity

TheoremSurjective bounded morphisms preserve and reflect validity#✓fully proved

Let \(M\) and \(N\) be Kripke models over the same atoms and let \(f\) be a bounded morphism from \(M\) to \(N\) whose map on worlds is surjective. Then for every formula \(\varphi\), \(\varphi\) is globally valid in \(M\) if and only if \(\varphi\) is globally valid in \(N\).

theorem valid_iff_of_surjective (morphism : BoundedMorphism source middle)
    (surjective : Function.Surjective morphism) (phi : Formula Atom) :
    source.Valid phi ↔ middle.Valid phi

Uses 6

Statement usesBounded morphism · Modal formulas · Kripke model · Global validity in a Kripke model

Proof usesInvariance of modal satisfaction under bounded morphisms · Satisfaction in a Kripke model

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.