structure LO.Modal.Kripke.Frame : Type 1

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

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

Equations

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

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

Equations

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

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

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.Rel' {F : 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 : 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 : _root_.Rel self.World self.World
• world_nonempty : Nonempty self.World
• world_finite : Finite self.World

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

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.reflexivePointFrame : 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 : 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 : FrameClass) : FiniteFrameClass

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.AllFrameClass : FrameClass

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.AllFiniteFrameClass : FiniteFrameClass

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.Valuation (F : 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 : _root_.Rel self.World self.World
• world_nonempty : Nonempty self.World
• Val : Valuation self.toFrame

instance LO.Modal.Kripke.instCoeFunModelForallWorldForallNatProp : CoeFun Model fun (M : 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 : Kripke.Model) (x : M.World) : 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 : Kripke.Model} : Semantics (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 : Kripke.Model} {x : M.World} {φ : Formula ℕ} : x ⊧ φ ↔ Satisfies M x φ

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

instance LO.Modal.Formula.Kripke.ValidOnModel.semantics : Semantics (Formula ℕ) 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 : Formula ℕ} {M : Kripke.Model} : M ⊧ f ↔ ValidOnModel M f

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

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

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

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

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

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

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

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

def LO.Modal.Formula.Kripke.ValidOnFrame (F : Kripke.Frame) (φ : 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 : Semantics (Formula ℕ) 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 : Kripke.Frame} {φ : Formula ℕ} : F ⊧ φ ↔ ValidOnFrame F φ

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

instance LO.Modal.Formula.Kripke.ValidOnFrameClass.semantics : Semantics (Formula ℕ) 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 : Kripke.FrameClass} {φ : Formula ℕ} : C ⊧ φ ↔ ValidOnFrameClass C φ

def LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass (FC : Kripke.FiniteFrameClass) (φ : 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 : Semantics (Formula ℕ) 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 : Kripke.FiniteFrameClass} {φ : Formula ℕ} : FC ⊧ φ ↔ ValidOnFrameClass FC.toFrameClass φ

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

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

Equations

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

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

Equations

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

def LO.Modal.Kripke.FiniteFrameClass.DefinedBy (C : FiniteFrameClass) (T : 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 : FrameClass} {Ax : Theory ℕ} (h : C.DefinedBy Ax) : C.restrictFinite.DefinedBy Ax

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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