def LO.Modal.Formula.Kripke.Satisfies {α : Type u_1} (M : LO.Kripke.Model α) (x : M.World) : LO.Modal.Formula α → Prop

Equations

• LO.Modal.Formula.Kripke.Satisfies M x (LO.Modal.Formula.atom a) = M.Valuation x a
• LO.Modal.Formula.Kripke.Satisfies M x LO.Modal.Formula.falsum = False
• LO.Modal.Formula.Kripke.Satisfies M x (p.imp q) = LO.Modal.Formula.Kripke.Satisfies M x p ➝ LO.Modal.Formula.Kripke.Satisfies M x q
• LO.Modal.Formula.Kripke.Satisfies M x p.box = ∀ (y : M.Frame.World), x ≺ y → LO.Modal.Formula.Kripke.Satisfies M y p

instance LO.Modal.Formula.Kripke.Satisfies.semantics {α : Type u_1} {M : LO.Kripke.Model α} : LO.Semantics (LO.Modal.Formula α) M.World

Equations

• LO.Modal.Formula.Kripke.Satisfies.semantics = { Realize := fun (x : M.World) => LO.Modal.Formula.Kripke.Satisfies M x }

@[simp]

theorem LO.Modal.Formula.Kripke.Satisfies.iff_models {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} : x ⊧ p ↔ LO.Modal.Formula.Kripke.Satisfies M x p

theorem LO.Modal.Formula.Kripke.Satisfies.box_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} : x ⊧ □p ↔ ∀ (y : M.Frame.World), x ≺ y → y ⊧ p

theorem LO.Modal.Formula.Kripke.Satisfies.dia_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} : x ⊧ ◇p ↔ ∃ (y : M.Frame.World), x ≺ y ∧ y ⊧ p

theorem LO.Modal.Formula.Kripke.Satisfies.not_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} : x ⊧ ∼p ↔ ¬x ⊧ p

instance LO.Modal.Formula.Kripke.Satisfies.instNotWorld {α : Type u_1} {M : LO.Kripke.Model α} : LO.Semantics.Not M.World

Equations

• LO.Modal.Formula.Kripke.Satisfies.instNotWorld = { realize_not := ⋯ }

theorem LO.Modal.Formula.Kripke.Satisfies.imp_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : x ⊧ p ➝ q ↔ x ⊧ p → x ⊧ q

instance LO.Modal.Formula.Kripke.Satisfies.instImpWorld {α : Type u_1} {M : LO.Kripke.Model α} : LO.Semantics.Imp M.World

Equations

• LO.Modal.Formula.Kripke.Satisfies.instImpWorld = { realize_imp := ⋯ }

theorem LO.Modal.Formula.Kripke.Satisfies.or_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : x ⊧ p ⋎ q ↔ x ⊧ p ∨ x ⊧ q

instance LO.Modal.Formula.Kripke.Satisfies.instOrWorld {α : Type u_1} {M : LO.Kripke.Model α} : LO.Semantics.Or M.World

Equations

• LO.Modal.Formula.Kripke.Satisfies.instOrWorld = { realize_or := ⋯ }

theorem LO.Modal.Formula.Kripke.Satisfies.and_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : x ⊧ p ⋏ q ↔ x ⊧ p ∧ x ⊧ q

instance LO.Modal.Formula.Kripke.Satisfies.instAndWorld {α : Type u_1} {M : LO.Kripke.Model α} : LO.Semantics.And M.World

Equations

• LO.Modal.Formula.Kripke.Satisfies.instAndWorld = { realize_and := ⋯ }

instance LO.Modal.Formula.Kripke.Satisfies.instTarskiWorld {α : Type u_1} {M : LO.Kripke.Model α} : LO.Semantics.Tarski M.World

Equations

• LO.Modal.Formula.Kripke.Satisfies.instTarskiWorld = LO.Semantics.Tarski.mk

theorem LO.Modal.Formula.Kripke.Satisfies.negneg_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} : x ⊧ ∼∼p ↔ x ⊧ p

theorem LO.Modal.Formula.Kripke.Satisfies.multibox_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {n : ℕ} : x ⊧ □^[n]p ↔ ∀ {y : M.Frame.World}, x ≺^[n] y → y ⊧ p

theorem LO.Modal.Formula.Kripke.Satisfies.multidia_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {n : ℕ} : x ⊧ ◇^[n]p ↔ ∃ (y : M.Frame.World), x ≺^[n] y ∧ y ⊧ p

