structure LO.Kripke.Frame : Type (u + 1)

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

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

theorem LO.Kripke.Frame.RelItr'.forward {n : ℕ} {F : LO.Kripke.Frame} {x : F.World} {y : F.World} : x ≺^[n + 1] y ↔ ∃ (z : F.World), x ≺^[n] z ∧ z ≺ y

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

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

@[reducible, inline]

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

Equations

• ﹫ = Classical.choice ⋯

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

Equations

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

@[reducible, inline]

abbrev LO.Kripke.Frame.Dep (α : Type v) : Type (u + 1)

Equations

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

@[reducible, inline]

abbrev LO.Kripke.Frame.alt (F : LO.Kripke.Frame) (α : Type v) : LO.Kripke.Frame.Dep α

Equations

• F#α = F

def LO.Kripke.«term_#_» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_#_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_#_ 1022 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

structure LO.Kripke.FiniteFrameextends LO.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.Kripke.FiniteFrame.World_finite (self : LO.Kripke.FiniteFrame) : Finite self.World

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

Equations

• ⋯ = ⋯

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Kripke.FrameClass.Dep (α : Type v) : Type (u + 1)

Equations

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

@[reducible, inline]

abbrev LO.Kripke.FrameClass.alt (𝔽 : LO.Kripke.FrameClass) (α : Type v) : LO.Kripke.FrameClass.Dep α

Equations

• 𝔽#α = 𝔽

def LO.Kripke.«term_#__1» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_#__1» = Lean.ParserDescr.trailingNode `LO.Kripke.term_#__1 1024 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Kripke.FiniteFrameClass.Dep (α : Type v) : Type (u + 1)

Equations

• LO.Kripke.FiniteFrameClass.Dep α = LO.Kripke.FiniteFrameClass

@[reducible, inline]

abbrev LO.Kripke.FiniteFrameClass.alt (𝔽 : LO.Kripke.FiniteFrameClass) (α : Type v) : LO.Kripke.FiniteFrameClass.Dep α

Equations

• 𝔽#α = 𝔽

def LO.Kripke.«term_#__2» : Lean.TrailingParserDescr

Equations

• LO.Kripke.«term_#__2» = Lean.ParserDescr.trailingNode `LO.Kripke.term_#__2 1024 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

@[reducible, inline]

abbrev LO.Kripke.FiniteFrameClass.toFrameClass (𝔽 : LO.Kripke.FiniteFrameClass) : LO.Kripke.FrameClass

Equations

• 𝔽.toFrameClass = LO.Kripke.FiniteFrame.toFrame '' 𝔽

@[reducible, inline]

abbrev LO.Kripke.FrameClass.toFiniteFrameClass (𝔽 : LO.Kripke.FrameClass) : LO.Kripke.FiniteFrameClass

Equations

• 𝔽ꟳ = {FF : LO.Kripke.FiniteFrame | FF.toFrame ∈ 𝔽}

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

Equations

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

theorem LO.Kripke.FrameClass.iff_mem_restrictFinite {𝔽 : LO.Kripke.FrameClass} {F : LO.Kripke.Frame} (h : F ∈ 𝔽) [Finite F.World] : LO.Kripke.FiniteFrame.mk F ∈ 𝔽ꟳ

@[reducible, inline]

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

FrameClass for 𝐊

Equations

• LO.Kripke.AllFrameClass = Set.univ

@[reducible, inline]

abbrev LO.Kripke.ReflexiveFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐊𝐓

Equations

• LO.Kripke.ReflexiveFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel}

@[reducible, inline]

abbrev LO.Kripke.SerialFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐊𝐃

Equations

• LO.Kripke.SerialFrameClass = {F : LO.Kripke.Frame | Serial F.Rel}

@[reducible, inline]

abbrev LO.Kripke.TransitiveFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐊𝟒

Equations

• LO.Kripke.TransitiveFrameClass = {F : LO.Kripke.Frame | Transitive F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ReflexiveEuclideanFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐊𝐓𝟓 (𝐒𝟓)

Equations

• LO.Kripke.ReflexiveEuclideanFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Euclidean F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ReflexiveSymmetricFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐊𝐓𝐁

Equations

• LO.Kripke.ReflexiveSymmetricFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Symmetric F.Rel}

@[reducible, inline]

abbrev LO.Kripke.UniversalFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐒𝟓

Equations

• LO.Kripke.UniversalFrameClass = {F : LO.Kripke.Frame | Universal F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ConnectedFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐊.𝟑

Equations

• LO.Kripke.ConnectedFrameClass = {F : LO.Kripke.Frame | Connected F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ReflexiveTransitiveFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐈𝐧𝐭 and 𝐒𝟒

Equations

• LO.Kripke.ReflexiveTransitiveFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel}

def LO.Kripke.PreorderFrameClass : LO.Kripke.FrameClass

Alias of LO.Kripke.ReflexiveTransitiveFrameClass.

---

FrameClass for 𝐈𝐧𝐭 and 𝐒𝟒

Equations

• LO.Kripke.PreorderFrameClass = LO.Kripke.ReflexiveTransitiveFrameClass

@[reducible, inline]

abbrev LO.Kripke.ReflexiveTransitiveConfluentFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐊𝐂 and 𝐒𝟒.𝟐

Equations

• LO.Kripke.ReflexiveTransitiveConfluentFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ Confluent F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ReflexiveTransitiveConnectedFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐋𝐂 and 𝐒𝟒.𝟑

Equations

• LO.Kripke.ReflexiveTransitiveConnectedFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ Connected F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ReflexiveTransitiveSymmetricFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐂𝐥 and 𝐊𝐓𝟒𝐁 (𝐒𝟓)

Equations

• LO.Kripke.ReflexiveTransitiveSymmetricFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ Symmetric F.Rel}

