Normal modal logics

35 fully proved

Modal

InductiveTheorems of a normal modal logic#✓fully proved

Let \(\Lambda\) be a set of modal formulas. The theorems of the normal modal logic \(\mathbf{K} \oplus \Lambda\) form the least set of modal formulas that contains, for all modal formulas \(\varphi\), \(\psi\), \(\chi\), the propositional axioms \(\varphi \to (\psi \to \varphi)\), \((\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))\) and \(\neg\neg\varphi \to \varphi\) (where \(\neg\varphi\) is \(\varphi \to \bot\)) and the distribution axiom \(\Box(\varphi \to \psi) \to (\Box\varphi \to \Box\psi)\), that contains every member of \(\Lambda\), and that is closed under modus ponens (from \(\varphi \to \psi\) and \(\varphi\) infer \(\psi\)) and necessitation (from \(\varphi\) infer \(\Box\varphi\)).

inductive Derivable (Λ : Set (Formula Atom)) : Formula Atom → Prop
  | ax1 (phi psi : Formula Atom) : Derivable Λ (.imp phi (.imp psi phi))
  | ax2 (phi psi chi : Formula Atom) :
      Derivable Λ (.imp (.imp phi (.imp psi chi)) (.imp (.imp phi psi) (.imp phi chi)))
  | dne (phi : Formula Atom) : Derivable Λ (.imp phi.neg.neg phi)
  | distrib (phi psi : Formula Atom) : Derivable Λ (Formula.axiomK phi psi)
  | extra {phi : Formula Atom} : phi ∈ Λ → Derivable Λ phi
  | mp {phi psi : Formula Atom} : Derivable Λ (.imp phi psi) → Derivable Λ phi → Derivable Λ psi
  | nec {phi : Formula Atom} : Derivable Λ phi → Derivable Λ (.box phi)

Uses 3 · Used by 61

Statement usesModal formulas · Axiom K · Negation of modal formulas

Used byFinite-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 · The monotonicity rule for necessity · Local consequence in a normal modal logic · Consequences of no hypotheses are the theorems · Compactness of local modal consequence · The deduction theorem for local modal consequence, forward direction · Self-implication is a theorem · Monotonicity of theorems in the extra axioms · Monotonicity of local consequence in the hypotheses · 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 · Local soundness · 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 · Boxing an implication chain · The canonical model · Strong completeness of K · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Double-negation introduction under a box · Soundness and completeness of K · Completeness for CSLib's 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 · Existence lemma · Soundness for CSLib's K · Soundness for CSLib's S4 · Soundness for CSLib's S5 · Soundness for CSLib's T · 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

InductiveLocal consequence in a normal modal logic#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas. The local consequences of the hypotheses \(\Gamma\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\) form the least set of modal formulas that contains every member of \(\Gamma\) and every theorem of \(\mathbf{K} \oplus \Lambda\) and is closed under modus ponens: whenever it contains \(\varphi \to \psi\) and \(\varphi\), it contains \(\psi\).

Necessitation applies to theorems only, not to hypotheses.

inductive Deduces (Λ : Set (Formula Atom)) (Γ : Set (Formula Atom)) : Formula Atom → Prop
  | hyp {phi : Formula Atom} : phi ∈ Γ → Deduces Λ Γ phi
  | thm {phi : Formula Atom} : Derivable Λ phi → Deduces Λ Γ phi
  | mp {phi psi : Formula Atom} : Deduces Λ Γ (.imp phi psi) → Deduces Λ Γ phi → Deduces Λ Γ psi

Uses 2 · Used by 46

Statement usesTheorems of a normal modal logic · Modal formulas

Used byContradiction yields falsity · Consequences of no hypotheses are the theorems · The deduction theorem for local modal consequence · Compactness of local modal consequence · The deduction theorem for local modal consequence, forward direction · Hypothetical syllogism · Monotonicity of local consequence in the hypotheses · Double-negation introduction · Negation introduction · Ex falso quodlibet · Local consequences of theorems are theorems · Proof by contradiction · Local soundness · Transitivity of local consequence · Boxing an implication chain · 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 · Existence lemma · Discharging a list of hypotheses · 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 · Model existence from the canonical model · Model existence for S4 · Model existence for S5 · Model existence for T · Truth lemma

