def LO.Modal.Standard.RelItr {α : Sort u_1} (R : α → α → Prop) : ℕ → α → α → Prop

Equations

• LO.Modal.Standard.RelItr R 0 = fun (x x_1 : α) => x = x_1
• LO.Modal.Standard.RelItr R n.succ = fun (x y : α) => ∃ (z : α), R x z ∧ LO.Modal.Standard.RelItr R n z y

@[simp]

theorem LO.Modal.Standard.RelItr.iff_zero {α : Sort u_1} {R : α → α → Prop} {x : α} {y : α} : LO.Modal.Standard.RelItr R 0 x y ↔ x = y

@[simp]

theorem LO.Modal.Standard.RelItr.iff_succ {α : Sort u_1} {n : ℕ} {R : α → α → Prop} {x : α} {y : α} : LO.Modal.Standard.RelItr R (n + 1) x y ↔ ∃ (z : α), R x z ∧ LO.Modal.Standard.RelItr R n z y

@[simp]

theorem LO.Modal.Standard.RelItr.eq {α : Sort u_1} {n : ℕ} : LO.Modal.Standard.RelItr (fun (x x_1 : α) => x = x_1) n = fun (x x_1 : α) => x = x_1

theorem LO.Modal.Standard.RelItr.forward : ∀ {α : Sort u_1} {x y : α} {R : α → α → Prop} {n : ℕ}, LO.Modal.Standard.RelItr R (n + 1) x y ↔ ∃ (z : α), LO.Modal.Standard.RelItr R n x z ∧ R z y

structure LO.Modal.Standard.Kripke.Frame : Type (u_1 + 1)

• World : Type u_1
• Rel : Rel self.World self.World
• World_nonempty : Nonempty self.World

theorem LO.Modal.Standard.Kripke.Frame.World_nonempty (self : LO.Modal.Standard.Kripke.Frame) : Nonempty self.World

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

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instCoeSortFrameType : CoeSort LO.Modal.Standard.Kripke.Frame (Type u)

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• LO.Modal.Standard.Kripke.Frame.Rel' x y = F.Rel x y

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

Equations

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

@[reducible, inline]

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

Equations

• LO.Modal.Standard.Kripke.Frame.RelItr' n = LO.Modal.Standard.RelItr (fun (x x_1 : F.World) => LO.Modal.Standard.Kripke.Frame.Rel' x x_1) n

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

Equations

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

@[reducible, inline]

noncomputable abbrev LO.Modal.Standard.Kripke.Frame.default {F : LO.Modal.Standard.Kripke.Frame} : F.World

Equations

• ﹫ = Classical.choice ⋯

def LO.Modal.Standard.Kripke.«term﹫» : Lean.ParserDescr

Equations