def LO.Kripke.EquivalenceFrameClass : LO.Kripke.FrameClass

Alias of LO.Kripke.ReflexiveTransitiveSymmetricFrameClass.

---

FrameClass for 𝐂𝐥 and 𝐊𝐓𝟒𝐁 (𝐒𝟓)

Equations

• LO.Kripke.EquivalenceFrameClass = LO.Kripke.ReflexiveTransitiveSymmetricFrameClass

@[reducible, inline]

abbrev LO.Kripke.TransitiveConverseWellFoundedFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐆𝐋

Equations

• LO.Kripke.TransitiveConverseWellFoundedFrameClass = {F : LO.Kripke.Frame | Transitive F.Rel ∧ ConverseWellFounded F.Rel}

@[reducible, inline]

abbrev LO.Kripke.TransitiveIrreflexiveFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐆𝐋 (Finite version)

Equations

• LO.Kripke.TransitiveIrreflexiveFrameClass = {F : LO.Kripke.Frame | Transitive F.Rel ∧ Irreflexive F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐆𝐫𝐳

Equations

• LO.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ WeaklyConverseWellFounded F.Rel}

@[reducible, inline]

abbrev LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClass : LO.Kripke.FrameClass

FrameClass for 𝐆𝐫𝐳 (Finite version)

Equations

• LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClass = {F : LO.Kripke.Frame | Reflexive F.Rel ∧ Transitive F.Rel ∧ Antisymmetric F.Rel}

class LO.Kripke.FrameClass.Characteraizable (𝔽₁ : LO.Kripke.FrameClass) (𝔽₂ : outParam LO.Kripke.FrameClass) : Type

𝔽₁ is characterized by 𝔽₂

• characterize : ∀ {F : LO.Kripke.Frame}, F ∈ 𝔽₂ → F ∈ 𝔽₁
• nonempty : Set.Nonempty 𝔽₂

theorem LO.Kripke.FrameClass.Characteraizable.characterize {𝔽₁ : LO.Kripke.FrameClass} {𝔽₂ : outParam LO.Kripke.FrameClass} [self : 𝔽₁.Characteraizable 𝔽₂] {F : LO.Kripke.Frame} : F ∈ 𝔽₂ → F ∈ 𝔽₁

theorem LO.Kripke.FrameClass.Characteraizable.nonempty (𝔽₁ : LO.Kripke.FrameClass) {𝔽₂ : outParam LO.Kripke.FrameClass} [self : 𝔽₁.Characteraizable 𝔽₂] : Set.Nonempty 𝔽₂

class LO.Kripke.FrameClass.DefinedBy (𝔽₁ : LO.Kripke.FrameClass) (𝔽₂ : outParam LO.Kripke.FrameClass) : Type

𝔽₁ is defined by 𝔽₂

• define : ∀ {F : LO.Kripke.Frame}, F ∈ 𝔽₁ ↔ F ∈ 𝔽₂
• nonempty : Set.Nonempty 𝔽₂

theorem LO.Kripke.FrameClass.DefinedBy.define {𝔽₁ : LO.Kripke.FrameClass} {𝔽₂ : outParam LO.Kripke.FrameClass} [self : 𝔽₁.DefinedBy 𝔽₂] {F : LO.Kripke.Frame} : F ∈ 𝔽₁ ↔ F ∈ 𝔽₂

theorem LO.Kripke.FrameClass.DefinedBy.nonempty (𝔽₁ : LO.Kripke.FrameClass) {𝔽₂ : outParam LO.Kripke.FrameClass} [self : 𝔽₁.DefinedBy 𝔽₂] : Set.Nonempty 𝔽₂

instance LO.Kripke.instCharacteraizableOfDefinedBy {𝔽₁ : LO.Kripke.FrameClass} {𝔽₂ : LO.Kripke.FrameClass} [defines : 𝔽₁.DefinedBy 𝔽₂] : 𝔽₁.Characteraizable 𝔽₂

Equations

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

class LO.Kripke.FiniteFrameClass.Characteraizable (𝔽₁ : LO.Kripke.FiniteFrameClass) (𝔽₂ : outParam LO.Kripke.FiniteFrameClass) : Type

• characterize : ∀ {F : LO.Kripke.FiniteFrame}, F ∈ 𝔽₂ → F ∈ 𝔽₁
• nonempty : Set.Nonempty 𝔽₂