theorem LO.Modal.Formula.Kripke.Satisfies.trans {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (hpq : x ⊧ p ➝ q) (hqr : x ⊧ q ➝ r) : x ⊧ p ➝ r

theorem LO.Modal.Formula.Kripke.Satisfies.mdp {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : x ⊧ p ➝ q) (hp : x ⊧ p) : x ⊧ q

theorem LO.Modal.Formula.Kripke.Satisfies.dia_dual {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} : x ⊧ ◇p ↔ x ⊧ ∼□(∼p)

theorem LO.Modal.Formula.Kripke.Satisfies.box_dual {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} : x ⊧ □p ↔ x ⊧ ∼◇(∼p)

theorem LO.Modal.Formula.Kripke.Satisfies.not_imp {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : ¬x ⊧ p ➝ q ↔ x ⊧ p ⋏ ∼q

def LO.Modal.Formula.Kripke.ValidOnModel {α : Type u_1} (M : LO.Kripke.Model α) (p : LO.Modal.Formula α) : Prop

Equations

• LO.Modal.Formula.Kripke.ValidOnModel M p = ∀ (x : M.World), x ⊧ p

instance LO.Modal.Formula.Kripke.ValidOnModel.semantics {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Kripke.Model α)

Equations

• LO.Modal.Formula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.Kripke.Model α) => LO.Modal.Formula.Kripke.ValidOnModel M }

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnModel.iff_models {α : Type u_1} {f : LO.Modal.Formula α} {M : LO.Kripke.Model α} : M ⊧ f ↔ LO.Modal.Formula.Kripke.ValidOnModel M f

instance LO.Modal.Formula.Kripke.ValidOnModel.instBotModel {α : Type u_1} : LO.Semantics.Bot (LO.Kripke.Model α)

Equations

• LO.Modal.Formula.Kripke.ValidOnModel.instBotModel = { realize_bot := ⋯ }

theorem LO.Modal.Formula.Kripke.ValidOnModel.mdp {α : Type u_1} {M : LO.Kripke.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : M ⊧ p ➝ q) (hp : M ⊧ p) : M ⊧ q

theorem LO.Modal.Formula.Kripke.ValidOnModel.nec {α : Type u_1} {M : LO.Kripke.Model α} {p : LO.Modal.Formula α} (h : M ⊧ p) : M ⊧ □p

theorem LO.Modal.Formula.Kripke.ValidOnModel.verum {α : Type u_1} {M : LO.Kripke.Model α} : M ⊧ ⊤

