structure LO.Modal.Kripke.Frame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World

instance LO.Modal.Kripke.instCoeSortFrameType : CoeSort LO.Modal.Kripke.Frame Type

Equations

• LO.Modal.Kripke.instCoeSortFrameType = { coe := LO.Modal.Kripke.Frame.World }

instance LO.Modal.Kripke.instCoeFunFrameForallWorldForallProp : CoeFun LO.Modal.Kripke.Frame fun (F : LO.Modal.Kripke.Frame) => F.World → F.World → Prop

Equations

• LO.Modal.Kripke.instCoeFunFrameForallWorldForallProp = { coe := LO.Modal.Kripke.Frame.Rel }

instance LO.Modal.Kripke.instNonemptyWorld {F : LO.Modal.Kripke.Frame} : Nonempty F.World

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.Rel' {F : LO.Modal.Kripke.Frame} (x y : F.World) : Prop

Equations

• (x ≺ y) = F.Rel x y

def LO.Modal.Kripke.«term_≺_» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_≺_» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_≺_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.RelItr' {F : LO.Modal.Kripke.Frame} (n : ℕ) : F.World → F.World → Prop

Equations

• LO.Modal.Kripke.Frame.RelItr' n = F.Rel.iterate n

def LO.Modal.Kripke.«term_≺^[_]_» : Lean.TrailingParserDescr

Equations

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

structure LO.Modal.Kripke.FiniteFrameextends LO.Modal.Kripke.Frame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• world_finite : Finite self.World

instance LO.Modal.Kripke.instFiniteWorld {F : LO.Modal.Kripke.FiniteFrame} : Finite F.World

Equations

• ⋯ = ⋯

def LO.Modal.Kripke.Frame.toFinite (F : LO.Modal.Kripke.Frame) [Finite F.World] : LO.Modal.Kripke.FiniteFrame

Equations

• F.toFinite = LO.Modal.Kripke.FiniteFrame.mk F

@[reducible, inline]

abbrev LO.Modal.Kripke.reflexivePointFrame : LO.Modal.Kripke.FiniteFrame

Equations

• LO.Modal.Kripke.reflexivePointFrame = LO.Modal.Kripke.FiniteFrame.mk (LO.Modal.Kripke.Frame.mk Unit fun (x x : Unit) => True)

@[reducible, inline]

abbrev LO.Modal.Kripke.irreflexivePointFrame : LO.Modal.Kripke.FiniteFrame

Equations

• LO.Modal.Kripke.irreflexivePointFrame = LO.Modal.Kripke.FiniteFrame.mk (LO.Modal.Kripke.Frame.mk Unit fun (x x : Unit) => False)

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass : Type 1

Equations

• LO.Modal.Kripke.FrameClass = Set LO.Modal.Kripke.Frame

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrameClass : Type 1

Equations

• LO.Modal.Kripke.FiniteFrameClass = Set LO.Modal.Kripke.FiniteFrame

def LO.Modal.Kripke.FrameClass.restrictFinite (C : LO.Modal.Kripke.FrameClass) : LO.Modal.Kripke.FiniteFrameClass

Equations

• C.restrictFinite = {F : LO.Modal.Kripke.FiniteFrame | F.toFrame ∈ C}

def LO.Modal.Kripke.FiniteFrameClass.toFrameClass (C : LO.Modal.Kripke.FiniteFrameClass) : LO.Modal.Kripke.FrameClass

Equations

• C.toFrameClass = (fun (x : LO.Modal.Kripke.FiniteFrame) => x.toFrame) '' C

instance LO.Modal.Kripke.instCoeFiniteFrameClassFrameClass : Coe LO.Modal.Kripke.FiniteFrameClass LO.Modal.Kripke.FrameClass

Equations

• LO.Modal.Kripke.instCoeFiniteFrameClassFrameClass = { coe := LO.Modal.Kripke.FiniteFrameClass.toFrameClass }

@[reducible, inline]

abbrev LO.Modal.Kripke.AllFrameClass : LO.Modal.Kripke.FrameClass

