@[reducible, inline]

abbrev LO.Modal.Kripke.GeachConfluentFrameClass (t : GeachConfluent.Taple) : 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) : FrameClass

Equations

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

@[simp]

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

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

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveFrameClass : FrameClass

Frame class of Hilbert.KT

Equations

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

Instances For

• LO.Modal.Hilbert.KT.Kripke.complete
• LO.Modal.Hilbert.KT.Kripke.sound

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

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialFrameClass : FrameClass

Frame class of Hilbert.KD

Equations

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

Instances For

• LO.Modal.Hilbert.KD.Kripke.sound

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

@[reducible, inline]

abbrev LO.Modal.Kripke.SymmetricFrameClass : FrameClass

Frame class of Hilbert.KB

Equations

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

Instances For

• LO.Modal.Hilbert.KB.Kripke.complete
• LO.Modal.Hilbert.KB.Kripke.sound

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

@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveFrameClass : FrameClass

Frame class of Hilbert.K4

Equations

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

Instances For

• LO.Modal.Hilbert.K4.Kripke.complete
• LO.Modal.Hilbert.K4.Kripke.sound

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

@[reducible, inline]

abbrev LO.Modal.Kripke.EuclideanFrameClass : FrameClass

Frame class of Hilbert.K5

Equations

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

Instances For

• LO.Modal.Hilbert.K5.Kripke.complete
• LO.Modal.Hilbert.K5.Kripke.sound

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

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveEuclideanFrameClass : FrameClass

Frame class of Hilbert.S5

Equations

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

Instances For

• LO.Modal.Hilbert.S5.Kripke.complete
• LO.Modal.Hilbert.S5.Kripke.sound

theorem LO.Modal.Kripke.ReflexiveEuclideanFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.KTB

Equations

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

Instances For

• LO.Modal.Hilbert.KTB.Kripke.complete
• LO.Modal.Hilbert.KTB.Kripke.sound

theorem LO.Modal.Kripke.ReflexiveSymmetricFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.S4

Equations

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

Instances For

• LO.Modal.Hilbert.S4.Kripke.complete
• LO.Modal.Hilbert.S4.Kripke.sound

theorem LO.Modal.Kripke.ReflexiveTransitiveFrameClass.is_geach : 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 : 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 : 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 : 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}

Instances For

• LO.Modal.Hilbert.KT4B.Kripke.complete
• LO.Modal.Hilbert.KT4B.Kripke.sound

theorem LO.Modal.Kripke.ReflexiveTransitiveSymmetricFrameClass.is_geach : 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 : 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}

Instances For

• LO.Modal.Hilbert.KD45.Kripke.complete
• LO.Modal.Hilbert.KD45.Kripke.sound

theorem LO.Modal.Kripke.SerialTransitiveEuclideanFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.K45

Equations

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

Instances For

• LO.Modal.Hilbert.K45.Kripke.complete
• LO.Modal.Hilbert.K45.Kripke.sound

theorem LO.Modal.Kripke.TransitiveEuclideanFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.KB4

Equations

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

Instances For

• LO.Modal.Hilbert.KB4.Kripke.complete
• LO.Modal.Hilbert.KB4.Kripke.sound

theorem LO.Modal.Kripke.SymmetricTransitiveFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.KB5

Equations

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

Instances For

• LO.Modal.Hilbert.KB5.Kripke.complete
• LO.Modal.Hilbert.KB5.Kripke.sound

theorem LO.Modal.Kripke.SymmetricEuclideanFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.KDB

Equations

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

Instances For

• LO.Modal.Hilbert.KDB.Kripke.complete
• LO.Modal.Hilbert.KDB.Kripke.sound

theorem LO.Modal.Kripke.SerialSymmetricFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.KD4

Equations

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

Instances For

• LO.Modal.Hilbert.KD4.Kripke.complete
• LO.Modal.Hilbert.KD4.Kripke.sound

theorem LO.Modal.Kripke.SerialTransitiveFrameClass.is_geach : 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 : FrameClass

Frame class of Hilbert.KD5

Equations

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

Instances For

• LO.Modal.Hilbert.KD5.Kripke.complete
• LO.Modal.Hilbert.KD5.Kripke.sound

theorem LO.Modal.Kripke.SerialEuclideanFrameClass.is_geach : 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} : (GeachConfluentFrameClass t).DefinedBy 𝗴𝗲(t)

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

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

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

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

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

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

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

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

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

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

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

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