Axioms

DefinitionExtra axioms of the modal logic K#✓fully proved

The set of extra axioms of the normal modal logic K is the empty set of modal formulas over a given type of atoms; that is, K adds no axioms to the propositional axioms and the distribution axiom.

def K : Set (Formula Atom) := ∅

Uses 1 · Used by 12

Statement usesModal formulas

Used byFinite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · Finite model property of K · Completeness of K, countermodel form · Consistency of K · Soundness of K for Kripke models · Strong completeness of K · Strong soundness and completeness of K · Soundness and completeness of K · Completeness for CSLib's K · Soundness for CSLib's K · Model existence for K

DefinitionExtra axioms of T#✓fully proved

The extra axioms of the modal logic T are the formulas \(\Box\varphi \to \varphi\) (axiom T), for all modal formulas \(\varphi\).

def T : Set (Formula Atom) := Set.range Formula.axiomT

Uses 2 · Used by 10

Statement usesModal formulas · Axiom T

Used byT-provability via finite reflexive models · Finite model property of T · Consistency of T · Soundness of T for reflexive Kripke models · Strong completeness of T · Strong soundness and completeness of T · Completeness for CSLib's T · Soundness and completeness of T · Soundness for CSLib's T · Model existence for T

DefinitionExtra axioms of S4#✓fully proved

The extra axioms of the modal logic S4 are the formulas \(\Box\varphi \to \varphi\) (axiom T) and \(\Box\varphi \to \Box\Box\varphi\) (axiom 4), for all modal formulas \(\varphi\).

def S4 : Set (Formula Atom) := Set.range Formula.axiomT ∪ Set.range Formula.axiomFour

Uses 3 · Used by 10

Statement usesModal formulas · Axiom 4 · Axiom T

Used byS4-provability via finite reflexive transitive models · Finite model property of S4 · Consistency 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 · Soundness and completeness of S4 · Soundness for CSLib's S4 · Model existence for S4

DefinitionExtra axioms of S5#✓fully proved

For a modal formula \(\varphi\), write \(\Diamond\varphi\) for \(\neg\Box\neg\varphi\). The extra axioms of the modal logic S5 are the formulas \(\Box\varphi \to \varphi\) (axiom T) and \(\Diamond\varphi \to \Box\Diamond\varphi\) (axiom 5), for all modal formulas \(\varphi\).

def S5 : Set (Formula Atom) := Set.range Formula.axiomT ∪ Set.range Formula.axiomFive

Uses 3 · Used by 10

Statement usesModal formulas · Axiom 5 · Axiom T

Used byS5-provability via finite equivalence models · Finite model property of S5 · Consistency 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 · Soundness and completeness of S5 · Soundness for CSLib's S5 · Model existence for S5

Derivable

TheoremSelf-implication is a theorem#✓fully proved

Let \(\Lambda\) be a set of modal formulas. For every modal formula \(\varphi\), the formula \(\varphi \to \varphi\) is a theorem of the normal modal logic \(\mathbf{K} \oplus \Lambda\).

theorem imp_self (phi : Formula Atom) : Derivable Λ (.imp phi phi)

Uses 2 · Used by 2

Statement usesTheorems of a normal modal logic · Modal formulas

Used byThe deduction theorem for local modal consequence, forward direction · Boxing an implication chain

TheoremMonotonicity of theorems in the extra axioms#✓fully proved

Let \(\Lambda \subseteq \Lambda'\) be sets of modal formulas. Every theorem of the normal modal logic \(\mathrm{K} \oplus \Lambda\) is a theorem of \(\mathrm{K} \oplus \Lambda'\).