Equations

• LO.Modal.Kripke.AllFrameClass = Set.univ

@[reducible, inline]

abbrev LO.Modal.Kripke.AllFiniteFrameClass : LO.Modal.Kripke.FiniteFrameClass

Equations

• LO.Modal.Kripke.AllFiniteFrameClass = Set.univ

@[reducible, inline]

abbrev LO.Modal.Kripke.Valuation (F : LO.Modal.Kripke.Frame) : Type

Equations

• LO.Modal.Kripke.Valuation F = (F.World → ℕ → Prop)

structure LO.Modal.Kripke.Modelextends LO.Modal.Kripke.Frame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• Val : LO.Modal.Kripke.Valuation self.toFrame

instance LO.Modal.Kripke.instCoeFunModelForallWorldForallNatProp : CoeFun LO.Modal.Kripke.Model fun (M : LO.Modal.Kripke.Model) => M.World → ℕ → Prop

Equations

• LO.Modal.Kripke.instCoeFunModelForallWorldForallNatProp = { coe := fun (m : LO.Modal.Kripke.Model) => m.Val }

def LO.Modal.Formula.Kripke.Satisfies (M : LO.Modal.Kripke.Model) (x : M.World) : LO.Modal.Formula ℕ → Prop

Equations

• LO.Modal.Formula.Kripke.Satisfies M x (LO.Modal.Formula.atom a) = M.Val x a
• LO.Modal.Formula.Kripke.Satisfies M x LO.Modal.Formula.falsum = False
• LO.Modal.Formula.Kripke.Satisfies M x (φ.imp ψ) = LO.Modal.Formula.Kripke.Satisfies M x φ ➝ LO.Modal.Formula.Kripke.Satisfies M x ψ
• LO.Modal.Formula.Kripke.Satisfies M x φ.box = ∀ (y : M.World), x ≺ y → LO.Modal.Formula.Kripke.Satisfies M y φ