theorem LO.Modal.Formula.Kripke.ValidOnModel.imply₁ {α : Type u_1} {M : LO.Kripke.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : M ⊧ LO.Axioms.Imply₁ p q

theorem LO.Modal.Formula.Kripke.ValidOnModel.imply₂ {α : Type u_1} {M : LO.Kripke.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} : M ⊧ LO.Axioms.Imply₂ p q r

theorem LO.Modal.Formula.Kripke.ValidOnModel.elimContra {α : Type u_1} {M : LO.Kripke.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : M ⊧ LO.Axioms.ElimContra p q

theorem LO.Modal.Formula.Kripke.ValidOnModel.axiomK {α : Type u_1} {M : LO.Kripke.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : M ⊧ LO.Axioms.K p q

def LO.Modal.Formula.Kripke.ValidOnFrame {α : Type u_1} (F : LO.Kripke.Frame) (p : LO.Modal.Formula α) : Prop

Equations

• LO.Modal.Formula.Kripke.ValidOnFrame F p = ∀ (V : LO.Kripke.Valuation F α), { Frame := F, Valuation := V } ⊧ p

instance LO.Modal.Formula.Kripke.ValidOnFrame.semantics {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Kripke.Frame.Dep α)

Equations

• LO.Modal.Formula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.Kripke.Frame.Dep α) => LO.Modal.Formula.Kripke.ValidOnFrame F }

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFrame.models_iff {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} : F ⊧ p ↔ LO.Modal.Formula.Kripke.ValidOnFrame F p

instance LO.Modal.Formula.Kripke.ValidOnFrame.instBotDep {α : Type u_1} : LO.Semantics.Bot (LO.Kripke.Frame.Dep α)

Equations

• LO.Modal.Formula.Kripke.ValidOnFrame.instBotDep = { realize_bot := ⋯ }

theorem LO.Modal.Formula.Kripke.ValidOnFrame.nec {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} (h : F ⊧ p) : F ⊧ □p

theorem LO.Modal.Formula.Kripke.ValidOnFrame.mdp {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : F ⊧ p ➝ q) (hp : F ⊧ p) : F ⊧ q

theorem LO.Modal.Formula.Kripke.ValidOnFrame.verum {α : Type u_1} {F : LO.Kripke.Frame.Dep α} : F ⊧ ⊤

theorem LO.Modal.Formula.Kripke.ValidOnFrame.imply₁ {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : F ⊧ LO.Axioms.Imply₁ p q

theorem LO.Modal.Formula.Kripke.ValidOnFrame.imply₂ {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} : F ⊧ LO.Axioms.Imply₂ p q r

theorem LO.Modal.Formula.Kripke.ValidOnFrame.elimContra {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : F ⊧ LO.Axioms.ElimContra p q

theorem LO.Modal.Formula.Kripke.ValidOnFrame.axiomK {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : F ⊧ LO.Axioms.K p q

theorem LO.Modal.Formula.Kripke.ValidOnFrame.axiomK_set {α : Type u_2} {F : LO.Kripke.Frame.Dep α} : F ⊧* 𝗞

def LO.Modal.Formula.Kripke.ValidOnFrameClass {α : Type u_1} (𝔽 : LO.Kripke.FrameClass) (p : LO.Modal.Formula α) : Prop

Equations

• LO.Modal.Formula.Kripke.ValidOnFrameClass 𝔽 p = ∀ {F : LO.Kripke.Frame}, F ∈ 𝔽 → F#α ⊧ p

instance LO.Modal.Formula.Kripke.ValidOnFrameClass.semantics {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Kripke.FrameClass.Dep α)

Equations

• LO.Modal.Formula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (𝔽 : LO.Kripke.FrameClass.Dep α) => LO.Modal.Formula.Kripke.ValidOnFrameClass 𝔽 }

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.models_iff {α : Type u_1} {𝔽 : LO.Kripke.FrameClass.Dep α} {p : LO.Modal.Formula α} : 𝔽 ⊧ p ↔ LO.Modal.Formula.Kripke.ValidOnFrameClass 𝔽 p

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.nec {α : Type u_1} {𝔽 : LO.Kripke.FrameClass.Dep α} {p : LO.Modal.Formula α} (h : 𝔽 ⊧ p) : 𝔽 ⊧ □p

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.mdp {α : Type u_1} {𝔽 : LO.Kripke.FrameClass.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : 𝔽 ⊧ p ➝ q) (hp : 𝔽 ⊧ p) : 𝔽 ⊧ q

@[reducible, inline]

abbrev LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass {α : Type u_1} (𝔽 : LO.Kripke.FiniteFrameClass) (p : LO.Modal.Formula α) : Prop

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass 𝔽 p = (𝔽.toFrameClass#α ⊧ p)

instance LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.semantics {α : Type u_1} : LO.Semantics (LO.Modal.Formula α) (LO.Kripke.FiniteFrameClass.Dep α)

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.semantics = { Realize := fun (𝔽 : LO.Kripke.FiniteFrameClass.Dep α) => LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass 𝔽 }

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.models_iff {α : Type u_1} {𝔽 : LO.Kripke.FiniteFrameClass.Dep α} {p : LO.Modal.Formula α} : 𝔽 ⊧ p ↔ LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass 𝔽 p

theorem LO.Modal.Kripke.axiomK {α : Type u_2} {𝔽 : LO.Kripke.FrameClass} : 𝔽#α ⊧* 𝗞

theorem LO.Modal.Kripke.nec {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} (h : 𝔽#α ⊧ p) : 𝔽#α ⊧ □p

theorem LO.Modal.Kripke.mdp {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : 𝔽#α ⊧ p ➝ q) (hp : 𝔽#α ⊧ p) : 𝔽#α ⊧ q

theorem LO.Modal.Kripke.iff_not_validOnFrameClass {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} : ¬𝔽#α ⊧ p ↔ ∃ F ∈ 𝔽, ∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World), ¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p

theorem LO.Modal.Kripke.iff_not_set_validOnFrameClass {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {T : Set (LO.Modal.Formula α)} : ¬𝔽#α ⊧* T ↔ ∃ p ∈ T, ∃ F ∈ 𝔽, ∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World), ¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p

theorem LO.Modal.Kripke.iff_not_validOnFrame {α : Type u_1} {F : LO.Kripke.Frame} {T : Set (LO.Modal.Formula α)} : ¬F#α ⊧* T ↔ ∃ p ∈ T, ∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World), ¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClassOfTheory {α : Type u_1} (T : LO.Modal.Theory α) : LO.Kripke.FrameClass

Equations

• 𝔽(T) = {F : LO.Kripke.Frame | F#α ⊧* T}

def LO.Modal.Kripke.«term𝔽(_)» : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrameClassOfTheory {α : Type u_1} (T : LO.Modal.Theory α) : LO.Kripke.FiniteFrameClass

Equations

• 𝔽ꟳ(T) = {FF : LO.Kripke.FiniteFrame | FF.toFrame#α ⊧* T}

def LO.Modal.Kripke.«term𝔽ꟳ(_)» : Lean.ParserDescr

Equations

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

def LO.Modal.Kripke.definability_union_frameclass_of_theory {α : Type u_1} {𝔽₁ : LO.Kripke.FrameClass} {𝔽₂ : LO.Kripke.FrameClass} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} (defi₁ : 𝔽(T₁).DefinedBy 𝔽₁) (defi₂ : 𝔽(T₂).DefinedBy 𝔽₂) (nonempty : Set.Nonempty (𝔽₁ ∩ 𝔽₂)) : 𝔽(T₁ ∪ T₂).DefinedBy (𝔽₁ ∩ 𝔽₂)

Equations

• LO.Modal.Kripke.definability_union_frameclass_of_theory defi₁ defi₂ nonempty = { define := ⋯, nonempty := nonempty }

def LO.Modal.Kripke.characterizability_union_frameclass_of_theory {α : Type u_1} {𝔽₁ : LO.Kripke.FrameClass} {𝔽₂ : LO.Kripke.FrameClass} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} (char₁ : 𝔽(T₁).Characteraizable 𝔽₁) (char₂ : 𝔽(T₂).Characteraizable 𝔽₂) (nonempty : Set.Nonempty (𝔽₁ ∩ 𝔽₂)) : 𝔽(T₁ ∪ T₂).Characteraizable (𝔽₁ ∩ 𝔽₂)

Equations

• LO.Modal.Kripke.characterizability_union_frameclass_of_theory char₁ char₂ nonempty = { characterize := ⋯, nonempty := nonempty }

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClassOfHilbert {α : Type u_1} (Λ : LO.Modal.Hilbert α) : LO.Kripke.FrameClass.Dep α

Equations

• 𝔽(Λ) = 𝔽(Λ.theorems)

def LO.Modal.Kripke.«term𝔽(_)_1» : Lean.ParserDescr

Equations

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

instance LO.Modal.Kripke.instDefinedByFrameClassOfHilbertNormalOfFrameClassOfTheory {α : Type u_1} {Ax : LO.Modal.Theory α} {𝔽 : LO.Kripke.FrameClass} [defi : 𝔽(Ax).DefinedBy 𝔽] : LO.Kripke.FrameClass.DefinedBy 𝔽(𝝂Ax) 𝔽

Equations

• LO.Modal.Kripke.instDefinedByFrameClassOfHilbertNormalOfFrameClassOfTheory = { define := ⋯, nonempty := ⋯ }

instance LO.Modal.Kripke.instCharacteraizableFrameClassOfHilbertNormalOfFrameClassOfTheory {α : Type u_1} {Ax : LO.Modal.Theory α} {𝔽 : LO.Kripke.FrameClass} [char : 𝔽(Ax).Characteraizable 𝔽] : LO.Kripke.FrameClass.Characteraizable 𝔽(𝝂Ax) 𝔽

Equations

• LO.Modal.Kripke.instCharacteraizableFrameClassOfHilbertNormalOfFrameClassOfTheory = { characterize := ⋯, nonempty := ⋯ }

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrameClassOfHilbert {α : Type u_1} (Λ : LO.Modal.Hilbert α) : LO.Kripke.FiniteFrameClass.Dep α

Equations

• 𝔽ꟳ(Λ) = 𝔽(Λ)ꟳ

def LO.Modal.Kripke.«term𝔽ꟳ(_)_1» : Lean.ParserDescr

Equations

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

instance LO.Modal.Kripke.instDefinedByFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory {α : Type u_1} {Ax : Set (LO.Modal.Formula α)} {𝔽 : LO.Kripke.FiniteFrameClass} [defi : 𝔽ꟳ(Ax).DefinedBy 𝔽] : LO.Kripke.FiniteFrameClass.DefinedBy 𝔽ꟳ(𝝂Ax) 𝔽

Equations

• LO.Modal.Kripke.instDefinedByFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory = { define := ⋯, nonempty := ⋯ }

instance LO.Modal.Kripke.instCharacteraizableFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory {α : Type u_1} {Ax : Set (LO.Modal.Formula α)} {𝔽 : LO.Kripke.FiniteFrameClass} [char : 𝔽ꟳ(Ax).Characteraizable 𝔽] : LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(𝝂Ax) 𝔽

Equations

• LO.Modal.Kripke.instCharacteraizableFiniteFrameClassOfHilbertNormalOfFiniteFrameClassOfTheory = { characterize := ⋯, nonempty := ⋯ }

theorem LO.Modal.Kripke.sound {α : Type u} {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} : Λ ⊢! p → 𝔽(Λ) ⊧ p

instance LO.Modal.Kripke.instSoundHilbertFormulaDepFrameClassOfHilbert {α : Type u} {Λ : LO.Modal.Hilbert α} : LO.Sound Λ 𝔽(Λ)

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.sound_finite {α : Type u} {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} : Λ ⊢! p → 𝔽ꟳ(Λ) ⊧ p

instance LO.Modal.Kripke.instSoundHilbertFormulaDepFiniteFrameClassOfHilbert {α : Type u} {Λ : LO.Modal.Hilbert α} : LO.Sound Λ 𝔽ꟳ(Λ)

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.unprovable_bot {α : Type u} {Λ : LO.Modal.Hilbert α} (hc : Set.Nonempty 𝔽(Λ)) : Λ ⊬ ⊥

instance LO.Modal.Kripke.instConsistentFormulaHilbertOfNonemptyFrameFrameClassOfHilbert {α : Type u} {Λ : LO.Modal.Hilbert α} (hc : Set.Nonempty 𝔽(Λ)) : LO.System.Consistent Λ

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.unprovable_bot_finite {α : Type u} {Λ : LO.Modal.Hilbert α} (hc : Set.Nonempty 𝔽ꟳ(Λ)) : Λ ⊬ ⊥

instance LO.Modal.Kripke.instConsistentFormulaHilbertOfNonemptyFiniteFrameFiniteFrameClassOfHilbert {α : Type u} {Λ : LO.Modal.Hilbert α} (hc : Set.Nonempty 𝔽ꟳ(Λ)) : LO.System.Consistent Λ

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.sound_of_characterizability {α : Type u} {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} {𝔽 : LO.Kripke.FrameClass} [char : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽] : Λ ⊢! p → 𝔽#α ⊧ p

instance LO.Modal.Kripke.instSoundHilbertFormulaDepAltOfCharacteraizableFrameClassOfHilbert {α : Type u} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FrameClass} [LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽] : LO.Sound Λ 𝔽#α

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.sound_of_finite_characterizability {α : Type u} {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} {𝔽 : LO.Kripke.FiniteFrameClass} [char : LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽] : Λ ⊢! p → 𝔽#α ⊧ p

instance LO.Modal.Kripke.instSoundHilbertFormulaDepAltOfCharacteraizableFiniteFrameClassOfHilbert {α : Type u} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FiniteFrameClass} [LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽] : LO.Sound Λ 𝔽#α

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.unprovable_bot_of_characterizability {α : Type u} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FrameClass} [char : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽] : Λ ⊬ ⊥

instance LO.Modal.Kripke.instConsistentFormulaHilbertOfCharacteraizableFrameClassOfHilbert {𝔽 : LO.Kripke.FrameClass} {α : Type u} {Λ : LO.Modal.Hilbert α} [LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽] : LO.System.Consistent Λ

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.unprovable_bot_of_finite_characterizability {α : Type u} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FiniteFrameClass} [char : LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽] : Λ ⊬ ⊥

instance LO.Modal.Kripke.instConsistentFormulaHilbertOfCharacteraizableFiniteFrameClassOfHilbert {α : Type u} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FiniteFrameClass} [LO.Kripke.FiniteFrameClass.Characteraizable 𝔽ꟳ(Λ) 𝔽] : LO.System.Consistent Λ

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.empty_axiom_definability {α : Type u_1} : 𝔽(∅).DefinedBy LO.Kripke.AllFrameClass

Equations

• LO.Modal.Kripke.empty_axiom_definability = { define := ⋯, nonempty := LO.Modal.Kripke.empty_axiom_definability.proof_2 }

instance LO.Modal.Kripke.K_definability {α : Type u_1} : LO.Kripke.FrameClass.DefinedBy 𝔽(𝐊) LO.Kripke.AllFrameClass

Equations

• LO.Modal.Kripke.K_definability = ⋯.mpr LO.Modal.Kripke.K_definability'

instance LO.Modal.Kripke.K_sound {α : Type u_1} : LO.Sound 𝐊 LO.Kripke.AllFrameClass#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.K_consistent {α : Type u_1} : LO.System.Consistent 𝐊

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.restrict_finite {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} : 𝔽#α ⊧ p → 𝔽ꟳ#α ⊧ p

instance LO.Modal.Kripke.instSoundHilbertFormulaDepAltToFiniteFrameClassOfDepAlt {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {Λ : LO.Modal.Hilbert α} [sound : LO.Sound Λ 𝔽#α] : LO.Sound Λ 𝔽ꟳ#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instSoundHilbertFormulaDepKAltToFiniteFrameClassAllFrameClass {α : Type u_1} : LO.Sound 𝐊 LO.Kripke.AllFrameClassꟳ#α

Equations

• ⋯ = ⋯

theorem LO.Modal.Kripke.exists_finite_frame {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} : ¬𝔽ꟳ#α ⊧ p ↔ ∃ F ∈ 𝔽ꟳ, ¬F.toFrame#α ⊧ p

class LO.Modal.Kripke.FiniteFrameProperty {α : Type u_1} (Λ : LO.Modal.Hilbert α) (𝔽 : LO.Kripke.FrameClass) : Type

• complete : LO.Complete Λ 𝔽ꟳ#α
• sound : LO.Sound Λ 𝔽ꟳ#α

theorem LO.Modal.Kripke.FiniteFrameProperty.complete {α : Type u_1} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FrameClass} [self : LO.Modal.Kripke.FiniteFrameProperty Λ 𝔽] : LO.Complete Λ 𝔽ꟳ#α

theorem LO.Modal.Kripke.FiniteFrameProperty.sound {α : Type u_1} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FrameClass} [self : LO.Modal.Kripke.FiniteFrameProperty Λ 𝔽] : LO.Sound Λ 𝔽ꟳ#α

theorem LO.Modal.K_strictlyWeakerThan_KD {α : Type u_1} [DecidableEq α] [Inhabited α] : 𝐊 <ₛ 𝐊𝐃

theorem LO.Modal.K_strictlyWeakerThan_KB {α : Type u_1} [DecidableEq α] [Inhabited α] : 𝐊 <ₛ 𝐊𝐁

theorem LO.Modal.K_strictlyWeakerThan_K4 {α : Type u_1} [DecidableEq α] [Inhabited α] : 𝐊 <ₛ 𝐊𝟒

theorem LO.Modal.K_strictlyWeakerThan_K5 {α : Type u_1} [DecidableEq α] [Inhabited α] : 𝐊 <ₛ 𝐊𝟓

theorem LO.Modal.weakerThan_of_subset_FrameClass {α : Type u_2} {Ax₁ : LO.Modal.Theory α} {Ax₂ : LO.Modal.Theory α} (𝔽₁ : LO.Kripke.FrameClass) (𝔽₂ : LO.Kripke.FrameClass) [sound₁ : LO.Sound (𝝂Ax₁) 𝔽₁#α] [complete₂ : LO.Complete (𝝂Ax₂) 𝔽₂#α] (h𝔽 : 𝔽₂ ⊆ 𝔽₁) : 𝝂Ax₁ ≤ₛ 𝝂Ax₂

theorem LO.Modal.equiv_of_eq_FrameClass {α : Type u_2} {Ax₁ : LO.Modal.Theory α} {Ax₂ : LO.Modal.Theory α} (𝔽₁ : LO.Kripke.FrameClass) (𝔽₂ : LO.Kripke.FrameClass) [sound₁ : LO.Sound (𝝂Ax₁) 𝔽₁#α] [sound₂ : LO.Sound (𝝂Ax₂) 𝔽₂#α] [complete₁ : LO.Complete (𝝂Ax₁) 𝔽₁#α] [complete₂ : LO.Complete (𝝂Ax₂) 𝔽₂#α] (h𝔽 : 𝔽₁ = 𝔽₂) : 𝝂Ax₁ =ₛ 𝝂Ax₂