• LO.Modal.Standard.Kripke.«term﹫» = Lean.ParserDescr.node `LO.Modal.Standard.Kripke.term﹫ 1024 (Lean.ParserDescr.symbol "﹫")

theorem LO.Modal.Standard.Kripke.Frame.RelItr'.congr {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} {n : ℕ} {m : ℕ} (h : LO.Modal.Standard.Kripke.Frame.RelItr' n x y) (he : autoParam (n = m) _auto✝) : LO.Modal.Standard.Kripke.Frame.RelItr' m x y

theorem LO.Modal.Standard.Kripke.Frame.RelItr'.forward {n : ℕ} {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} : LO.Modal.Standard.Kripke.Frame.RelItr' (n + 1) x y ↔ ∃ (z : F.World), LO.Modal.Standard.Kripke.Frame.RelItr' n x z ∧ LO.Modal.Standard.Kripke.Frame.Rel' z y

theorem LO.Modal.Standard.Kripke.Frame.RelItr'.comp {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} {n : ℕ} {m : ℕ} : (∃ (z : F.World), LO.Modal.Standard.Kripke.Frame.RelItr' n x z ∧ LO.Modal.Standard.Kripke.Frame.RelItr' m z y) ↔ LO.Modal.Standard.Kripke.Frame.RelItr' (n + m) x y

theorem LO.Modal.Standard.Kripke.Frame.RelItr'.comp' {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} {n : ℕ+} {m : ℕ+} : (∃ (z : F.World), LO.Modal.Standard.Kripke.Frame.RelItr' (↑n) x z ∧ LO.Modal.Standard.Kripke.Frame.RelItr' (↑m) z y) ↔ LO.Modal.Standard.Kripke.Frame.RelItr' (↑n + ↑m) x y

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Frame.Dep (α : Type u_1) : Type (u_2 + 1)

dependent-version frame

Equations

• LO.Modal.Standard.Kripke.Frame.Dep α = LO.Modal.Standard.Kripke.Frame

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Frame.alt (F : LO.Modal.Standard.Kripke.Frame) {α : Type u_2} : LO.Modal.Standard.Kripke.Frame.Dep α

Equations

• F.alt = F

def LO.Modal.Standard.Kripke.«term_#» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.«term_#» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.term_# 1024 1024 (Lean.ParserDescr.symbol "#")

structure LO.Modal.Standard.Kripke.FiniteFrameextends LO.Modal.Standard.Kripke.Frame : Type (u_1 + 1)

• World : Type u_1
• Rel : Rel self.World self.World
• World_nonempty : Nonempty self.World
• World_finite : Finite self.World

theorem LO.Modal.Standard.Kripke.FiniteFrame.World_finite (self : LO.Modal.Standard.Kripke.FiniteFrame) : Finite self.World

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

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instCoeFiniteFrameFrame : Coe LO.Modal.Standard.Kripke.FiniteFrame LO.Modal.Standard.Kripke.Frame

Equations

• LO.Modal.Standard.Kripke.instCoeFiniteFrameFrame = { coe := fun (F : LO.Modal.Standard.Kripke.FiniteFrame) => F.toFrame }

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Frame.RelReflTransGen {F : LO.Modal.Standard.Kripke.Frame} : Rel F.World F.World

Equations

• LO.Modal.Standard.Kripke.Frame.RelReflTransGen = Relation.ReflTransGen fun (x x_1 : F.World) => LO.Modal.Standard.Kripke.Frame.Rel' x x_1

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

Equations

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

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelReflTransGen.single {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} (hxy : LO.Modal.Standard.Kripke.Frame.Rel' x y) : LO.Modal.Standard.Kripke.Frame.RelReflTransGen x y

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelReflTransGen.reflexive {F : LO.Modal.Standard.Kripke.Frame} : Reflexive LO.Modal.Standard.Kripke.Frame.RelReflTransGen

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelReflTransGen.refl {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} : LO.Modal.Standard.Kripke.Frame.RelReflTransGen x x

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelReflTransGen.transitive {F : LO.Modal.Standard.Kripke.Frame} : Transitive LO.Modal.Standard.Kripke.Frame.RelReflTransGen

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelReflTransGen.symmetric {F : LO.Modal.Standard.Kripke.Frame} : Symmetric F.Rel → Symmetric LO.Modal.Standard.Kripke.Frame.RelReflTransGen

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Frame.TransitiveReflexiveClosure (F : LO.Modal.Standard.Kripke.Frame) : LO.Modal.Standard.Kripke.Frame

Equations

• F^* = LO.Modal.Standard.Kripke.Frame.mk F.World fun (x x_1 : F.World) => LO.Modal.Standard.Kripke.Frame.RelReflTransGen x x_1

def LO.Modal.Standard.Kripke.«term_^*» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.«term_^*» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.term_^* 1024 1024 (Lean.ParserDescr.symbol "^*")

theorem LO.Modal.Standard.Kripke.Frame.TransitiveReflexiveClosure.single {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} (hxy : LO.Modal.Standard.Kripke.Frame.Rel' x y) : F^*.Rel x y

theorem LO.Modal.Standard.Kripke.Frame.TransitiveReflexiveClosure.rel_reflexive {F : LO.Modal.Standard.Kripke.Frame} : Reflexive F^*.Rel

theorem LO.Modal.Standard.Kripke.Frame.TransitiveReflexiveClosure.rel_transitive {F : LO.Modal.Standard.Kripke.Frame} : Transitive F^*.Rel

theorem LO.Modal.Standard.Kripke.Frame.TransitiveReflexiveClosure.rel_symmetric {F : LO.Modal.Standard.Kripke.Frame} : Symmetric F.Rel → Symmetric F^*.Rel

def LO.Modal.Standard.Kripke.Frame.RelItr'.toReflTransGen {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} {n : ℕ} (h : LO.Modal.Standard.Kripke.Frame.RelItr' n x y) : LO.Modal.Standard.Kripke.Frame.RelReflTransGen x y

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Frame.RelTransGen {F : LO.Modal.Standard.Kripke.Frame} : Rel F.World F.World

Equations

• LO.Modal.Standard.Kripke.Frame.RelTransGen = Relation.TransGen fun (x x_1 : F.World) => LO.Modal.Standard.Kripke.Frame.Rel' x x_1

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

Equations

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

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelTransGen.single {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} (hxy : LO.Modal.Standard.Kripke.Frame.Rel' x y) : LO.Modal.Standard.Kripke.Frame.RelTransGen x y

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelTransGen.transitive {F : LO.Modal.Standard.Kripke.Frame} : Transitive LO.Modal.Standard.Kripke.Frame.RelTransGen

@[simp]

theorem LO.Modal.Standard.Kripke.Frame.RelTransGen.symmetric {F : LO.Modal.Standard.Kripke.Frame} (hSymm : Symmetric F.Rel) : Symmetric LO.Modal.Standard.Kripke.Frame.RelTransGen

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Frame.TransitiveClosure (F : LO.Modal.Standard.Kripke.Frame) : LO.Modal.Standard.Kripke.Frame

Equations

• F.TransitiveClosure = LO.Modal.Standard.Kripke.Frame.mk F.World fun (x x_1 : F.World) => LO.Modal.Standard.Kripke.Frame.RelTransGen x x_1

def LO.Modal.Standard.Kripke.«term_^+» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.«term_^+» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.term_^+ 1024 1024 (Lean.ParserDescr.symbol "^+")

theorem LO.Modal.Standard.Kripke.Frame.TransitiveClosure.single {F : LO.Modal.Standard.Kripke.Frame} {x : F.World} {y : F.World} (hxy : LO.Modal.Standard.Kripke.Frame.Rel' x y) : F.TransitiveClosure.Rel x y

theorem LO.Modal.Standard.Kripke.Frame.TransitiveClosure.rel_transitive {F : LO.Modal.Standard.Kripke.Frame} : Transitive F.TransitiveClosure.Rel

theorem LO.Modal.Standard.Kripke.Frame.TransitiveClosure.rel_symmetric {F : LO.Modal.Standard.Kripke.Frame} (hSymm : Symmetric F.Rel) : Symmetric F.TransitiveClosure.Rel

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FrameClass : Type (u_1 + 1)

Equations

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

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FrameClass.Dep (α : Type u_1) : Type (u_2 + 1)

dependent-version frame class

Equations

• LO.Modal.Standard.Kripke.FrameClass.Dep α = LO.Modal.Standard.Kripke.FrameClass

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FrameClass.alt (𝔽 : LO.Modal.Standard.Kripke.FrameClass) {α : Type u_2} : LO.Modal.Standard.Kripke.FrameClass.Dep α

Equations

• 𝔽.alt = 𝔽

def LO.Modal.Standard.Kripke.«term_#_1» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.«term_#_1» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.term_#_1 1024 1024 (Lean.ParserDescr.symbol "#")

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FiniteFrameClass : Type (u_1 + 1)

Equations

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

def LO.Modal.Standard.Kripke.FiniteFrameClass.toFrameClass (𝔽 : LO.Modal.Standard.Kripke.FiniteFrameClass) : LO.Modal.Standard.Kripke.FrameClass

Equations

• 𝔽.toFrameClass = {F : LO.Modal.Standard.Kripke.Frame | ∃ F' ∈ 𝔽, F'.toFrame = F}

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

Equations

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

def LO.Modal.Standard.Kripke.FrameClass.toFiniteFrameClass (𝔽 : LO.Modal.Standard.Kripke.FrameClass) : LO.Modal.Standard.Kripke.FiniteFrameClass

Equations

• 𝔽.toFiniteFrameClass = {F : LO.Modal.Standard.Kripke.FiniteFrame | F.toFrame ∈ 𝔽}

instance LO.Modal.Standard.Kripke.instCoeFrameClassFiniteFrameClass : Coe LO.Modal.Standard.Kripke.FrameClass LO.Modal.Standard.Kripke.FiniteFrameClass

Equations

• LO.Modal.Standard.Kripke.instCoeFrameClassFiniteFrameClass = { coe := LO.Modal.Standard.Kripke.FrameClass.toFiniteFrameClass }

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.FrameClass.restrictFinite (𝔽 : LO.Modal.Standard.Kripke.FrameClass) : LO.Modal.Standard.Kripke.FrameClass

Equations

• 𝔽ꟳ = 𝔽.toFiniteFrameClass.toFrameClass

def LO.Modal.Standard.Kripke.«term_ꟳ» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.«term_ꟳ» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.term_ꟳ 1024 1024 (Lean.ParserDescr.symbol "ꟳ")

theorem LO.Modal.Standard.Kripke.FrameClass.iff_mem_restrictFinite {F : LO.Modal.Standard.Kripke.Frame} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} (h : F ∈ 𝔽) (F_finite : Finite F.World) : F ∈ 𝔽ꟳ

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.terminalFrame : LO.Modal.Standard.Kripke.FiniteFrame

Frame with single world and identiy relation

Equations

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

@[simp]

theorem LO.Modal.Standard.Kripke.terminalFrame.iff_rel' {x : LO.Modal.Standard.Kripke.terminalFrame.World} {y : LO.Modal.Standard.Kripke.terminalFrame.World} : LO.Modal.Standard.Kripke.Frame.Rel' x y ↔ x = y

@[simp]

theorem LO.Modal.Standard.Kripke.terminalFrame.iff_relItr' {n : ℕ} {x : LO.Modal.Standard.Kripke.terminalFrame.World} {y : LO.Modal.Standard.Kripke.terminalFrame.World} : LO.Modal.Standard.Kripke.Frame.RelItr' n x y ↔ x = y

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.PointFrame : LO.Modal.Standard.Kripke.FiniteFrame

Equations

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

@[simp]

theorem LO.Modal.Standard.Kripke.PointFrame.iff_rel' {x : LO.Modal.Standard.Kripke.PointFrame.World} {y : LO.Modal.Standard.Kripke.PointFrame.World} : ¬LO.Modal.Standard.Kripke.Frame.Rel' x y

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Valuation (F : LO.Modal.Standard.Kripke.Frame) (α : Type u_1) : Type (max u_1 u_2)

Equations

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

structure LO.Modal.Standard.Kripke.Model (α : Type u_1) : Type (max u_1 (u_2 + 1))

• Frame : LO.Modal.Standard.Kripke.Frame
• Valuation : LO.Modal.Standard.Kripke.Valuation self.Frame α

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Model.World {α : Type u_1} (M : LO.Modal.Standard.Kripke.Model α) : Type u_2

Equations

• M.World = M.Frame.World

instance LO.Modal.Standard.Kripke.instCoeSortModelType {α : Type u_1} : CoeSort (LO.Modal.Standard.Kripke.Model α) (Type u)

Equations

• LO.Modal.Standard.Kripke.instCoeSortModelType = { coe := LO.Modal.Standard.Kripke.Model.World }

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

Equations

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

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

Equations

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

@[simp]

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

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

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

Equations

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

instance LO.Modal.Standard.Formula.Kripke.ValidOnModel.instSemanticsModel {α : Type u_2} : LO.Semantics (LO.Modal.Standard.Formula α) (LO.Modal.Standard.Kripke.Model α)

Equations

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

@[simp]

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

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

Equations

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

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

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

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

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

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

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.andElim₁ {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.AndElim₁ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.andElim₂ {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.AndElim₂ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.andInst {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.AndInst p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.orInst₁ {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.OrInst₁ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.orInst₂ {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.OrInst₂ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.orElim {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} {r : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.OrElim p q r

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.dne {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.DNE p

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.negEquiv {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.NegEquiv p

theorem LO.Modal.Standard.Formula.Kripke.ValidOnModel.diaDual {α : Type u_2} {M : LO.Modal.Standard.Kripke.Model α} {p : LO.Modal.Standard.Formula α} : M ⊧ LO.Axioms.DiaDuality p

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

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

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

Equations

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

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

Equations

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

@[simp]

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

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

Equations

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

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

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

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

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

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

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.andElim₁ {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.AndElim₁ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.andElim₂ {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.AndElim₂ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.andInst {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.AndInst p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.orInst₁ {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.OrInst₁ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.orInst₂ {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.OrInst₂ p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.orElim {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} {r : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.OrElim p q r

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.dne {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.DNE p

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

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.negEquiv {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.NegEquiv p

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrame.diaDual {α : Type u_2} {F : LO.Modal.Standard.Kripke.Frame.Dep α} {p : LO.Modal.Standard.Formula α} : F ⊧ LO.Axioms.DiaDuality p

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.verum {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} : 𝔽 ⊧ ⊤

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.imply₁ {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.Imply₁ p q

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.imply₂ {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} {r : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.Imply₂ p q r

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.andElim₁ {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.AndElim₁ p q

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.andElim₂ {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.AndElim₂ p q

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.andInst {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.AndInst p q

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.orInst₁ {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.OrInst₁ p q

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.orInst₂ {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.OrInst₂ p q

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.orElim {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} {r : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.OrElim p q r

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.dne {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.DNE p

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.elimContra {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.ElimContra p q

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.negEquiv {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.NegEquiv p

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.diaDual {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.DiaDuality p

@[simp]

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.axiomK {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : 𝔽 ⊧ LO.Axioms.K p q

theorem LO.Modal.Standard.Formula.Kripke.ValidOnFrameClass.axiomK_set {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass.Dep α} : 𝔽 ⊧* 𝗞

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

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

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

def LO.Modal.Standard.AxiomSet.DefinesKripkeFrameClass {α : Type u_2} (Ax : LO.Modal.Standard.AxiomSet α) (𝔽 : LO.Modal.Standard.Kripke.FrameClass) : Prop

Equations

• Ax.DefinesKripkeFrameClass 𝔽 = ∀ {F : LO.Modal.Standard.Kripke.Frame}, F.alt ⊧* Ax ↔ F ∈ 𝔽

theorem LO.Modal.Standard.AxiomSet.DefinesKripkeFrameClass.union {α : Type u_2} {Ax₁ : LO.Modal.Standard.AxiomSet α} {Ax₂ : LO.Modal.Standard.AxiomSet α} {𝔽₁ : LO.Modal.Standard.Kripke.FrameClass} {𝔽₂ : LO.Modal.Standard.Kripke.FrameClass} (defines₁ : Ax₁.DefinesKripkeFrameClass 𝔽₁) (defines₂ : Ax₂.DefinesKripkeFrameClass 𝔽₂) : (Ax₁ ∪ Ax₂).DefinesKripkeFrameClass (𝔽₁ ∩ 𝔽₂)

def LO.Modal.Standard.AxiomSet.FinitelyDefinesKripkeFrameClass {α : Type u_2} (Ax : LO.Modal.Standard.AxiomSet α) (𝔽 : LO.Modal.Standard.Kripke.FiniteFrameClass) : Prop

Equations

• Ax.FinitelyDefinesKripkeFrameClass 𝔽 = ∀ {F : LO.Modal.Standard.Kripke.FiniteFrame}, F.alt ⊧* Ax ↔ F ∈ 𝔽

theorem LO.Modal.Standard.AxiomSet.FinitelyDefinesKripkeFrameClass.union {α : Type u_2} {Ax₁ : LO.Modal.Standard.AxiomSet α} {Ax₂ : LO.Modal.Standard.AxiomSet α} {𝔽₁ : LO.Modal.Standard.Kripke.FiniteFrameClass} {𝔽₂ : LO.Modal.Standard.Kripke.FiniteFrameClass} (defines₁ : Ax₁.FinitelyDefinesKripkeFrameClass 𝔽₁) (defines₂ : Ax₂.FinitelyDefinesKripkeFrameClass 𝔽₂) : (Ax₁ ∪ Ax₂).FinitelyDefinesKripkeFrameClass (𝔽₁ ∩ 𝔽₂)

@[reducible, inline]

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

Equations

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

theorem LO.Modal.Standard.Kripke.AllFrameClass.nonempty : Set.Nonempty LO.Modal.Standard.Kripke.AllFrameClass

theorem LO.Modal.Standard.Kripke.axiomK_defines {α : Type u_2} : LO.Modal.Standard.AxiomSet.DefinesKripkeFrameClass 𝗞 LO.Modal.Standard.Kripke.AllFrameClass

theorem LO.Modal.Standard.Kripke.axiomK_union_definability {α : Type u_2} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} {Ax : LO.Modal.Standard.AxiomSet α} : Ax.DefinesKripkeFrameClass 𝔽 ↔ (𝗞 ∪ Ax).DefinesKripkeFrameClass 𝔽

@[reducible, inline]

abbrev LO.Modal.Standard.DeductionParameter.DefinesKripkeFrameClass {α : Type u_2} (Λ : LO.Modal.Standard.DeductionParameter α) [Λ.IsNormal] (𝔽 : LO.Modal.Standard.Kripke.FrameClass) : Prop

Equations

• Λ.DefinesKripkeFrameClass 𝔽 = Ax(Λ).DefinesKripkeFrameClass 𝔽

theorem LO.Modal.Standard.DeductionParameter.DefinesKripkeFrameClass.toAx {α : Type u_2} {Λ : LO.Modal.Standard.DeductionParameter α} [Λ.IsNormal] {𝔽 : LO.Modal.Standard.Kripke.FrameClass} (defines : Λ.DefinesKripkeFrameClass 𝔽) : Ax(Λ).DefinesKripkeFrameClass 𝔽

theorem LO.Modal.Standard.DeductionParameter.DefinesKripkeFrameClass.toAx' {α : Type u_2} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} (defines : (𝝂Ax).DefinesKripkeFrameClass 𝔽) : Ax.DefinesKripkeFrameClass 𝔽

theorem LO.Modal.Standard.DeductionParameter.DefinesKripkeFrameClass.ofAx {α : Type u_2} {Ax : LO.Modal.Standard.AxiomSet α} {𝔽 : LO.Modal.Standard.Kripke.FrameClass} (defines : Ax.DefinesKripkeFrameClass 𝔽) [(𝝂Ax).IsNormal] : (𝝂Ax).DefinesKripkeFrameClass 𝔽