instance LO.Modal.Formula.Kripke.Satisfies.semantics {M : LO.Modal.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 {M : LO.Modal.Kripke.Model} {x : M.World} {φ : LO.Modal.Formula ℕ} : x ⊧ φ ↔ LO.Modal.Formula.Kripke.Satisfies M x φ

@[simp]

theorem LO.Modal.Formula.Kripke.Satisfies.atom_def {M : LO.Modal.Kripke.Model} {x : M.World} {a : ℕ} : x ⊧ LO.Modal.Formula.atom a ↔ M.Val x a

theorem LO.Modal.Formula.Kripke.Satisfies.box_def {M : LO.Modal.Kripke.Model} {x : M.World} {φ : LO.Modal.Formula ℕ} : x ⊧ □φ ↔ ∀ (y : M.World), x ≺ y → y ⊧ φ

theorem LO.Modal.Formula.Kripke.Satisfies.dia_def {M : LO.Modal.Kripke.Model} {x : M.World} {φ : LO.Modal.Formula ℕ} : x ⊧ ◇φ ↔ ∃ (y : M.World), x ≺ y ∧ y ⊧ φ

theorem LO.Modal.Formula.Kripke.Satisfies.not_def {M : LO.Modal.Kripke.Model} {x : M.World} {φ : LO.Modal.Formula ℕ} : x ⊧ ∼φ ↔ ¬x ⊧ φ

theorem LO.Modal.Formula.Kripke.Satisfies.imp_def {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ} : x ⊧ φ ➝ ψ ↔ x ⊧ φ → x ⊧ ψ

theorem LO.Modal.Formula.Kripke.Satisfies.or_def {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ} : x ⊧ φ ⋎ ψ ↔ x ⊧ φ ∨ x ⊧ ψ

theorem LO.Modal.Formula.Kripke.Satisfies.and_def {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ} : x ⊧ φ ⋏ ψ ↔ x ⊧ φ ∧ x ⊧ ψ

theorem LO.Modal.Formula.Kripke.Satisfies.top_def {M : LO.Modal.Kripke.Model} {x : M.World} : x ⊧ ⊤

theorem LO.Modal.Formula.Kripke.Satisfies.bot_def {M : LO.Modal.Kripke.Model} {x : M.World} : ¬x ⊧ ⊥

instance LO.Modal.Formula.Kripke.Satisfies.instTarskiWorldNat {M : LO.Modal.Kripke.Model} : LO.Semantics.Tarski M.World

Equations

• ⋯ = ⋯

theorem LO.Modal.Formula.Kripke.Satisfies.negneg_def {M : LO.Modal.Kripke.Model} {x : M.World} {φ : LO.Modal.Formula ℕ} : x ⊧ ∼∼φ ↔ x ⊧ φ

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

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

theorem LO.Modal.Formula.Kripke.Satisfies.trans {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ χ : LO.Modal.Formula ℕ} (hpq : x ⊧ φ ➝ ψ) (hqr : x ⊧ ψ ➝ χ) : x ⊧ φ ➝ χ

theorem LO.Modal.Formula.Kripke.Satisfies.mdp {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ} (hpq : x ⊧ φ ➝ ψ) (hp : x ⊧ φ) : x ⊧ ψ

theorem LO.Modal.Formula.Kripke.Satisfies.dia_dual {M : LO.Modal.Kripke.Model} {x : M.World} {φ : LO.Modal.Formula ℕ} : x ⊧ ◇φ ↔ x ⊧ ∼□(∼φ)

theorem LO.Modal.Formula.Kripke.Satisfies.box_dual {M : LO.Modal.Kripke.Model} {x : M.World} {φ : LO.Modal.Formula ℕ} : x ⊧ □φ ↔ x ⊧ ∼◇(∼φ)

theorem LO.Modal.Formula.Kripke.Satisfies.not_imp {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ} : ¬x ⊧ φ ➝ ψ ↔ x ⊧ φ ⋏ ∼ψ

def LO.Modal.Formula.Kripke.ValidOnModel (M : LO.Modal.Kripke.Model) (φ : LO.Modal.Formula ℕ) : Prop

Equations

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

instance LO.Modal.Formula.Kripke.ValidOnModel.semantics : LO.Semantics (LO.Modal.Formula ℕ) LO.Modal.Kripke.Model

Equations

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

@[simp]

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

instance LO.Modal.Formula.Kripke.ValidOnModel.instBotModelNat : LO.Semantics.Bot LO.Modal.Kripke.Model

Equations

• LO.Modal.Formula.Kripke.ValidOnModel.instBotModelNat = ⋯

theorem LO.Modal.Formula.Kripke.ValidOnModel.mdp {M : LO.Modal.Kripke.Model} {φ ψ : LO.Modal.Formula ℕ} (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) : M ⊧ ψ

theorem LO.Modal.Formula.Kripke.ValidOnModel.nec {M : LO.Modal.Kripke.Model} {φ : LO.Modal.Formula ℕ} (h : M ⊧ φ) : M ⊧ □φ

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

theorem LO.Modal.Formula.Kripke.ValidOnModel.imply₁ {M : LO.Modal.Kripke.Model} {φ ψ : LO.Modal.Formula ℕ} : M ⊧ LO.Axioms.Imply₁ φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnModel.imply₂ {M : LO.Modal.Kripke.Model} {φ ψ χ : LO.Modal.Formula ℕ} : M ⊧ LO.Axioms.Imply₂ φ ψ χ

theorem LO.Modal.Formula.Kripke.ValidOnModel.elimContra {M : LO.Modal.Kripke.Model} {φ ψ : LO.Modal.Formula ℕ} : M ⊧ LO.Axioms.ElimContra φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnModel.axiomK {M : LO.Modal.Kripke.Model} {φ ψ : LO.Modal.Formula ℕ} : M ⊧ LO.Axioms.K φ ψ

def LO.Modal.Formula.Kripke.ValidOnFrame (F : LO.Modal.Kripke.Frame) (φ : LO.Modal.Formula ℕ) : Prop

Equations

• LO.Modal.Formula.Kripke.ValidOnFrame F φ = ∀ (V : LO.Modal.Kripke.Valuation F), { toFrame := F, Val := V } ⊧ φ

instance LO.Modal.Formula.Kripke.ValidOnFrame.semantics : LO.Semantics (LO.Modal.Formula ℕ) LO.Modal.Kripke.Frame

Equations

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

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFrame.models_iff {F : LO.Modal.Kripke.Frame} {φ : LO.Modal.Formula ℕ} : F ⊧ φ ↔ LO.Modal.Formula.Kripke.ValidOnFrame F φ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.models_set_iff {F : LO.Modal.Kripke.Frame} {Φ : Set (LO.Modal.Formula ℕ)} : F ⊧* Φ ↔ ∀ φ ∈ Φ, F ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.not_valid_iff_exists_valuation_world {F : LO.Modal.Kripke.Frame} {φ : LO.Modal.Formula ℕ} : ¬F ⊧ φ ↔ ∃ (V : LO.Modal.Kripke.Valuation F) (x : F.World), ¬LO.Modal.Formula.Kripke.Satisfies { toFrame := F, Val := V } x φ

instance LO.Modal.Formula.Kripke.ValidOnFrame.instBotFrameNat : LO.Semantics.Bot LO.Modal.Kripke.Frame

Equations

• LO.Modal.Formula.Kripke.ValidOnFrame.instBotFrameNat = ⋯

theorem LO.Modal.Formula.Kripke.ValidOnFrame.nec {F : LO.Modal.Kripke.Frame} {φ : LO.Modal.Formula ℕ} (h : F ⊧ φ) : F ⊧ □φ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.mdp {F : LO.Modal.Kripke.Frame} {φ ψ : LO.Modal.Formula ℕ} (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) : F ⊧ ψ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.verum {F : LO.Modal.Kripke.Frame} : F ⊧ ⊤

theorem LO.Modal.Formula.Kripke.ValidOnFrame.imply₁ {F : LO.Modal.Kripke.Frame} {φ ψ : LO.Modal.Formula ℕ} : F ⊧ LO.Axioms.Imply₁ φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.imply₂ {F : LO.Modal.Kripke.Frame} {φ ψ χ : LO.Modal.Formula ℕ} : F ⊧ LO.Axioms.Imply₂ φ ψ χ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.elimContra {F : LO.Modal.Kripke.Frame} {φ ψ : LO.Modal.Formula ℕ} : F ⊧ LO.Axioms.ElimContra φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.axiomK {F : LO.Modal.Kripke.Frame} {φ ψ : LO.Modal.Formula ℕ} : F ⊧ LO.Axioms.K φ ψ

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

def LO.Modal.Formula.Kripke.ValidOnFrameClass (C : LO.Modal.Kripke.FrameClass) (φ : LO.Modal.Formula ℕ) : Prop

Equations

• LO.Modal.Formula.Kripke.ValidOnFrameClass C φ = ∀ {F : LO.Modal.Kripke.Frame}, F ∈ C → F ⊧ φ

instance LO.Modal.Formula.Kripke.ValidOnFrameClass.semantics : LO.Semantics (LO.Modal.Formula ℕ) LO.Modal.Kripke.FrameClass

Equations

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

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.models_iff {C : LO.Modal.Kripke.FrameClass} {φ : LO.Modal.Formula ℕ} : C ⊧ φ ↔ LO.Modal.Formula.Kripke.ValidOnFrameClass C φ

def LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass (FC : LO.Modal.Kripke.FiniteFrameClass) (φ : LO.Modal.Formula ℕ) : Prop

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass FC φ = ∀ {F : LO.Modal.Kripke.FiniteFrame}, F ∈ FC → F.toFrame ⊧ φ

instance LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.semantics : LO.Semantics (LO.Modal.Formula ℕ) LO.Modal.Kripke.FiniteFrameClass

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.semantics = { Realize := fun (C : LO.Modal.Kripke.FiniteFrameClass) => LO.Modal.Formula.Kripke.ValidOnFrameClass C.toFrameClass }

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.models_iff {FC : LO.Modal.Kripke.FiniteFrameClass} {φ : LO.Modal.Formula ℕ} : FC ⊧ φ ↔ LO.Modal.Formula.Kripke.ValidOnFrameClass FC.toFrameClass φ

theorem LO.Modal.Formula.Kripke.notValidOnFiniteFrameClass_of_exists_finite_frame {φ : LO.Modal.Formula ℕ} {FC : LO.Modal.Kripke.FiniteFrameClass} (h : ∃ F ∈ FC, ¬F.toFrame ⊧ φ) : ¬FC ⊧ φ

def LO.Modal.Kripke.Frame.theorems (F : LO.Modal.Kripke.Frame) : LO.Modal.Theory ℕ

Equations

• F.theorems = {φ : LO.Modal.Formula ℕ | F ⊧ φ}

def LO.Modal.Kripke.FrameClass.DefinedBy (C : LO.Modal.Kripke.FrameClass) (T : LO.Modal.Theory ℕ) : Prop

Equations

• C.DefinedBy T = ∀ (F : LO.Modal.Kripke.Frame), F ∈ C ↔ F ⊧* T

def LO.Modal.Kripke.FiniteFrameClass.DefinedBy (C : LO.Modal.Kripke.FiniteFrameClass) (T : LO.Modal.Theory ℕ) : Prop

Equations

• C.DefinedBy T = ∀ (F : LO.Modal.Kripke.FiniteFrame), F ∈ C ↔ F.toFrame ⊧* T

theorem LO.Modal.Kripke.FiniteFrameClass.definedBy_of_definedBy_frameclass_aux {C : LO.Modal.Kripke.FrameClass} {Ax : LO.Modal.Theory ℕ} (h : C.DefinedBy Ax) : C.restrictFinite.DefinedBy Ax

theorem LO.Modal.Kripke.FiniteFrameClass.definedBy_of_definedBy_frameclass {C : LO.Modal.Kripke.FrameClass} {FC : LO.Modal.Kripke.FiniteFrameClass} {Ax : LO.Modal.Theory ℕ} (h : C.DefinedBy Ax) (e : FC = C.restrictFinite) : FC.DefinedBy Ax

theorem LO.Modal.Kripke.AllFrameClass.isDefinedBy : LO.Modal.Kripke.AllFrameClass.DefinedBy 𝗞

theorem LO.Modal.Kripke.AllFiniteFrameClass.isDefinedBy : LO.Modal.Kripke.AllFiniteFrameClass.DefinedBy 𝗞

theorem LO.Modal.Hilbert.Kripke.instSound_of_frameClass_definedBy_aux {φ : LO.Modal.Formula ℕ} {T : LO.Modal.Theory ℕ} {C : LO.Modal.Kripke.FrameClass} (definedBy : C.DefinedBy T) : LO.Modal.Hilbert.ExtK T ⊢! φ → C ⊧ φ

theorem LO.Modal.Hilbert.Kripke.instSound_of_frameClass_definedBy {H : LO.Modal.Hilbert ℕ} {T : LO.Modal.Theory ℕ} {C : LO.Modal.Kripke.FrameClass} (definedBy : C.DefinedBy T) (heq : H =ₛ LO.Modal.Hilbert.ExtK T) : LO.Sound H C

theorem LO.Modal.Hilbert.Kripke.instConsistent_of_nonempty_frameclass_aux {H : LO.Modal.Hilbert ℕ} {C : LO.Modal.Kripke.FrameClass} [sound : LO.Sound H C] (hNonempty : Set.Nonempty C) : H ⊬ ⊥

theorem LO.Modal.Hilbert.Kripke.instConsistent_of_nonempty_frameclass {H : LO.Modal.Hilbert ℕ} {C : LO.Modal.Kripke.FrameClass} [LO.Sound H C] (h_nonempty : Set.Nonempty C) : H.Consistent

theorem LO.Modal.Hilbert.Kripke.instSound_of_finiteFrameClass_definedBy_aux {φ : LO.Modal.Formula ℕ} {T : LO.Modal.Theory ℕ} {FC : LO.Modal.Kripke.FiniteFrameClass} (definedBy : FC.DefinedBy T) : LO.Modal.Hilbert.ExtK T ⊢! φ → FC ⊧ φ

theorem LO.Modal.Hilbert.Kripke.instSound_of_finiteFrameClass_definedBy {H : LO.Modal.Hilbert ℕ} {T : LO.Modal.Theory ℕ} {FC : LO.Modal.Kripke.FiniteFrameClass} (definedBy : FC.DefinedBy T) (heq : H =ₛ LO.Modal.Hilbert.ExtK T) : LO.Sound H FC

theorem LO.Modal.Hilbert.Kripke.instConsistent_of_nonempty_finiteFrameclass_aux {H : LO.Modal.Hilbert ℕ} {FC : LO.Modal.Kripke.FiniteFrameClass} [sound : LO.Sound H FC] (hNonempty : Set.Nonempty FC) : H ⊬ ⊥

theorem LO.Modal.Hilbert.Kripke.instConsistent_of_nonempty_finiteFrameclass {H : LO.Modal.Hilbert ℕ} {FC : LO.Modal.Kripke.FiniteFrameClass} [LO.Sound H FC] (h_nonempty : Set.Nonempty FC) : H.Consistent

theorem LO.Modal.Hilbert.Kripke.instFiniteSound_of_instSound {H : LO.Modal.Hilbert ℕ} {C : LO.Modal.Kripke.FrameClass} {FC : LO.Modal.Kripke.FiniteFrameClass} (heq : C.restrictFinite = FC) [sound : LO.Sound H C] : LO.Sound H FC

class LO.Modal.Hilbert.Kripke.FiniteFrameProperty (H : LO.Modal.Hilbert ℕ) (FC : LO.Modal.Kripke.FiniteFrameClass) : Prop

• sound : LO.Sound H FC
• complete : LO.Complete H FC

instance LO.Modal.Hilbert.K.Kripke.sound : LO.Sound (LO.Modal.Hilbert.K ℕ) LO.Modal.Kripke.AllFrameClass

Equations

• LO.Modal.Hilbert.K.Kripke.sound = ⋯

instance LO.Modal.Hilbert.K.consistent : LO.System.Consistent (LO.Modal.Hilbert.K ℕ)

Equations

• LO.Modal.Hilbert.K.consistent = ⋯

theorem LO.Modal.Hilbert.Kripke.weakerThan_of_subset_FrameClass {Ax₁ Ax₂ : LO.Modal.Theory ℕ} (C₁ C₂ : LO.Modal.Kripke.FrameClass) [sound₁ : LO.Sound (LO.Modal.Hilbert.ExtK Ax₁) C₁] [complete₂ : LO.Complete (LO.Modal.Hilbert.ExtK Ax₂) C₂] (h𝔽 : C₂ ⊆ C₁) : LO.Modal.Hilbert.ExtK Ax₁ ≤ₛ LO.Modal.Hilbert.ExtK Ax₂

theorem LO.Modal.Hilbert.Kripke.equiv_of_eq_FrameClass {Ax₁ Ax₂ : LO.Modal.Theory ℕ} (C₁ C₂ : LO.Modal.Kripke.FrameClass) [sound₁ : LO.Sound (LO.Modal.Hilbert.ExtK Ax₁) C₁] [sound₂ : LO.Sound (LO.Modal.Hilbert.ExtK Ax₂) C₂] [complete₁ : LO.Complete (LO.Modal.Hilbert.ExtK Ax₁) C₁] [complete₂ : LO.Complete (LO.Modal.Hilbert.ExtK Ax₂) C₂] (hC : C₁ = C₂) : LO.Modal.Hilbert.ExtK Ax₁ =ₛ LO.Modal.Hilbert.ExtK Ax₂