Soundness and completeness of normal modal logics

DefinitionTranslation of CSLib's modal propositions#✓fully proved

CSLib's unimodal propositions are translated into modal formulas in the \(\bot\), \(\to\), \(\Box\) basis by recursion, writing \(\varphi'\) for the translation of \(\varphi\): an atom \(p\) goes to \(p\), falsehood to \(\bot\), \(\neg\varphi\) to \(\varphi' \to \bot\), \(\varphi \lor \psi\) to \((\varphi' \to \bot) \to \psi'\), and the diamond (the unimodal triangle) applied to \(\varphi\) goes to \(\Diamond\varphi'\), that is, to \(\Box(\varphi' \to \bot) \to \bot\).

def Formula.ofProposition : Logic.Modal.Unimodal.Proposition Atom → Formula Atom
  | .atom p => .atom p
  | .false => .bot
  | .not phi => (ofProposition phi).neg
  | .or phi psi => (ofProposition phi).or (ofProposition psi)
  | .triangle _ phis => (ofProposition (phis default)).dia
termination_by structural phi => phi

Uses 4 · Used by 11

Statement usesModal formulas · The possibility operator · Negation of modal formulas · Disjunction of modal formulas

Used byCompleteness 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 for CSLib's K · Validity of the translation gives membership in CSLib's logic · Soundness for CSLib's S4 · Soundness for CSLib's S5 · Soundness for CSLib's T · The translation preserves satisfaction

DefinitionKripke model of a CSLib model#✓fully proved

For a CSLib unimodal model \(m\) on a nonempty type of worlds, the associated Kripke model has the same worlds, the binary accessibility relation of \(m\) as its accessibility relation, and the valuation of \(m\) as its valuation.

def KripkeModel.ofModel [Nonempty World] (m : Logic.Modal.Unimodal.Model World Atom) :
    KripkeModel World Atom where
  nonempty_world := inferInstance
  rel := m.rel
  valuation := m.v

Uses 1 · Used by 9

Statement usesKripke model

Used byValidity in a class containing the canonical model gives derivability · Soundness for CSLib's K · Validity of the translation gives membership in CSLib's logic · Soundness for CSLib's S4 · Soundness for CSLib's S5 · Soundness for CSLib's T · Kripke to CSLib and back is the identity · The translation preserves satisfaction · Round trip from CSLib models through Kripke models

TheoremThe translation preserves satisfaction#✓fully proved

Let \(m\) be a CSLib unimodal model on a nonempty type of worlds, \(w\) a world and \(\varphi\) a CSLib unimodal proposition. Then the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis holds at \(w\) in the Kripke model of \(m\) if and only if \(\varphi\) holds at \(w\) in \(m\).

theorem satisfies_ofProposition [Nonempty World]
    (m : Logic.Modal.Unimodal.Model World Atom) (w : World)
    (phi : Logic.Modal.Unimodal.Proposition Atom) :
    (KripkeModel.ofModel m).Satisfies w (Formula.ofProposition phi) ↔
      Logic.Modal.Satisfies m w phi

Uses 9 · Used by 2

Statement usesTranslation of CSLib's modal propositions · Satisfaction in a Kripke model · Kripke model of a CSLib model

Proof usesModal formulas · The possibility operator · Negation of modal formulas · Disjunction of modal formulas · Kripke model · Semantics of possibility

Used byValidity in a class containing the canonical model gives derivability · Validity of the translation gives membership in CSLib's logic

DefinitionThe CSLib unimodal model of a Kripke model#✓fully proved

A Kripke model \(k\) on worlds \(W\) gives the CSLib unimodal model on \(W\) whose frame is the unimodal frame built from the accessibility relation of \(k\) and whose valuation is the valuation of \(k\).

def KripkeModel.toModel (k : KripkeModel World Atom) :
    Logic.Modal.Unimodal.Model World Atom where
  toFrame := Frame.ofRelation k.rel
  v := k.valuation

Uses 1 · Used by 4

Statement usesKripke model

Used byKripke to CSLib and back is the identity · The reverse translation preserves satisfaction · Round trip from CSLib models through Kripke models · Validity agrees with its CSLib translation

TheoremKripke to CSLib and back is the identity#✓fully proved

Let \(k\) be a Kripke model on a nonempty type of worlds. Converting \(k\) to a CSLib unimodal model and converting that model back to a Kripke model gives \(k\).

theorem KripkeModel.ofModel_toModel [Nonempty World] (k : KripkeModel World Atom) :
    KripkeModel.ofModel (KripkeModel.toModel k) = k

Uses 3

Statement usesKripke model · Kripke model of a CSLib model · The CSLib unimodal model of a Kripke model

TheoremRound trip from CSLib models through Kripke models#✓fully proved

For a nonempty type of worlds \(W\), converting a CSLib unimodal model \(m\) on \(W\) into a Kripke model and then back into a CSLib unimodal model returns \(m\): a unimodal frame is determined by its binary accessibility relation.

theorem KripkeModel.toModel_ofModel [Nonempty World]
    (m : Logic.Modal.Unimodal.Model World Atom) :
    (KripkeModel.ofModel m).toModel = m

Uses 2

Statement usesKripke model of a CSLib model · The CSLib unimodal model of a Kripke model

DefinitionTranslation of modal formulas into CSLib propositions#✓fully proved

Each modal formula built from atoms, \(\bot\), \(\to\) and \(\Box\) is translated into a CSLib unimodal proposition by recursion: an atom \(p\) goes to the atom \(p\), \(\bot\) goes to false, \(\varphi \to \psi\) goes to \(\neg\varphi' \lor \psi'\), and \(\Box\varphi\) goes to \(\neg\Diamond\neg\varphi'\), where \(\varphi'\) and \(\psi'\) are the translations of \(\varphi\) and \(\psi\) and \(\Diamond\) is the possibility operator of CSLib's unimodal language.

def Formula.toProposition : Formula Atom → Logic.Modal.Unimodal.Proposition Atom
  | .atom p => .atom p
  | .bot => .false
  | .imp phi psi => .or (.not (toProposition phi)) (toProposition psi)
  | .box phi => .not (.triangle default (fun _ => .not (toProposition phi)))

Uses 1 · Used by 2

Statement usesModal formulas

Used byThe reverse translation preserves satisfaction · Validity agrees with its CSLib translation

TheoremThe reverse translation preserves satisfaction#✓fully proved

Let \(k\) be a Kripke model, \(w\) a world and \(\varphi\) a modal formula in the \(\bot\), \(\to\), \(\Box\) basis. Then \(\varphi\) holds at \(w\) in \(k\) if and only if its translation into a CSLib unimodal proposition holds at \(w\) in the CSLib model associated with \(k\).

Together with the preservation of satisfaction by the forward translation and the two model round trips, this shows that the two presentations have the same unimodal semantics.

theorem satisfies_toProposition (k : KripkeModel World Atom) (w : World)
    (phi : Formula Atom) :
    k.Satisfies w phi ↔ Logic.Modal.Satisfies k.toModel w (Formula.toProposition phi)

Uses 5 · Used by 1

Statement usesModal formulas · Translation of modal formulas into CSLib propositions · Kripke model · Satisfaction in a Kripke model · The CSLib unimodal model of a Kripke model

Used byValidity agrees with its CSLib translation

TheoremValidity agrees with its CSLib translation#✓fully proved

A modal formula \(\varphi\) is valid in a Kripke model \(k\) (true at every world of \(k\)) if and only if its translation into a CSLib unimodal proposition is satisfied at every world of the CSLib unimodal model associated with \(k\).

theorem KripkeModel.valid_toProposition (k : KripkeModel World Atom)
    (phi : Formula Atom) :
    k.Valid phi ↔
      ∀ w, Logic.Modal.Satisfies k.toModel w (Formula.toProposition phi)

Uses 7

Statement usesModal formulas · Translation of modal formulas into CSLib propositions · Kripke model · Global validity in a Kripke model · The CSLib unimodal model of a Kripke model

Proof usesSatisfaction in a Kripke model · The reverse translation preserves satisfaction

TheoremValidity of the translation gives membership in CSLib's logic#✓fully proved

Let \(S\) be a class of CSLib unimodal models on a type of worlds and \(\varphi\) a CSLib unimodal proposition. Suppose that, if the type of worlds is nonempty, the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is valid in the Kripke model of every model in \(S\). Then \(\varphi\) belongs to CSLib's semantic logic of \(S\): it holds at every world of every model in \(S\).

theorem mem_logic_of_valid {S : Set (Logic.Modal.Unimodal.Model World Atom)}
    {phi : Logic.Modal.Unimodal.Proposition Atom}
    (h : ∀ m ∈ S, ∀ _ : Nonempty World, (KripkeModel.ofModel m).Valid (Formula.ofProposition phi)) :
    phi ∈ Logic.Modal.logic S

Uses 5 · Used by 4

Statement usesTranslation of CSLib's modal propositions · Global validity in a Kripke model · Kripke model of a CSLib model

Proof usesSatisfaction in a Kripke model · The translation preserves satisfaction

Used bySoundness for CSLib's K · Soundness for CSLib's S4 · Soundness for CSLib's S5 · Soundness for CSLib's T

TheoremSoundness for CSLib's K#✓fully proved

Let \(\varphi\) be a CSLib unimodal proposition. If the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of the Hilbert system K, then, for every type of worlds, \(\varphi\) belongs to CSLib's modal logic K: it holds at every world of every CSLib unimodal model on that type.

theorem mem_K (h : Derivable Axioms.K (Formula.ofProposition phi)) :
    phi ∈ Logic.Modal.Unimodal.K World Atom

Uses 6 · Used by 1

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesSoundness of K for Kripke models · Kripke model of a CSLib model · Validity of the translation gives membership in CSLib's logic

Used byCompleteness for CSLib's K

TheoremSoundness for CSLib's T#✓fully proved

Let \(\varphi\) be a CSLib unimodal proposition. If the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of the Hilbert system T, then, for every type of worlds, \(\varphi\) belongs to CSLib's modal logic T: it holds at every world of every CSLib unimodal model on that type whose accessibility relation is reflexive.

theorem mem_T (h : Derivable Axioms.T (Formula.ofProposition phi)) :
    phi ∈ Logic.Modal.Unimodal.T World Atom

Uses 6 · Used by 1

Statement usesExtra axioms of T · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesSoundness of T for reflexive Kripke models · Kripke model of a CSLib model · Validity of the translation gives membership in CSLib's logic

Used byCompleteness for CSLib's T

TheoremSoundness for CSLib's S4#✓fully proved

Let \(\varphi\) be a CSLib unimodal proposition. If the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of the Hilbert system S4, then, for every type of worlds, \(\varphi\) belongs to CSLib's modal logic S4: it holds at every world of every CSLib unimodal model on that type whose accessibility relation is reflexive and transitive.

theorem mem_S4 (h : Derivable Axioms.S4 (Formula.ofProposition phi)) :
    phi ∈ Logic.Modal.Unimodal.S4 World Atom

Uses 7 · Used by 1

Statement usesExtra axioms of S4 · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesSoundness of S4 for reflexive transitive Kripke models · Kripke model · Kripke model of a CSLib model · Validity of the translation gives membership in CSLib's logic

Used byCompleteness for CSLib's S4

TheoremSoundness for CSLib's S5#✓fully proved

Let \(\varphi\) be a CSLib unimodal proposition. If the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of the Hilbert system S5, then, for every type of worlds, \(\varphi\) belongs to CSLib's modal logic S5: it holds at every world of every CSLib unimodal model on that type whose accessibility relation \(R\) is reflexive, transitive and Euclidean (\(R(w, u)\) and \(R(w, v)\) imply \(R(u, v)\)).

theorem mem_S5 (h : Derivable Axioms.S5 (Formula.ofProposition phi)) :
    phi ∈ Logic.Modal.Unimodal.S5 World Atom

Uses 7 · Used by 1

Statement usesExtra axioms of S5 · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesSoundness of S5 for Kripke models with an equivalence relation · Kripke model · Kripke model of a CSLib model · Validity of the translation gives membership in CSLib's logic

Used byCompleteness for CSLib's S5

DefinitionConsistency relative to a normal modal logic#✓fully proved

For sets of formulas \(\Lambda\) and \(\Gamma\), the set \(\Gamma\) is consistent relative to \(K \oplus \Lambda\) when \(\bot\) is not deducible from \(\Gamma\) in \(K \oplus \Lambda\).

def Consistent (Λ Γ : Set (Formula Atom)) : Prop := ¬Deduces Λ Γ .bot

Uses 2 · Used by 24

Statement usesLocal consequence in a normal modal logic · Modal formulas

Used byThe canonical model as a CSLib model · The canonical model · Worlds of the canonical model · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Consistency is of finite character · 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 · Lindenbaum's lemma for normal modal logics · Existence lemma · 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 · 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

TheoremConsistency is of finite character#✓fully proved

For every set \(\Lambda\) of extra axioms, a set of formulas is consistent relative to \(K \oplus \Lambda\) iff all its finite subsets are.

theorem consistent_isOfFiniteCharacter :
    Order.IsOfFiniteCharacter {M : Set (Formula Atom) | Consistent Λ M}

Uses 5 · Used by 1

Statement usesConsistency relative to a normal modal logic · Modal formulas

Proof usesLocal consequence in a normal modal logic · Compactness of local modal consequence · Monotonicity of local consequence in the hypotheses

Used byLindenbaum's lemma for normal modal logics

TheoremLindenbaum's lemma for normal modal logics#✓fully proved

Let \(\Lambda\) be a set of modal formulas and \(\mathrm{K} \oplus \Lambda\) the normal modal logic K extended by the axioms \(\Lambda\). Every set \(\Gamma\) of modal formulas that is consistent relative to \(\mathrm{K} \oplus \Lambda\) is contained in a set \(M\) of modal formulas that is maximal among the sets consistent relative to \(\mathrm{K} \oplus \Lambda\).

The proof applies the Teichmüller–Tukey lemma: consistency is a property of finite character.

theorem exists_maximal_consistent {Γ : Set (Formula Atom)} (hΓ : Consistent Λ Γ) :
    ∃ M, Γ ⊆ M ∧ Maximal (Consistent Λ) M

Uses 3 · Used by 4

Statement usesConsistency relative to a normal modal logic · Modal formulas

Proof usesConsistency is of finite character

Used byThe canonical model · Existence lemma · Deducibility from maximal consistent extensions · Model existence from the canonical model

TheoremMaximal consistent sets of modal formulas are deductively closed#✓fully proved

Let \(\Lambda\) be a set of modal formulas and \(M\) a set of modal formulas that is maximal among the sets consistent relative to the normal modal logic K extended by the axioms \(\Lambda\). Every formula that is a local consequence of \(M\) in that logic belongs to \(M\).

theorem mem_of_deduces {phi : Formula Atom} (h : Deduces Λ M phi) : phi ∈ M

Uses 6 · Used by 13

Statement usesConsistency relative to a normal modal logic · Local consequence in a normal modal logic · Modal formulas

Proof usesContradiction yields falsity · Negation introduction · Negation of modal formulas

Used byStrong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Completeness for CSLib's S4 · Completeness for CSLib's S5 · Completeness for CSLib's T · Existence lemma · Iterated modus ponens in maximal consistent sets · Deducibility from maximal consistent extensions · Model existence for S4 · Model existence for S5 · Model existence for T · Truth lemma

TheoremIterated modus ponens in maximal consistent sets#✓fully proved

Let \(\Lambda\) be a set of modal formulas, \(M\) a set of modal formulas that is maximal among the sets consistent relative to the normal modal logic K extended by the axioms \(\Lambda\), and \(\varphi\) and \(\gamma_1, \dots, \gamma_n\) modal formulas. If \(\gamma_1 \to (\gamma_2 \to \cdots \to (\gamma_n \to \varphi) \cdots) \in M\) and \(\gamma_1, \dots, \gamma_n \in M\), then \(\varphi \in M\).

theorem mem_of_foldr_imp_mem {l : List (Formula Atom)} {phi : Formula Atom}
    (h : l.foldr .imp phi ∈ M) (hl : ∀ psi ∈ l, psi ∈ M) : phi ∈ M

Uses 4 · Used by 1

Statement usesConsistency relative to a normal modal logic · Modal formulas

Proof usesLocal consequence in a normal modal logic · Maximal consistent sets of modal formulas are deductively closed

Used byExistence lemma

TheoremDischarging a list of hypotheses#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas, \(\varphi\) a modal formula and \(\gamma_1, \dots, \gamma_n\) a list of modal formulas. If \(\varphi\) is a local consequence of \(\Gamma \cup \{\gamma_1, \dots, \gamma_n\}\) in the normal modal logic K extended by the axioms \(\Lambda\), then \(\gamma_1 \to (\gamma_2 \to \cdots \to (\gamma_n \to \varphi) \cdots)\) is a local consequence of \(\Gamma\) in the same logic.

theorem Deduces.foldr_imp {Γ : Set (Formula Atom)} {l : List (Formula Atom)}
    {phi : Formula Atom} (h : Deduces Λ (Γ ∪ {x | x ∈ l}) phi) :
    Deduces Λ Γ (l.foldr .imp phi)

Uses 4 · Used by 1

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

Used byExistence lemma

TheoremBoxing an implication chain#✓fully proved

Let \(\Lambda\) be a set of extra axioms, let \(\gamma_1, \dots, \gamma_n\) be formulas (with \(n \ge 0\)) and let \(\varphi\) be a formula. Then \(\Box(\gamma_1 \to \cdots \to \gamma_n \to \varphi) \to (\Box\gamma_1 \to \cdots \to \Box\gamma_n \to \Box\varphi)\) is a theorem of \(K \oplus \Lambda\).

theorem Derivable.box_foldr_imp (l : List (Formula Atom)) (phi : Formula Atom) :
    Derivable Λ (.imp (.box (l.foldr .imp phi)) ((l.map .box).foldr .imp (.box phi)))

Uses 7 · Used by 1

Statement usesTheorems of a normal modal logic · Modal formulas

Proof usesLocal consequence in a normal modal logic · The deduction theorem for local modal consequence, forward direction · Self-implication is a theorem · Axiom K · Consequences of no hypotheses are the theorems

Used byExistence lemma

DefinitionWorlds of the canonical model#✓fully proved

For a set \(\Lambda\) of extra axioms, the worlds of the canonical model of \(K \oplus \Lambda\) are the maximal consistent sets of \(K \oplus \Lambda\): the sets of formulas that are consistent relative to \(K \oplus \Lambda\) and have no consistent proper superset.

def CanonicalWorld (Λ : Set (Formula Atom)) : Type u :=
  {M : Set (Formula Atom) // Maximal (Consistent Λ) M}

Uses 2 · Used by 20

Statement usesConsistency relative to a normal modal logic · Modal formulas

Used byThe canonical model as a CSLib model · The canonical model · Strong completeness of K · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · 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 · Existence lemma · Deducibility from maximal consistent extensions · Completeness relative to the canonical model · The canonical accessibility relation · Model existence from the canonical model · Model existence for S4 · Model existence for S5 · Model existence for T · Truth lemma

DefinitionThe canonical accessibility relation#✓fully proved

For a set \(\Lambda\) of modal formulas and maximal \((K \oplus \Lambda)\)-consistent sets \(M\) and \(N\) (worlds of the canonical model), \(M\) is related to \(N\) iff every formula \(\varphi\) with \(\Box\varphi \in M\) belongs to \(N\).

def CanonicalWorld.rel (M N : CanonicalWorld Λ) : Prop := ∀ phi, Formula.box phi ∈ M.1 → phi ∈ N.1

Uses 3 · Used by 13

Statement usesWorlds of the canonical model · Consistency relative to a normal modal logic · Modal formulas

Used byThe canonical model as a CSLib model · The canonical model · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Completeness for CSLib's S4 · Completeness for CSLib's S5 · Completeness for CSLib's T · Existence lemma · Model existence for S4 · Model existence for S5 · Model existence for T · Truth lemma

DefinitionThe canonical model#✓fully proved

Let \(\Lambda\) be a set of extra axioms such that \(\bot\) is not a theorem of \(K \oplus \Lambda\). The canonical model of \(K \oplus \Lambda\) is the Kripke model whose worlds are the maximal consistent sets of \(K \oplus \Lambda\) (there is at least one, by Lindenbaum's lemma), in which \(M\) sees \(N\) iff \(\varphi \in N\) for every formula \(\varphi\) with \(\Box\varphi \in M\), and in which an atom \(p\) is true at \(M\) iff \(p \in M\).

def canonicalModel (h : ¬Derivable Λ .bot) : KripkeModel (CanonicalWorld Λ) Atom where
  nonempty_world :=
    let ⟨M, _, hM⟩ := exists_maximal_consistent (consistent_empty h)
    ⟨⟨M, hM⟩⟩
  rel := CanonicalWorld.rel
  valuation M p := Formula.atom p ∈ M.1

Uses 9 · Used by 9

Statement usesWorlds of the canonical model · The canonical accessibility relation · Consistency relative to a normal modal logic · Local consequence in a normal modal logic · Theorems of a normal modal logic · Modal formulas · Kripke model · Consequences of no hypotheses are the theorems · Lindenbaum's lemma for normal modal logics

Used byStrong completeness of K · Strong completeness of S4 · Strong completeness of S5 · Strong completeness of T · Validity in a class containing the canonical model gives derivability · Completeness relative to the canonical model · Model existence from the canonical model · Model existence for S4 · Truth lemma

TheoremExistence lemma#✓fully proved

Let \(\Lambda\) be a set of modal formulas, \(\mathrm{K} \oplus \Lambda\) the normal modal logic K extended by the axioms \(\Lambda\), \(M\) a canonical world, that is, a set of modal formulas maximal among the sets consistent relative to \(\mathrm{K} \oplus \Lambda\), and \(\varphi\) a modal formula. If \(\Box\varphi \notin M\), then there is a canonical world \(N\) with \(\varphi \notin N\) that is accessible from \(M\) in the canonical relation: every \(\psi\) with \(\Box\psi \in M\) lies in \(N\).

theorem CanonicalWorld.exists_rel_not_mem (M : CanonicalWorld Λ) {phi : Formula Atom}
    (h : Formula.box phi ∉ M.1) : ∃ N : CanonicalWorld Λ, M.rel N ∧ phi ∉ N.1

Uses 16 · Used by 1

Statement usesWorlds of the canonical model · The canonical accessibility relation · Consistency relative to a normal modal logic · Modal formulas

Proof usesLocal consequence in a normal modal logic · Compactness of local modal consequence · Discharging a list of hypotheses · Monotonicity of local consequence in the hypotheses · Proof by contradiction · Theorems of a normal modal logic · Boxing an implication chain · Negation of modal formulas · Maximal consistent sets of modal formulas are deductively closed · Iterated modus ponens in maximal consistent sets · Consequences of no hypotheses are the theorems · Lindenbaum's lemma for normal modal logics

Used byTruth lemma

TheoremTruth lemma#✓fully proved

A formula holds at a world of the canonical model iff it belongs to it.

theorem satisfies_canonical_iff (h : ¬Derivable Λ .bot) (M : CanonicalWorld Λ)
    (phi : Formula Atom) : (canonicalModel h).Satisfies M phi ↔ phi ∈ M.1

Uses 16 · Used by 3

Statement usesWorlds of the canonical model · Consistency relative to a normal modal logic · Theorems of a normal modal logic · Modal formulas · Satisfaction in a Kripke model · The canonical model

Proof usesExistence lemma · The canonical accessibility relation · Local consequence in a normal modal logic · Contradiction yields falsity · The deduction theorem for local modal consequence, forward direction · Negation introduction · Ex falso quodlibet · Negation of modal formulas · Kripke model · Maximal consistent sets of modal formulas are deductively closed

Used byValidity in a class containing the canonical model gives derivability · Completeness relative to the canonical model · Model existence from the canonical model

TheoremDeducibility from maximal consistent extensions#✓fully proved

Let \(\Lambda\) and \(\Gamma\) be sets of modal formulas and \(\varphi\) a formula. If \(\varphi\) belongs to every maximal \((K \oplus \Lambda)\)-consistent set that contains \(\Gamma\), then \(\Gamma\) deduces \(\varphi\) in \(K \oplus \Lambda\).

theorem Deduces.of_canonical {Γ : Set (Formula Atom)} {phi : Formula Atom}
    (h : ∀ M : CanonicalWorld Λ, Γ ⊆ M.1 → phi ∈ M.1) : Deduces Λ Γ phi

Uses 8 · Used by 2

Statement usesWorlds of the canonical model · Consistency relative to a normal modal logic · Local consequence in a normal modal logic · Modal formulas

Proof usesProof by contradiction · Negation of modal formulas · Maximal consistent sets of modal formulas are deductively closed · Lindenbaum's lemma for normal modal logics

Used byValidity in a class containing the canonical model gives derivability · Completeness relative to the canonical model

TheoremCompleteness relative to the canonical model#✓fully proved

Let \(\Lambda\) be a set of modal formulas such that \(\bot\) is not a theorem of \(K \oplus \Lambda\), let \(\Gamma\) be a set of formulas and \(\varphi\) a formula. If \(\varphi\) holds at every world of the canonical model of \(K \oplus \Lambda\) at which every formula of \(\Gamma\) holds, then \(\Gamma\) deduces \(\varphi\) in \(K \oplus \Lambda\).

theorem Deduces.of_canonicalModel (h : ¬Derivable Λ .bot) {Γ : Set (Formula Atom)}
    {phi : Formula Atom}
    (hsem : ∀ M, (∀ psi ∈ Γ, (canonicalModel h).Satisfies M psi) →
      (canonicalModel h).Satisfies M phi) : Deduces Λ Γ phi

Uses 9 · Used by 4

Statement usesWorlds of the canonical model · Local consequence in a normal modal logic · Theorems of a normal modal logic · Modal formulas · Satisfaction in a Kripke model · The canonical model

Proof usesConsistency relative to a normal modal logic · Deducibility from maximal consistent extensions · Truth lemma

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

TheoremDouble-negation introduction under a box#✓fully proved

For every set \(\Lambda\) of extra axioms and every modal formula \(\psi\), the formula \(\Box\psi \to \Box\neg\neg\psi\) is a theorem of the normal modal logic \(K \oplus \Lambda\), where \(\neg\chi\) abbreviates \(\chi \to \bot\).

theorem derivable_box_imp_box_neg_neg (psi : Formula Atom) :
    Derivable Λ (.imp (.box psi) (.box psi.neg.neg))

Uses 8 · Used by 3

Statement usesTheorems of a normal modal logic · Modal formulas · Negation of modal formulas

Proof usesLocal consequence in a normal modal logic · The deduction theorem for local modal consequence, forward direction · Double-negation introduction · The monotonicity rule for necessity · Consequences of no hypotheses are the theorems

Used byStrong completeness of S5 · Completeness for CSLib's S5 · Model existence for S5

DefinitionLocal semantic consequence over a class of Kripke models#✓fully proved

Let \(C\) be a class of Kripke models, given as a predicate on models. A set \(\Gamma\) of modal formulas locally entails a formula \(\varphi\) over \(C\) when, for every Kripke model \(M\) in \(C\) whose type of worlds lies in the universe of the atoms and every world \(w\) of \(M\), if every formula of \(\Gamma\) is satisfied at \(w\) in \(M\), then \(\varphi\) is satisfied at \(w\) in \(M\).

def LocallyEntails (C : ∀ {W : Type u}, KripkeModel W Atom → Prop) (Γ : Set (Formula Atom))
    (phi : Formula Atom) : Prop :=
  ∀ (W : Type u) (M : KripkeModel W Atom) (w : W), C M → (∀ psi ∈ Γ, M.Satisfies w psi) →
    M.Satisfies w phi

Uses 3 · Used by 8

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

Used byStrong 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

TheoremStrong completeness of K#✓fully proved

Let \(\Gamma\) be a set of formulas and \(\varphi\) a formula. Suppose that for every Kripke model whose worlds form a type in the universe of the atoms, and every world \(w\) of it at which all formulas of \(\Gamma\) hold, \(\varphi\) holds at \(w\). Then \(\varphi\) is deducible from \(\Gamma\) in K.

theorem completeness_K (hsem : LocallyEntails (fun _ ↦ True) Γ phi) : Deduces Axioms.K Γ phi

Uses 11 · Used by 2

Statement usesExtra axioms of the modal logic K · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesWorlds of the canonical model · Completeness relative to the canonical model · Theorems of a normal modal logic · Satisfaction in a Kripke model · The canonical model · Consistency of K

Used byStrong soundness and completeness of K · Soundness and completeness of K

TheoremStrong completeness of T#✓fully proved

Let \(\Gamma\) be a set of formulas and \(\varphi\) a formula. Suppose that for every Kripke model with reflexive accessibility relation whose worlds form a type in the universe of the atoms, and every world \(w\) of it at which all formulas of \(\Gamma\) hold, \(\varphi\) holds at \(w\). Then \(\varphi\) is deducible from \(\Gamma\) in T.

theorem completeness_T (hsem : LocallyEntails (fun M ↦ ∀ w, M.rel w w) Γ phi) :
    Deduces Axioms.T Γ phi

Uses 15 · Used by 2

Statement usesExtra axioms of T · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesWorlds of the canonical model · The canonical accessibility relation · Consistency relative to a normal modal logic · Completeness relative to the canonical model · Theorems of a normal modal logic · Axiom T · Satisfaction in a Kripke model · Maximal consistent sets of modal formulas are deductively closed · The canonical model · Consistency of T

Used byStrong soundness and completeness of T · Soundness and completeness of T

TheoremStrong completeness of S4#✓fully proved

Let \(\Gamma\) be a set of formulas and \(\varphi\) a formula. Suppose that for every Kripke model with reflexive and transitive accessibility relation whose worlds form a type in the universe of the atoms, and every world \(w\) of it at which all formulas of \(\Gamma\) hold, \(\varphi\) holds at \(w\). Then \(\varphi\) is deducible from \(\Gamma\) in S4.

theorem completeness_S4 (hsem : LocallyEntails (fun M ↦ (∀ w, M.rel w w) ∧
    ∀ {a b c}, M.rel a b → M.rel b c → M.rel a c) Γ phi) : Deduces Axioms.S4 Γ phi

Uses 16 · Used by 2

Statement usesExtra axioms of S4 · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesWorlds of the canonical model · The canonical accessibility relation · Consistency relative to a normal modal logic · Completeness relative to the canonical model · Theorems of a normal modal logic · Axiom 4 · Axiom T · Satisfaction in a Kripke model · Maximal consistent sets of modal formulas are deductively closed · The canonical model · Consistency of S4

Used byStrong soundness and completeness of S4 · Soundness and completeness of S4

TheoremStrong completeness of S5#✓fully proved

Let \(\Gamma\) be a set of formulas and \(\varphi\) a formula. Suppose that for every Kripke model whose accessibility relation is an equivalence relation and whose worlds form a type in the universe of the atoms, and every world \(w\) of it at which all formulas of \(\Gamma\) hold, \(\varphi\) holds at \(w\). Then \(\varphi\) is deducible from \(\Gamma\) in S5.

theorem completeness_S5 (hsem : LocallyEntails (fun M ↦ Equivalence M.rel) Γ phi) :
    Deduces Axioms.S5 Γ phi

Uses 20 · Used by 2

Statement usesExtra axioms of S5 · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesWorlds of the canonical model · Double-negation introduction under a box · The canonical accessibility relation · Consistency relative to a normal modal logic · Negation introduction · Completeness relative to the canonical model · Theorems of a normal modal logic · Axiom 5 · Axiom T · The possibility operator · Negation of modal formulas · Satisfaction in a Kripke model · Maximal consistent sets of modal formulas are deductively closed · The canonical model · Consistency of S5

Used byStrong soundness and completeness of S5 · Soundness and completeness of S5

TheoremSoundness and completeness of K#✓fully proved

A modal formula \(\varphi\) is a theorem of K if and only if \(\varphi\) is valid, that is, true at every world, in every Kripke model whose worlds live in the universe of the atoms.

theorem derivable_K_iff :
    Derivable Axioms.K phi ↔ ∀ (W : Type u) (M : KripkeModel W Atom), M.Valid phi

Uses 10 · Used by 1

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 usesLocal consequence in a normal modal logic · Soundness of K for Kripke models · Satisfaction in a Kripke model · Strong completeness of K · Consequences of no hypotheses are the theorems

Used byCompleteness of K, countermodel form

TheoremSoundness and completeness of T#✓fully proved

A modal formula \(\varphi\) is a theorem of T if and only if \(\varphi\) is valid in every Kripke model whose accessibility relation is reflexive and whose type of worlds lies in the same universe as the type of atoms.

theorem derivable_T_iff :
    Derivable Axioms.T phi ↔
      ∀ (W : Type u) (M : KripkeModel W Atom), (∀ w, M.rel w w) → M.Valid phi

Uses 10 · Used by 2

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

Proof usesLocal consequence in a normal modal logic · Soundness of T for reflexive Kripke models · Satisfaction in a Kripke model · Strong completeness of T · Consequences of no hypotheses are the theorems

Used byT-provability via finite reflexive models · Finite model property of T

TheoremSoundness and completeness of S4#✓fully proved

A modal formula \(\varphi\) is a theorem of S4 if and only if \(\varphi\) is valid in every Kripke model whose accessibility relation is reflexive and transitive and whose type of worlds lies in the same universe as the type of atoms.

theorem derivable_S4_iff :
    Derivable Axioms.S4 phi ↔
      ∀ (W : Type u) (M : KripkeModel W Atom), (∀ w, M.rel w w) →
        (∀ {a b c}, M.rel a b → M.rel b c → M.rel a c) → M.Valid phi

Uses 10 · Used by 2

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

Proof usesLocal consequence in a normal modal logic · Soundness of S4 for reflexive transitive Kripke models · Satisfaction in a Kripke model · Strong completeness of S4 · Consequences of no hypotheses are the theorems

Used byS4-provability via finite reflexive transitive models · Finite model property of S4

TheoremSoundness and completeness of S5#✓fully proved

A modal formula \(\varphi\) is a theorem of S5 if and only if \(\varphi\) is valid in every Kripke model whose accessibility relation is an equivalence relation and whose type of worlds lies in the same universe as the type of atoms.

theorem derivable_S5_iff :
    Derivable Axioms.S5 phi ↔
      ∀ (W : Type u) (M : KripkeModel W Atom), Equivalence M.rel → M.Valid phi

Uses 10 · Used by 2

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

Proof usesLocal consequence in a normal modal logic · Soundness of S5 for Kripke models with an equivalence relation · Satisfaction in a Kripke model · Strong completeness of S5 · Consequences of no hypotheses are the theorems

Used byS5-provability via finite equivalence models · Finite model property of S5

TheoremModel existence from the canonical model#✓fully proved

Let \(\Lambda\) be a set of modal formulas and \(C\) a class of Kripke models whose worlds lie in the universe of the atoms, such that \(C\) contains the canonical model of \(K \oplus \Lambda\) whenever \(\bot\) is not a theorem of \(K \oplus \Lambda\). Then every \((K \oplus \Lambda)\)-consistent set \(\Gamma\) of formulas is satisfiable in \(C\): some model in \(C\) has a world at which every formula of \(\Gamma\) holds.

This is strong completeness in satisfiability form. The converse needs every model in \(C\) to validate \(\Lambda\); for K, T, S4 and S5 it is soundness.

theorem satisfiable_of_consistent {C : ∀ {W : Type u}, KripkeModel W Atom → Prop}
    (hC : ∀ h : ¬Derivable Λ .bot, C (canonicalModel h)) (hΓ : Consistent Λ Γ) :
    ∃ (W : Type u) (M : KripkeModel W Atom) (w : W), C M ∧ ∀ psi ∈ Γ, M.Satisfies w psi

Uses 10 · Used by 4

Statement usesWorlds of the canonical model · Consistency relative to a normal modal logic · Theorems of a normal modal logic · Modal formulas · Kripke model · Satisfaction in a Kripke model · The canonical model

Proof usesLocal consequence in a normal modal logic · Lindenbaum's lemma for normal modal logics · Truth lemma

Used byModel existence for K · Model existence for S4 · Model existence for S5 · Model existence for T

TheoremModel existence for K#✓fully proved

For every K-consistent set \(\Gamma\) of modal formulas there are a Kripke model, whose worlds lie in the universe of the atoms, and a world of it at which every formula of \(\Gamma\) holds.

theorem satisfiable_K (hΓ : Consistent Axioms.K Γ) :
    ∃ (W : Type u) (M : KripkeModel W Atom) (w : W), ∀ psi ∈ Γ, M.Satisfies w psi

Uses 7

Statement usesExtra axioms of the modal logic K · Consistency relative to a normal modal logic · Modal formulas · Kripke model · Satisfaction in a Kripke model

Proof usesTheorems of a normal modal logic · Model existence from the canonical model

TheoremModel existence for T#✓fully proved

For every T-consistent set \(\Gamma\) of modal formulas there are a reflexive Kripke model, whose worlds lie in the universe of the atoms, and a world of it at which every formula of \(\Gamma\) holds.

theorem satisfiable_T (hΓ : Consistent Axioms.T Γ) :
    ∃ (W : Type u) (M : KripkeModel W Atom) (w : W), (∀ w, M.rel w w) ∧
      ∀ psi ∈ Γ, M.Satisfies w psi

Uses 12

Statement usesExtra axioms of T · Consistency relative to a normal modal logic · Modal formulas · Kripke model · Satisfaction in a Kripke model

Proof usesWorlds of the canonical model · The canonical accessibility relation · Local consequence in a normal modal logic · Theorems of a normal modal logic · Axiom T · Maximal consistent sets of modal formulas are deductively closed · Model existence from the canonical model

TheoremModel existence for S4#✓fully proved

For every S4-consistent set \(\Gamma\) of modal formulas there are a reflexive transitive Kripke model, whose worlds lie in the universe of the atoms, and a world of it at which every formula of \(\Gamma\) holds.

theorem satisfiable_S4 (hΓ : Consistent Axioms.S4 Γ) :
    ∃ (W : Type u) (M : KripkeModel W Atom) (w : W), ((∀ w, M.rel w w) ∧
      ∀ {a b c}, M.rel a b → M.rel b c → M.rel a c) ∧ ∀ psi ∈ Γ, M.Satisfies w psi

Uses 14

Statement usesExtra axioms of S4 · Consistency relative to a normal modal logic · Modal formulas · Kripke model · Satisfaction in a Kripke model

Proof usesWorlds of the canonical model · The canonical accessibility relation · Local consequence in a normal modal logic · Theorems of a normal modal logic · Axiom 4 · Axiom T · Maximal consistent sets of modal formulas are deductively closed · The canonical model · Model existence from the canonical model

TheoremModel existence for S5#✓fully proved

For every S5-consistent set \(\Gamma\) of modal formulas there are a Kripke model whose accessibility relation is an equivalence and whose worlds lie in the universe of the atoms, and a world of it at which every formula of \(\Gamma\) holds.

theorem satisfiable_S5 (hΓ : Consistent Axioms.S5 Γ) :
    ∃ (W : Type u) (M : KripkeModel W Atom) (w : W), Equivalence M.rel ∧
      ∀ psi ∈ Γ, M.Satisfies w psi

Uses 17

Statement usesExtra axioms of S5 · Consistency relative to a normal modal logic · Modal formulas · Kripke model · Satisfaction in a Kripke model

Proof usesWorlds of the canonical model · Double-negation introduction under a box · The canonical accessibility relation · Local consequence in a normal modal logic · Negation introduction · Theorems of a normal modal logic · Axiom 5 · Axiom T · The possibility operator · Negation of modal formulas · Maximal consistent sets of modal formulas are deductively closed · Model existence from the canonical model

TheoremStrong soundness and completeness of K#✓fully proved

For every set \(\Gamma\) of modal formulas and every modal formula \(\varphi\), \(\varphi\) is a local consequence of \(\Gamma\) in K if and only if \(\Gamma\) locally entails \(\varphi\) over all Kripke models: \(\varphi\) holds at every world of every Kripke model, with worlds in the universe of the atoms, at which every formula of \(\Gamma\) holds.

theorem deduces_K_iff : Deduces Axioms.K Γ phi ↔ LocallyEntails (fun _ ↦ True) Γ phi

Uses 9

Statement usesExtra axioms of the modal logic K · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesLocal soundness · Satisfaction in a Kripke model · Global validity in a Kripke model · Strong completeness of K

TheoremStrong soundness and completeness of T#✓fully proved

For every set \(\Gamma\) of modal formulas and every modal formula \(\varphi\), \(\varphi\) is a local consequence of \(\Gamma\) in T if and only if \(\Gamma\) locally entails \(\varphi\) over reflexive Kripke models: \(\varphi\) holds at every world of every Kripke model with reflexive accessibility relation, with worlds in the universe of the atoms, at which every formula of \(\Gamma\) holds.

theorem deduces_T_iff :
    Deduces Axioms.T Γ phi ↔ LocallyEntails (fun M ↦ ∀ w, M.rel w w) Γ phi

Uses 11

Statement usesExtra axioms of T · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesLocal soundness · Axiom T · Satisfaction in a Kripke model · Global validity in a Kripke model · Axiom T is valid on reflexive Kripke models · Strong completeness of T

TheoremStrong soundness and completeness of S4#✓fully proved

For every set \(\Gamma\) of modal formulas and every modal formula \(\varphi\), \(\varphi\) is a local consequence of \(\Gamma\) in S4 if and only if \(\Gamma\) locally entails \(\varphi\) over reflexive transitive Kripke models: \(\varphi\) holds at every world of every Kripke model with reflexive and transitive accessibility relation, with worlds in the universe of the atoms, at which every formula of \(\Gamma\) holds.

theorem deduces_S4_iff :
    Deduces Axioms.S4 Γ phi ↔ LocallyEntails (fun M ↦ (∀ w, M.rel w w) ∧
      ∀ {a b c}, M.rel a b → M.rel b c → M.rel a c) Γ phi

Uses 13

Statement usesExtra axioms of S4 · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesLocal soundness · Axiom 4 · Axiom T · Satisfaction in a Kripke model · Global validity in a Kripke model · Axiom 4 is valid on transitive Kripke models · Axiom T is valid on reflexive Kripke models · Strong completeness of S4

TheoremStrong soundness and completeness of S5#✓fully proved

For every set \(\Gamma\) of modal formulas and every modal formula \(\varphi\), \(\varphi\) is a local consequence of \(\Gamma\) in S5 if and only if \(\Gamma\) locally entails \(\varphi\) over Kripke models whose accessibility relation is an equivalence relation: \(\varphi\) holds at every world of every such Kripke model, with worlds in the universe of the atoms, at which every formula of \(\Gamma\) holds.

theorem deduces_S5_iff :
    Deduces Axioms.S5 Γ phi ↔ LocallyEntails (fun M ↦ Equivalence M.rel) Γ phi

Uses 13

Statement usesExtra axioms of S5 · Local consequence in a normal modal logic · Modal formulas · Kripke model · Local semantic consequence over a class of Kripke models

Proof usesLocal soundness · Axiom 5 · Axiom T · Satisfaction in a Kripke model · Global validity in a Kripke model · Axiom 5 is valid on euclidean Kripke models · Axiom T is valid on reflexive Kripke models · Strong completeness of S5

DefinitionThe canonical model as a CSLib model#✓fully proved

For a set \(\Lambda\) of extra axioms, this is the unimodal model of CSLib's modal semantics whose worlds are the maximal consistent sets of \(K \oplus \Lambda\), in which \(M\) sees \(N\) iff \(\varphi \in N\) for every formula \(\varphi\) with \(\Box\varphi \in M\), and in which an atom \(p\) is true at \(M\) iff \(p \in M\).

No consistency hypothesis on \(K \oplus \Lambda\) is needed here, since a CSLib model may have no worlds.

def canonicalCslibModel : Logic.Modal.Unimodal.Model (CanonicalWorld Λ) Atom where
  toFrame := Frame.ofRelation (τ := Logic.Modal.τUnimodal Atom) CanonicalWorld.rel
  v M p := Formula.atom p ∈ M.1

Uses 4 · Used by 5

Statement usesWorlds of the canonical model · The canonical accessibility relation · Consistency relative to a normal modal logic · Modal formulas

Used byCompleteness 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

TheoremValidity in a class containing the canonical model gives derivability#✓fully proved

Let \(\Lambda\) be a set of extra axioms, and let \(S\) be a set of CSLib unimodal models whose worlds are the maximal consistent sets of \(K \oplus \Lambda\). If \(S\) contains the canonical model of \(K \oplus \Lambda\), viewed as a CSLib model, and a CSLib proposition \(\varphi\) holds at every world of every model in \(S\), then the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of \(K \oplus \Lambda\).

theorem derivable_ofProposition_of_mem_logic
    {S : Set (Logic.Modal.Unimodal.Model (CanonicalWorld Λ) Atom)}
    (hphi : phi ∈ Logic.Modal.logic S)
    (hS : canonicalCslibModel ∈ S) : Derivable Λ (Formula.ofProposition phi)

Uses 16 · Used by 4

Statement usesWorlds of the canonical model · Theorems of a normal modal logic · Modal formulas · Translation of CSLib's modal propositions · The canonical model as a CSLib model

Proof usesConsistency relative to a normal modal logic · Local consequence in a normal modal logic · Ex falso quodlibet · Deducibility from maximal consistent extensions · Kripke model · Satisfaction in a Kripke model · Kripke model of a CSLib model · The canonical model · Consequences of no hypotheses are the theorems · Truth lemma · The translation preserves satisfaction

Used byCompleteness for CSLib's K · Completeness for CSLib's S4 · Completeness for CSLib's S5 · Completeness for CSLib's T

TheoremCompleteness for CSLib's K#✓fully proved

Let \(\varphi\) be a proposition of CSLib's unimodal language over a type of atoms \(A\). Then the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of K if and only if, for every type of worlds \(W\) in the universe of \(A\), \(\varphi\) belongs to CSLib's semantic logic K over \(W\) and \(A\), that is, \(\varphi\) holds at every world of every CSLib model with worlds \(W\).

theorem derivable_ofProposition_K_iff :
    Derivable Axioms.K (Formula.ofProposition phi) ↔
      ∀ World : Type u, phi ∈ Logic.Modal.Unimodal.K World Atom

Uses 7

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesWorlds of the canonical model · Soundness for CSLib's K · The canonical model as a CSLib model · Validity in a class containing the canonical model gives derivability

TheoremCompleteness for CSLib's T#✓fully proved

For a CSLib unimodal proposition \(\varphi\), the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of the Hilbert system T if and only if, for every type of worlds in the universe of the atoms, \(\varphi\) belongs to CSLib's modal logic T over that type, that is, \(\varphi\) holds at every world of every CSLib model on that type whose accessibility relation is reflexive.

theorem derivable_ofProposition_T_iff :
    Derivable Axioms.T (Formula.ofProposition phi) ↔
      ∀ World : Type u, phi ∈ Logic.Modal.Unimodal.T World Atom

Uses 13

Statement usesExtra axioms of T · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesWorlds of the canonical model · The canonical accessibility relation · Consistency relative to a normal modal logic · Local consequence in a normal modal logic · Soundness for CSLib's T · Modal formulas · Axiom T · Maximal consistent sets of modal formulas are deductively closed · The canonical model as a CSLib model · Validity in a class containing the canonical model gives derivability

TheoremCompleteness for CSLib's S4#✓fully proved

Let \(\varphi\) be a proposition of CSLib's unimodal language over a type of atoms \(A\). Then the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of S4 if and only if, for every type of worlds \(W\) in the universe of \(A\), \(\varphi\) belongs to CSLib's semantic logic S4 over \(W\) and \(A\), that is, \(\varphi\) holds at every world of every CSLib model with worlds \(W\) whose accessibility relation is reflexive and transitive.

theorem derivable_ofProposition_S4_iff :
    Derivable Axioms.S4 (Formula.ofProposition phi) ↔
      ∀ World : Type u, phi ∈ Logic.Modal.Unimodal.S4 World Atom

Uses 14

Statement usesExtra axioms of S4 · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesWorlds of the canonical model · The canonical accessibility relation · Consistency relative to a normal modal logic · Local consequence in a normal modal logic · Soundness for CSLib's S4 · Modal formulas · Axiom 4 · Axiom T · Maximal consistent sets of modal formulas are deductively closed · The canonical model as a CSLib model · Validity in a class containing the canonical model gives derivability

TheoremCompleteness for CSLib's S5#✓fully proved

Let \(\varphi\) be a proposition of CSLib's unimodal language over a type of atoms \(A\). Then the translation of \(\varphi\) into the \(\bot\), \(\to\), \(\Box\) basis is a theorem of S5 if and only if, for every type of worlds \(W\) in the universe of \(A\), \(\varphi\) belongs to CSLib's semantic logic S5 over \(W\) and \(A\), that is, \(\varphi\) holds at every world of every CSLib model with worlds \(W\) whose accessibility relation \(R\) is reflexive, transitive and right Euclidean (\(w R u\) and \(w R v\) imply \(u R v\)).

theorem derivable_ofProposition_S5_iff :
    Derivable Axioms.S5 (Formula.ofProposition phi) ↔
      ∀ World : Type u, phi ∈ Logic.Modal.Unimodal.S5 World Atom

Uses 18

Statement usesExtra axioms of S5 · Theorems of a normal modal logic · Translation of CSLib's modal propositions

Proof usesWorlds of the canonical model · Double-negation introduction under a box · The canonical accessibility relation · Consistency relative to a normal modal logic · Local consequence in a normal modal logic · Negation introduction · Soundness for CSLib's S5 · Modal formulas · Axiom 5 · Axiom T · The possibility operator · Negation of modal formulas · Maximal consistent sets of modal formulas are deductively closed · The canonical model as a CSLib model · Validity in a class containing the canonical model gives derivability

53 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.