theorem LO.Kripke.FiniteFrameClass.Characteraizable.characterize {𝔽₁ : LO.Kripke.FiniteFrameClass} {𝔽₂ : outParam LO.Kripke.FiniteFrameClass} [self : 𝔽₁.Characteraizable 𝔽₂] {F : LO.Kripke.FiniteFrame} : F ∈ 𝔽₂ → F ∈ 𝔽₁

theorem LO.Kripke.FiniteFrameClass.Characteraizable.nonempty (𝔽₁ : LO.Kripke.FiniteFrameClass) {𝔽₂ : outParam LO.Kripke.FiniteFrameClass} [self : 𝔽₁.Characteraizable 𝔽₂] : Set.Nonempty 𝔽₂

class LO.Kripke.FiniteFrameClass.DefinedBy (𝔽₁ : LO.Kripke.FiniteFrameClass) (𝔽₂ : outParam LO.Kripke.FiniteFrameClass) : Type

• define : ∀ {F : LO.Kripke.FiniteFrame}, F ∈ 𝔽₁ ↔ F ∈ 𝔽₂
• nonempty : Set.Nonempty 𝔽₂

theorem LO.Kripke.FiniteFrameClass.DefinedBy.define {𝔽₁ : LO.Kripke.FiniteFrameClass} {𝔽₂ : outParam LO.Kripke.FiniteFrameClass} [self : 𝔽₁.DefinedBy 𝔽₂] {F : LO.Kripke.FiniteFrame} : F ∈ 𝔽₁ ↔ F ∈ 𝔽₂

theorem LO.Kripke.FiniteFrameClass.DefinedBy.nonempty (𝔽₁ : LO.Kripke.FiniteFrameClass) {𝔽₂ : outParam LO.Kripke.FiniteFrameClass} [self : 𝔽₁.DefinedBy 𝔽₂] : Set.Nonempty 𝔽₂

instance LO.Kripke.instCharacteraizableOfDefinedBy_1 {𝔽₁ : LO.Kripke.FiniteFrameClass} {𝔽₂ : LO.Kripke.FiniteFrameClass} [defines : 𝔽₁.DefinedBy 𝔽₂] : 𝔽₁.Characteraizable 𝔽₂

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Kripke.Valuation.atomic_hereditary {F : LO.Kripke.Frame} {α : Type u_2} (V : LO.Kripke.Valuation F α) : Prop

Equations

• V.atomic_hereditary = ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a

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

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

@[reducible, inline]

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

Equations

• M.World = M.Frame.World

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

Equations

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

@[reducible, inline]

abbrev LO.Kripke.ClassicalFrame : LO.Kripke.Frame

Equations

• LO.Kripke.ClassicalFrame = LO.Kripke.Frame.mk Unit fun (x x : Unit) => True

@[simp]

theorem LO.Kripke.ClassicalFrame.transitive : Transitive LO.Kripke.ClassicalFrame.Rel

@[simp]

theorem LO.Kripke.ClassicalFrame.reflexive : Reflexive LO.Kripke.ClassicalFrame.Rel

@[simp]

theorem LO.Kripke.ClassicalFrame.euclidean : Euclidean LO.Kripke.ClassicalFrame.Rel

@[simp]

theorem LO.Kripke.ClassicalFrame.symmetric : Symmetric LO.Kripke.ClassicalFrame.Rel

@[simp]

theorem LO.Kripke.ClassicalFrame.extensive : Extensive LO.Kripke.ClassicalFrame.Rel

@[simp]

theorem LO.Kripke.ClassicalFrame.universal : Universal LO.Kripke.ClassicalFrame.Rel

@[reducible, inline]

abbrev LO.Kripke.ClassicalValuation (α : Type u_1) : Type u_1

Equations

• LO.Kripke.ClassicalValuation α = (α → Prop)

@[reducible, inline]

abbrev LO.Kripke.ClassicalModel {α : Type u_1} (V : LO.Kripke.ClassicalValuation α) : LO.Kripke.Model α

Equations

• LO.Kripke.ClassicalModel V = { Frame := LO.Kripke.ClassicalFrame, Valuation := fun (x : LO.Kripke.ClassicalFrame.World) (a : α) => V a }

@[reducible, inline]

abbrev LO.Kripke.terminalFrame : LO.Kripke.FiniteFrame

Frame with single world and identiy relation

Equations

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

@[simp]

theorem LO.Kripke.terminalFrame.iff_rel' {x : LO.Kripke.terminalFrame.World} {y : LO.Kripke.terminalFrame.World} : x ≺ y ↔ x = y

@[simp]

theorem LO.Kripke.terminalFrame.iff_relItr' {n : ℕ} {x : LO.Kripke.terminalFrame.World} {y : LO.Kripke.terminalFrame.World} : x ≺^[n] y ↔ x = y

@[reducible, inline]

abbrev LO.Kripke.PointFrame : LO.Kripke.FiniteFrame

Equations

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

@[simp]

theorem LO.Kripke.PointFrame.iff_rel' {x : LO.Kripke.PointFrame.World} {y : LO.Kripke.PointFrame.World} : ¬x ≺ y