@[reducible, inline]

abbrev LO.Modal.Kripke.GeachConfluentFrameClass (t : GeachConfluent.Taple) : LO.Modal.Kripke.FrameClass

Equations

• LO.Modal.Kripke.GeachConfluentFrameClass t = {F : LO.Modal.Kripke.Frame | GeachConfluent t F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.MultiGeachConfluentFrameClass (ts : List GeachConfluent.Taple) : LO.Modal.Kripke.FrameClass

Equations

• LO.Modal.Kripke.MultiGeachConfluentFrameClass ts = {F : LO.Modal.Kripke.Frame | MultiGeachConfluent ts F.Rel}

@[simp]

theorem LO.Modal.Kripke.MultiGeachConfluentFrameClass.def_nil : LO.Modal.Kripke.MultiGeachConfluentFrameClass [] = LO.Modal.Kripke.AllFrameClass

theorem LO.Modal.Kripke.MultiGeachConfluentFrameClass.def_one (t : GeachConfluent.Taple) : LO.Modal.Kripke.MultiGeachConfluentFrameClass [t] = LO.Modal.Kripke.GeachConfluentFrameClass t

theorem LO.Modal.Kripke.MultiGeachConfluentFrameClass.def_cons {t : GeachConfluent.Taple} {ts : List GeachConfluent.Taple} (ts_nil : ts ≠ []) : LO.Modal.Kripke.MultiGeachConfluentFrameClass (t :: ts) = LO.Modal.Kripke.GeachConfluentFrameClass t ∩ LO.Modal.Kripke.MultiGeachConfluentFrameClass ts

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.IsGeach (C : LO.Modal.Kripke.FrameClass) (ts : List GeachConfluent.Taple) : Prop

Equations

• C.IsGeach ts = (C = LO.Modal.Kripke.MultiGeachConfluentFrameClass ts)

@[reducible, inline]

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

Frame class of Hilbert.KT

Equations

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

theorem LO.Modal.Kripke.ReflexiveFrameClass.is_geach : LO.Modal.Kripke.ReflexiveFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }]

@[reducible, inline]

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

Frame class of Hilbert.KD

Equations

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

theorem LO.Modal.Kripke.SerialFrameClass.is_geach : LO.Modal.Kripke.SerialFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.SymmetricFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.KB

Equations

• LO.Modal.Kripke.SymmetricFrameClass = {F : LO.Modal.Kripke.Frame | Symmetric F.Rel}

theorem LO.Modal.Kripke.SymmetricFrameClass.is_geach : LO.Modal.Kripke.SymmetricFrameClass.IsGeach [{ i := 0, j := 1, m := 0, n := 1 }]

@[reducible, inline]

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

Frame class of Hilbert.K4

Equations

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

theorem LO.Modal.Kripke.TransitiveFrameClass.is_geach : LO.Modal.Kripke.TransitiveFrameClass.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.EuclideanFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.K5

Equations

• LO.Modal.Kripke.EuclideanFrameClass = {F : LO.Modal.Kripke.Frame | Euclidean F.Rel}

theorem LO.Modal.Kripke.EuclideanFrameClass.is_geach : LO.Modal.Kripke.EuclideanFrameClass.IsGeach [{ i := 1, j := 1, m := 0, n := 1 }]

@[reducible, inline]

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

Frame class of Hilbert.S5

Equations

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

theorem LO.Modal.Kripke.ReflexiveEuclideanFrameClass.is_geach : LO.Modal.Kripke.ReflexiveEuclideanFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]

@[reducible, inline]

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

Frame class of Hilbert.KTB

Equations

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

theorem LO.Modal.Kripke.ReflexiveSymmetricFrameClass.is_geach : LO.Modal.Kripke.ReflexiveSymmetricFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]

@[reducible, inline]

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

Frame class of Hilbert.S4

Equations

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

theorem LO.Modal.Kripke.ReflexiveTransitiveFrameClass.is_geach : LO.Modal.Kripke.ReflexiveTransitiveFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }]

@[reducible, inline]

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

Frame class of Hilbert.S4Dot2

Equations

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

theorem LO.Modal.Kripke.ReflexiveTransitiveConfluentFrameClass.is_geach : LO.Modal.Kripke.ReflexiveTransitiveConfluentFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 1, n := 1 }]

@[reducible, inline]

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

Frame class of Hilbert.KT4B

Equations

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

theorem LO.Modal.Kripke.ReflexiveTransitiveSymmetricFrameClass.is_geach : LO.Modal.Kripke.ReflexiveTransitiveSymmetricFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.KD45

Equations

• LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass = {F : LO.Modal.Kripke.Frame | Serial F.Rel ∧ Transitive F.Rel ∧ Euclidean F.Rel}

theorem LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass.is_geach : LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveEuclideanFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.K45

Equations