theorem mono (hΛ : Λ ⊆ Λ') {phi : Formula Atom} (h : Derivable Λ phi) : Derivable Λ' phi

Uses 4

Statement usesTheorems of a normal modal logic · Modal formulas

Proof usesAxiom K · Negation of modal formulas

Local consequence

TheoremMonotonicity of local consequence in the hypotheses#✓fully proved

Let \(\Lambda\), \(\Gamma\) and \(\Delta\) be sets of modal formulas with \(\Gamma \subseteq \Delta\). If a formula \(\varphi\) is a local consequence of the hypotheses \(\Gamma\) in the normal modal logic \(\mathrm{K} \oplus \Lambda\), then \(\varphi\) is a local consequence of the hypotheses \(\Delta\) in \(\mathrm{K} \oplus \Lambda\).

theorem mono (hΓ : Γ ⊆ Δ) (h : Deduces Λ Γ phi) : Deduces Λ Δ phi

Uses 3 · Used by 7

Statement usesLocal consequence in a normal modal logic · Modal formulas

Proof usesTheorems of a normal modal logic

Used byThe deduction theorem for local modal consequence · Compactness of local modal consequence · Hypothetical syllogism · Double-negation introduction · Consistency is of finite character · Existence lemma · Discharging a list of hypotheses

TheoremTransitivity of local consequence#✓fully proved

Let \(\Lambda\) be a set of modal formulas and let \(\Gamma\) and \(\Delta\) be sets of formulas such that every formula of \(\Delta\) is a local consequence of \(\Gamma\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\). If a formula \(\varphi\) is a local consequence of \(\Delta\) in \(\mathbf{K} \oplus \Lambda\), then \(\varphi\) is a local consequence of \(\Gamma\) in \(\mathbf{K} \oplus \Lambda\).

theorem trans (hΔ : ∀ psi ∈ Δ, Deduces Λ Γ psi) (h : Deduces Λ Δ phi) : Deduces Λ Γ phi

Uses 3 · Used by 1

Statement usesLocal consequence in a normal modal logic · Modal formulas

Proof usesTheorems of a normal modal logic

Used byLocal consequences of theorems are theorems

TheoremThe deduction theorem for local modal consequence, forward direction#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas and let \(\varphi\), \(\psi\) be modal formulas. If \(\varphi\) is a local consequence of \(\Gamma \cup \{\psi\}\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\), then \(\psi \to \varphi\) is a local consequence of \(\Gamma\) in \(\mathbf{K} \oplus \Lambda\).

theorem imp_of_insert (h : Deduces Λ (insert psi Γ) phi) : Deduces Λ Γ (.imp psi phi)

Uses 4 · Used by 8

Statement usesLocal consequence in a normal modal logic · Modal formulas

Proof usesTheorems of a normal modal logic · Self-implication is a theorem

Used byThe deduction theorem for local modal consequence · Hypothetical syllogism · Negation introduction · Proof by contradiction · Boxing an implication chain · Double-negation introduction under a box · Discharging a list of hypotheses · Truth lemma

TheoremThe deduction theorem for local modal consequence#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas and let \(\varphi\), \(\psi\) be modal formulas. In the normal modal logic \(\mathbf{K} \oplus \Lambda\), \(\varphi\) is a local consequence of \(\Gamma \cup \{\psi\}\) if and only if \(\psi \to \varphi\) is a local consequence of \(\Gamma\).

theorem _root_.Cslib.Modal.deduces_insert_iff :
    Deduces Λ (insert psi Γ) phi ↔ Deduces Λ Γ (.imp psi phi)

Uses 4

Statement usesLocal consequence in a normal modal logic · Modal formulas

Proof usesThe deduction theorem for local modal consequence, forward direction · Monotonicity of local consequence in the hypotheses

TheoremConsequences of no hypotheses are the theorems#✓fully proved

Let \(\Lambda\) be a set of modal formulas. A modal formula \(\varphi\) is a local consequence of the empty set of hypotheses in the normal modal logic \(\mathbf{K} \oplus \Lambda\) if and only if \(\varphi\) is a theorem of \(\mathbf{K} \oplus \Lambda\).

theorem _root_.Cslib.Modal.deduces_empty_iff : Deduces Λ ∅ phi ↔ Derivable Λ phi

Uses 3 · Used by 10

Statement usesLocal consequence in a normal modal logic · Theorems of a normal modal logic · Modal formulas

Used byLocal consequences of theorems are theorems · Boxing an implication chain · The canonical model · Double-negation introduction under a box · 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 · Existence lemma

TheoremCompactness of local modal consequence#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas. If a modal formula \(\varphi\) is a local consequence of the hypotheses \(\Gamma\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\), then there is a finite set \(\Delta \subseteq \Gamma\) such that \(\varphi\) is a local consequence of \(\Delta\) in \(\mathbf{K} \oplus \Lambda\).

theorem exists_finset (h : Deduces Λ Γ phi) :
    ∃ Δ : Finset (Formula Atom), ↑Δ ⊆ Γ ∧ Deduces Λ ↑Δ phi

Uses 4 · Used by 2

Statement usesLocal consequence in a normal modal logic · Modal formulas

Proof usesMonotonicity of local consequence in the hypotheses · Theorems of a normal modal logic

Used byConsistency is of finite character · Existence lemma

TheoremEx falso quodlibet#✓fully proved

Let \(\Lambda\) be a set of modal formulas and \(\Gamma\) a set of hypotheses. If \(\bot\) is a local consequence of \(\Gamma\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\), then every formula \(\varphi\) is a local consequence of \(\Gamma\) in \(\mathbf{K} \oplus \Lambda\).

theorem of_bot (h : Deduces Λ Γ .bot) : Deduces Λ Γ phi

Uses 4 · Used by 2

Statement usesLocal consequence in a normal modal logic · Modal formulas

Proof usesTheorems of a normal modal logic · Negation of modal formulas

Used byValidity in a class containing the canonical model gives derivability · Truth lemma

TheoremContradiction yields falsity#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas and let \(\varphi\) be a modal formula. If both \(\varphi\) and its negation \(\neg\varphi\) are local consequences of the hypotheses \(\Gamma\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\), then so is \(\bot\).

theorem bot_of_neg (h₁ : Deduces Λ Γ phi) (h₂ : Deduces Λ Γ phi.neg) : Deduces Λ Γ .bot

Uses 3 · Used by 3

Statement usesLocal consequence in a normal modal logic · Modal formulas · Negation of modal formulas

Used byDouble-negation introduction · Maximal consistent sets of modal formulas are deductively closed · Truth lemma

TheoremProof by contradiction#✓fully proved

Let \(\Lambda\) be a set of modal formulas, \(\Gamma\) a set of hypotheses and \(\varphi\) a formula. If \(\bot\) is a local consequence of \(\Gamma \cup \{\neg\varphi\}\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\), then \(\varphi\) is a local consequence of \(\Gamma\) in \(\mathbf{K} \oplus \Lambda\).

theorem of_insert_neg (h : Deduces Λ (insert phi.neg Γ) .bot) : Deduces Λ Γ phi

Uses 5 · Used by 2

Statement usesLocal consequence in a normal modal logic · Modal formulas · Negation of modal formulas

Proof usesThe deduction theorem for local modal consequence, forward direction · Theorems of a normal modal logic

Used byExistence lemma · Deducibility from maximal consistent extensions

TheoremNegation introduction#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas and \(\varphi\) a formula. If \(\bot\) is a local consequence of the hypotheses \(\Gamma \cup \{\varphi\}\) in the normal modal logic \(\mathrm{K} \oplus \Lambda\), then \(\neg\varphi\) is a local consequence of \(\Gamma\) in \(\mathrm{K} \oplus \Lambda\), where \(\neg\varphi\) abbreviates \(\varphi \to \bot\).

theorem neg_of_insert (h : Deduces Λ (insert phi Γ) .bot) : Deduces Λ Γ phi.neg

Uses 4 · Used by 6

Statement usesLocal consequence in a normal modal logic · Modal formulas · Negation of modal formulas

Proof usesThe deduction theorem for local modal consequence, forward direction

Used byDouble-negation introduction · Strong completeness of S5 · Completeness for CSLib's S5 · Maximal consistent sets of modal formulas are deductively closed · Model existence for S5 · Truth lemma

TheoremHypothetical syllogism#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas and let \(\varphi\), \(\psi\), \(\chi\) be modal formulas. If \(\varphi \to \psi\) and \(\psi \to \chi\) are local consequences of the hypotheses \(\Gamma\) in the normal modal logic \(\mathbf{K} \oplus \Lambda\), then so is \(\varphi \to \chi\).

theorem imp_trans (h₁ : Deduces Λ Γ (.imp phi psi)) (h₂ : Deduces Λ Γ (.imp psi chi)) :
    Deduces Λ Γ (.imp phi chi)

Uses 4

Statement usesLocal consequence in a normal modal logic · Modal formulas

Proof usesThe deduction theorem for local modal consequence, forward direction · Monotonicity of local consequence in the hypotheses

TheoremDouble-negation introduction#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas. If a formula \(\varphi\) is a local consequence of the hypotheses \(\Gamma\) in the normal modal logic \(\mathrm{K} \oplus \Lambda\), then so is \(\neg\neg\varphi\), where \(\neg\psi\) abbreviates \(\psi \to \bot\).

theorem neg_neg (h : Deduces Λ Γ phi) : Deduces Λ Γ phi.neg.neg

Uses 6 · Used by 1

Statement usesLocal consequence in a normal modal logic · Modal formulas · Negation of modal formulas

Proof usesContradiction yields falsity · Monotonicity of local consequence in the hypotheses · Negation introduction

Used byDouble-negation introduction under a box

Derivable

TheoremLocal consequences of theorems are theorems#✓fully proved

Let \(\Lambda\) be a set of modal formulas and let \(\Gamma\) be a set of formulas each of which is a theorem of the normal modal logic \(\mathbf{K} \oplus \Lambda\). If a formula \(\varphi\) is a local consequence of \(\Gamma\) in \(\mathbf{K} \oplus \Lambda\), then \(\varphi\) is a theorem of \(\mathbf{K} \oplus \Lambda\).

theorem of_deduces {Γ : Set (Formula Atom)} (hΓ : ∀ psi ∈ Γ, Derivable Λ psi)
    (h : Deduces Λ Γ phi) : Derivable Λ phi

Uses 5

Statement usesLocal consequence in a normal modal logic · Theorems of a normal modal logic · Modal formulas

Proof usesTransitivity of local consequence · Consequences of no hypotheses are the theorems

TheoremThe monotonicity rule for necessity#✓fully proved

Let \(\Lambda\) be a set of modal formulas and let \(\varphi\), \(\psi\) be modal formulas. If \(\varphi \to \psi\) is a theorem of the normal modal logic \(\mathbf{K} \oplus \Lambda\), then so is \(\Box\varphi \to \Box\psi\).

theorem box_imp_box (h : Derivable Λ (.imp phi psi)) : Derivable Λ (.imp (.box phi) (.box psi))

Uses 3 · Used by 1

Statement usesTheorems of a normal modal logic · Modal formulas

Proof usesAxiom K

Used byDouble-negation introduction under a box

Modal

TheoremSoundness of modal Hilbert systems for Kripke models#✓fully proved

Let \(\Lambda\) be a set of modal formulas and \(M\) a Kripke model in which every formula of \(\Lambda\) is valid. Then every formula derivable in \(K \oplus \Lambda\) (from the propositional axioms, the distribution axiom and the members of \(\Lambda\) by modus ponens and necessitation) is valid in \(M\), that is, it holds at every world of \(M\).

theorem Derivable.valid (hΛ : ∀ psi ∈ Λ, M.Valid psi) {phi : Formula Atom}
    (h : Derivable Λ phi) : M.Valid phi

Uses 8 · Used by 6

Statement usesTheorems of a normal modal logic · Modal formulas · Kripke model · Global validity in a Kripke model

Proof usesAxiom K · Negation of modal formulas · Satisfaction in a Kripke model · Validity of axiom K on Kripke models

Used byConsistency of normal modal logics · Local soundness · 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

TheoremLocal soundness#✓fully proved

Let \(M\) be a Kripke model and \(\Lambda\) a set of modal formulas each of which is valid in \(M\). If a formula \(\varphi\) is a local consequence of a set \(\Gamma\) of formulas in the normal modal logic \(\mathbf{K} \oplus \Lambda\), then \(\varphi\) holds at every world of \(M\) at which every formula of \(\Gamma\) holds.

theorem Deduces.satisfies (hΛ : ∀ psi ∈ Λ, M.Valid psi) {Γ : Set (Formula Atom)}
    {phi : Formula Atom} (h : Deduces Λ Γ phi) {world : World}
    (hΓ : ∀ psi ∈ Γ, M.Satisfies world psi) : M.Satisfies world phi

Uses 7 · Used by 4

Statement usesLocal consequence in a normal modal logic · Modal formulas · Kripke model · Satisfaction in a Kripke model · Global validity in a Kripke model

Proof usesTheorems of a normal modal logic · Soundness of modal Hilbert systems for Kripke models

Used byStrong soundness and completeness of K · Strong soundness and completeness of S4 · Strong soundness and completeness of S5 · Strong soundness and completeness of T

TheoremSoundness of K for Kripke models#✓fully proved

Every theorem of the modal logic K is valid in every Kripke model: if a formula \(\varphi\) is derivable in K, then \(\varphi\) holds at every world of every Kripke model \(M\).

theorem Derivable.valid_K {phi : Formula Atom} (h : Derivable Axioms.K phi) : M.Valid phi

Uses 6 · Used by 5

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Modal formulas · Kripke model · Global validity in a Kripke model

Proof usesSoundness of modal Hilbert systems for Kripke models

Used byFinite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · Consistency of K · Soundness and completeness of K · Soundness for CSLib's K

TheoremSoundness of T for reflexive Kripke models#✓fully proved

If the accessibility relation of a Kripke model \(M\) is reflexive, then every formula derivable in the modal logic T is valid in \(M\), that is, it holds at every world of \(M\).

theorem Derivable.valid_T (refl : ∀ world, M.rel world world) {phi : Formula Atom}
    (h : Derivable Axioms.T phi) : M.Valid phi

Uses 8 · Used by 4

Statement usesExtra axioms of T · Theorems of a normal modal logic · Modal formulas · Kripke model · Global validity in a Kripke model

Proof usesSoundness of modal Hilbert systems for Kripke models · Axiom T · Axiom T is valid on reflexive Kripke models

Used byT-provability via finite reflexive models · Consistency of T · Soundness and completeness of T · Soundness for CSLib's T

TheoremSoundness of S4 for reflexive transitive Kripke models#✓fully proved

If the accessibility relation of a Kripke model \(M\) is reflexive and transitive, then every formula derivable in the modal logic S4 is valid in \(M\), that is, it holds at every world of \(M\).

theorem Derivable.valid_S4 (refl : ∀ world, M.rel world world)
    (trans : ∀ {first second third}, M.rel first second → M.rel second third →
      M.rel first third)
    {phi : Formula Atom} (h : Derivable Axioms.S4 phi) : M.Valid phi

Uses 10 · Used by 4

Statement usesExtra axioms of S4 · Theorems of a normal modal logic · Modal formulas · Kripke model · Global validity in a Kripke model

Proof usesSoundness of modal Hilbert systems for Kripke models · Axiom 4 · Axiom T · Axiom 4 is valid on transitive Kripke models · Axiom T is valid on reflexive Kripke models

Used byS4-provability via finite reflexive transitive models · Consistency of S4 · Soundness and completeness of S4 · Soundness for CSLib's S4

TheoremSoundness of S5 for Kripke models with an equivalence relation#✓fully proved

If the accessibility relation of a Kripke model \(M\) is an equivalence relation, then every formula derivable in the modal logic S5 is valid in \(M\), that is, it holds at every world of \(M\).

theorem Derivable.valid_S5 (equiv : Equivalence M.rel) {phi : Formula Atom}
    (h : Derivable Axioms.S5 phi) : M.Valid phi

Uses 10 · Used by 4

Statement usesExtra axioms of S5 · Theorems of a normal modal logic · Modal formulas · Kripke model · Global validity in a Kripke model

Proof usesSoundness of modal Hilbert systems for Kripke models · Axiom 5 · Axiom T · Axiom 5 is valid on euclidean Kripke models · Axiom T is valid on reflexive Kripke models

Used byS5-provability via finite equivalence models · Consistency of S5 · Soundness and completeness of S5 · Soundness for CSLib's S5

DefinitionThe one-world Kripke model#✓fully proved

For any type of atoms, the one-world Kripke model has a single world, which sees itself, and every atom is false at that world.

def KripkeModel.unit : KripkeModel PUnit.{1} Atom where
  nonempty_world := ⟨PUnit.unit⟩
  rel _ _ := True
  valuation _ _ := False

Uses 1 · Used by 6

Statement usesKripke model

Used byConsistency of normal modal logics · Consistency of K · Consistency of S4 · Consistency of S5 · Consistency of T · The one-world model has an equivalence relation

TheoremThe one-world model has an equivalence relation#✓fully proved

The accessibility relation of the one-world Kripke model, whose single world sees itself and at which every atom is false, is an equivalence relation.

theorem KripkeModel.unit_equivalence : Equivalence (KripkeModel.unit (Atom := Atom)).rel

Uses 2 · Used by 1

Statement usesKripke model · The one-world Kripke model

Used byConsistency of S5

TheoremConsistency of normal modal logics#✓fully proved

Let \(\Lambda\) be a set of modal formulas each of which is valid in the one-world Kripke model whose world sees itself and in which every atom is false. Then \(\bot\) is not a theorem of the normal modal logic \(\mathrm{K} \oplus \Lambda\).

theorem not_derivable_bot (hΛ : ∀ psi ∈ Λ, KripkeModel.unit.Valid psi) : ¬Derivable Λ .bot

Uses 5

Statement usesTheorems of a normal modal logic · Modal formulas · Global validity in a Kripke model · The one-world Kripke model

Proof usesSoundness of modal Hilbert systems for Kripke models

TheoremConsistency of S5#✓fully proved

For every type of atoms, \(\bot\) is not a theorem of the normal modal logic S5, whose extra axioms are the formulas \(\Box\varphi \to \varphi\) and \(\Diamond\varphi \to \Box\Diamond\varphi\), where \(\Diamond\varphi\) abbreviates \(\neg\Box\neg\varphi\) and \(\neg\psi\) abbreviates \(\psi \to \bot\).

theorem not_derivable_bot_S5 : ¬Derivable (Axioms.S5 : Set (Formula Atom)) .bot

Uses 6 · Used by 1

Statement usesExtra axioms of S5 · Theorems of a normal modal logic · Modal formulas

Proof usesSoundness of S5 for Kripke models with an equivalence relation · The one-world Kripke model · The one-world model has an equivalence relation

Used byStrong completeness of S5

TheoremConsistency of S4#✓fully proved

For every type of atoms, \(\bot\) is not a theorem of the normal modal logic S4, whose extra axioms are the formulas \(\Box\varphi \to \varphi\) and \(\Box\varphi \to \Box\Box\varphi\).

theorem not_derivable_bot_S4 : ¬Derivable (Axioms.S4 : Set (Formula Atom)) .bot

Uses 6 · Used by 1

Statement usesExtra axioms of S4 · Theorems of a normal modal logic · Modal formulas

Proof usesSoundness of S4 for reflexive transitive Kripke models · Kripke model · The one-world Kripke model

Used byStrong completeness of S4

TheoremConsistency of T#✓fully proved

For every type of atoms, \(\bot\) is not a theorem of the normal modal logic T, whose extra axioms are the formulas \(\Box\varphi \to \varphi\).

theorem not_derivable_bot_T : ¬Derivable (Axioms.T : Set (Formula Atom)) .bot

Uses 5 · Used by 1

Statement usesExtra axioms of T · Theorems of a normal modal logic · Modal formulas

Proof usesSoundness of T for reflexive Kripke models · The one-world Kripke model

Used byStrong completeness of T

TheoremConsistency of K#✓fully proved

For every type of atoms, \(\bot\) is not a theorem of the normal modal logic K, the logic with no extra axioms.

theorem not_derivable_bot_K : ¬Derivable (Axioms.K : Set (Formula Atom)) .bot

Uses 5 · Used by 1

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Modal formulas

Proof usesSoundness of K for Kripke models · The one-world Kripke model

Used byStrong completeness of K

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.