• LO.Modal.Kripke.TransitiveEuclideanFrameClass = {F : LO.Modal.Kripke.Frame | Transitive F.Rel ∧ Euclidean F.Rel}

theorem LO.Modal.Kripke.TransitiveEuclideanFrameClass.is_geach : LO.Modal.Kripke.TransitiveEuclideanFrameClass.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.SymmetricTransitiveFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.KB4

Equations

• LO.Modal.Kripke.SymmetricTransitiveFrameClass = {F : LO.Modal.Kripke.Frame | Symmetric F.Rel ∧ Transitive F.Rel}

theorem LO.Modal.Kripke.SymmetricTransitiveFrameClass.is_geach : LO.Modal.Kripke.SymmetricTransitiveFrameClass.IsGeach [{ i := 0, j := 1, m := 0, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.SymmetricEuclideanFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.KB5

Equations

• LO.Modal.Kripke.SymmetricEuclideanFrameClass = {F : LO.Modal.Kripke.Frame | Symmetric F.Rel ∧ Euclidean F.Rel}

theorem LO.Modal.Kripke.SymmetricEuclideanFrameClass.is_geach : LO.Modal.Kripke.SymmetricEuclideanFrameClass.IsGeach [{ i := 0, j := 1, m := 0, n := 1 }, { i := 1, j := 1, m := 0, n := 1 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialSymmetricFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.KDB

Equations

• LO.Modal.Kripke.SerialSymmetricFrameClass = {F : LO.Modal.Kripke.Frame | Serial F.Rel ∧ Symmetric F.Rel}

theorem LO.Modal.Kripke.SerialSymmetricFrameClass.is_geach : LO.Modal.Kripke.SerialSymmetricFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 1, m := 0, n := 1 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialTransitiveFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.KD4

Equations

• LO.Modal.Kripke.SerialTransitiveFrameClass = {F : LO.Modal.Kripke.Frame | Serial F.Rel ∧ Transitive F.Rel}

theorem LO.Modal.Kripke.SerialTransitiveFrameClass.is_geach : LO.Modal.Kripke.SerialTransitiveFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }]

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialEuclideanFrameClass : LO.Modal.Kripke.FrameClass

Frame class of Hilbert.KD5

Equations

• LO.Modal.Kripke.SerialEuclideanFrameClass = {F : LO.Modal.Kripke.Frame | Serial F.Rel ∧ Euclidean F.Rel}

theorem LO.Modal.Kripke.SerialEuclideanFrameClass.is_geach : LO.Modal.Kripke.SerialEuclideanFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }, { i := 1, j := 1, m := 0, n := 1 }]

theorem LO.Modal.Kripke.GeachConfluentFrameClass.isDefinedBy {t : GeachConfluent.Taple} : (LO.Modal.Kripke.GeachConfluentFrameClass t).DefinedBy 𝗴𝗲(t)

theorem LO.Modal.Kripke.MultiGeachConfluentFrameClass.isDefinedBy {ts : List GeachConfluent.Taple} : (LO.Modal.Kripke.MultiGeachConfluentFrameClass ts).DefinedBy 𝗚𝗲(ts)

theorem LO.Modal.Kripke.ReflexiveFrameClass.isDefinedBy : LO.Modal.Kripke.ReflexiveFrameClass.DefinedBy 𝗧

theorem LO.Modal.Kripke.SerialFrameClass.isDefinedBy : LO.Modal.Kripke.SerialFrameClass.DefinedBy 𝗗

theorem LO.Modal.Kripke.TransitiveFrameClass.isDefinedBy : LO.Modal.Kripke.TransitiveFrameClass.DefinedBy 𝟰

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_geachConfluent_of_subset_Geach {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] {t : GeachConfluent.Taple} (h : 𝗴𝗲(t) ⊆ Ax) : GeachConfluent t (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_multiGeachConfluent_of_subset_MultiGeach {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] {ts : List GeachConfluent.Taple} (h : 𝗚𝗲(ts) ⊆ Ax) : MultiGeachConfluent ts (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_reflexive_of_subset_T {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] (h : 𝗧 ⊆ Ax) : Reflexive (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_serial_of_subset_D {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] (h : 𝗗 ⊆ Ax) : Serial (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_transitive_of_subset_Four {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] (h : 𝟰 ⊆ Ax) : Transitive (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_euclidean_of_subset_Five {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] (h : 𝟱 ⊆ Ax) : Euclidean (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_symmetric_of_subset_B {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] (h : 𝗕 ⊆ Ax) : Symmetric (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel

theorem LO.Modal.Hilbert.Kripke.canonicalFrame.is_confluent_of_subset_dot2 {Ax : LO.Modal.Theory ℕ} [(LO.Modal.Hilbert.ExtK Ax).Consistent] (h : .𝟮 ⊆ Ax) : Confluent (LO.Modal.Hilbert.Kripke.canonicalFrame (LO.Modal.Hilbert.ExtK Ax)).Rel