def LO.Modal.Standard.GeachConfluent {α : Type u} (t : LO.System.Axioms.Geach.Taple) (R : α → α → Prop) : Prop

Equations

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

@[simp]

theorem LO.Modal.Standard.GeachConfluent.serial_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 0, j := 0, m := 1, n := 1 } R ↔ Serial R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.reflexive_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 0, j := 0, m := 1, n := 0 } R ↔ Reflexive R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.symmetric_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 0, j := 1, m := 0, n := 1 } R ↔ Symmetric R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.transitive_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 0, j := 2, m := 1, n := 0 } R ↔ Transitive R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.euclidean_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 1, j := 1, m := 0, n := 1 } R ↔ Euclidean R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.confluent_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 1, j := 1, m := 1, n := 1 } R ↔ Confluent R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.extensive_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 0, j := 1, m := 0, n := 0 } R ↔ Extensive R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.functional_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 1, j := 1, m := 0, n := 0 } R ↔ Functional R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.dense_def {α : Type u} {R : α → α → Prop} : LO.Modal.Standard.GeachConfluent { i := 0, j := 1, m := 2, n := 0 } R ↔ Dense R

@[simp]

theorem LO.Modal.Standard.GeachConfluent.satisfies_eq {α : Type u} {t : LO.System.Axioms.Geach.Taple} : LO.Modal.Standard.GeachConfluent t fun (x x_1 : α) => x = x_1

def LO.Modal.Standard.MultiGeachConfluent {α : Type u} (ts : List LO.System.Axioms.Geach.Taple) (R : α → α → Prop) : Prop

Equations

• LO.Modal.Standard.MultiGeachConfluent [] R = True
• LO.Modal.Standard.MultiGeachConfluent (t :: ts_2) R = (LO.Modal.Standard.GeachConfluent t R ∧ LO.Modal.Standard.MultiGeachConfluent ts_2 R)

@[simp]

theorem LO.Modal.Standard.MultiGeachConfluent.satisfies_eq {α : Type u} {ts : List LO.System.Axioms.Geach.Taple} : LO.Modal.Standard.MultiGeachConfluent ts fun (x x_1 : α) => x = x_1

theorem LO.Modal.Standard.Kripke.TerminalFrame.geach_confluent {t : LO.System.Axioms.Geach.Taple} : LO.Modal.Standard.GeachConfluent t LO.Modal.Standard.Kripke.Frame.Rel'

theorem LO.Modal.Standard.Kripke.TerminalFrame.multi_geach_confluent {ts : List LO.System.Axioms.Geach.Taple} : LO.Modal.Standard.MultiGeachConfluent ts LO.Modal.Standard.Kripke.Frame.Rel'

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.GeachConfluentFrameClass (t : LO.System.Axioms.Geach.Taple) : LO.Modal.Standard.Kripke.FrameClass

Equations

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

theorem LO.Modal.Standard.Kripke.GeachConfluentFrameClass.nonempty {t : LO.System.Axioms.Geach.Taple} : Set.Nonempty (LO.Modal.Standard.Kripke.GeachConfluentFrameClass t)

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.MultiGeachConfluentFrameClass (ts : List LO.System.Axioms.Geach.Taple) : LO.Modal.Standard.Kripke.FrameClass

Equations

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

theorem LO.Modal.Standard.Kripke.MultiGeachConfluentFrameClass.nonempty {ts : List LO.System.Axioms.Geach.Taple} : Set.Nonempty (LO.Modal.Standard.Kripke.MultiGeachConfluentFrameClass ts)

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[simp]

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

theorem LO.Modal.Standard.Kripke.axiomGeach_defines {α : Type u} [Inhabited α] {t : LO.System.Axioms.Geach.Taple} : 𝗴𝗲(t).DefinesKripkeFrameClass (LO.Modal.Standard.Kripke.GeachConfluentFrameClass t)

instance LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterNormalGeach {α : Type u} [Inhabited α] {t : LO.System.Axioms.Geach.Taple} : LO.System.Consistent 𝝂𝗴𝗲(t)

Equations

• ⋯ = ⋯

theorem LO.Modal.Standard.Kripke.axiomMultiGeach_defines {α : Type u} [Inhabited α] {ts : List LO.System.Axioms.Geach.Taple} : 𝗚𝗲(ts).DefinesKripkeFrameClass (LO.Modal.Standard.Kripke.MultiGeachConfluentFrameClass ts)

theorem LO.Modal.Standard.Kripke.S4_defines {α : Type u} [Inhabited α] : 𝐒𝟒.DefinesKripkeFrameClass LO.Modal.Standard.Kripke.PreorderFrameClass

instance LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterGeach {α : Type u} [Inhabited α] {ts : List LO.System.Axioms.Geach.Taple} : LO.System.Consistent 𝐆𝐞(ts)

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterOfIsGeach {α : Type u} [Inhabited α] {Λ : LO.Modal.Standard.DeductionParameter α} [geach : Λ.IsGeach] : LO.System.Consistent Λ

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterS4 {α : Type u} [Inhabited α] : LO.System.Consistent 𝐒𝟒

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterS5 {α : Type u} [Inhabited α] : LO.System.Consistent 𝐒𝟓

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.sound_KD {α : Type u} [Inhabited α] : LO.Sound 𝐊𝐃 LO.Modal.Standard.Kripke.SerialFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.sound_KT {α : Type u} [Inhabited α] : LO.Sound 𝐊𝐓 LO.Modal.Standard.Kripke.ReflexiveFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.sound_KTB {α : Type u} [Inhabited α] : LO.Sound 𝐊𝐓𝐁 LO.Modal.Standard.Kripke.ReflexiveSymmetricFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.sound_K4 {α : Type u} [Inhabited α] : LO.Sound 𝐊𝟒 LO.Modal.Standard.Kripke.TransitiveFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.sound_S4 {α : Type u} [Inhabited α] : LO.Sound 𝐒𝟒 LO.Modal.Standard.Kripke.PreorderFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.sound_S5 {α : Type u} [Inhabited α] : LO.Sound 𝐒𝟓 LO.Modal.Standard.Kripke.ReflexiveEuclideanFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.sound_KT4B {α : Type u} [Inhabited α] : LO.Sound 𝐊𝐓𝟒𝐁 LO.Modal.Standard.Kripke.EquivalenceFrameClass.alt

Equations

• ⋯ = ⋯

theorem LO.Modal.Standard.Kripke.geachConfluent_CanonicalFrame {α : Type u} [DecidableEq α] {Ax : LO.Modal.Standard.AxiomSet α} [LO.System.Consistent 𝝂Ax] {t : LO.System.Axioms.Geach.Taple} (h : 𝗴𝗲(t) ⊆ Ax) : LO.Modal.Standard.GeachConfluent t (LO.Modal.Standard.Kripke.CanonicalFrame 𝝂Ax).Rel

theorem LO.Modal.Standard.Kripke.multiGeachConfluent_CanonicalFrame {α : Type u} [DecidableEq α] {Ax : LO.Modal.Standard.AxiomSet α} [LO.System.Consistent 𝝂Ax] {ts : List LO.System.Axioms.Geach.Taple} (h : 𝗚𝗲(ts) ⊆ Ax) : LO.Modal.Standard.MultiGeachConfluent ts (LO.Modal.Standard.Kripke.CanonicalFrame 𝝂Ax).Rel

instance LO.Modal.Standard.Kripke.instCompleteDeductionParameterFormulaDepAltMultiGeachConfluentFrameClassTaples {α : Type u} [Inhabited α] [DecidableEq α] {Λ : LO.Modal.Standard.DeductionParameter α} [g : Λ.IsGeach] : LO.Complete Λ (LO.Modal.Standard.Kripke.MultiGeachConfluentFrameClass (LO.Modal.Standard.DeductionParameter.IsGeach.taples Λ)).alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instCompleteDeductionParameterFormulaDepKTAltReflexiveFrameClass {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐊𝐓 LO.Modal.Standard.Kripke.ReflexiveFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.KT_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐊𝐓 LO.Modal.Standard.Kripke.ReflexiveFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.KTB_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐊𝐓𝐁 LO.Modal.Standard.Kripke.ReflexiveSymmetricFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.S4_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐒𝟒 LO.Modal.Standard.Kripke.PreorderFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.S5_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐒𝟓 LO.Modal.Standard.Kripke.ReflexiveEuclideanFrameClass.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.KT4B_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐊𝐓𝟒𝐁 LO.Modal.Standard.Kripke.EquivalenceFrameClass.alt

Equations

• ⋯ = ⋯

theorem LO.Modal.Standard.KD_weakerThan_KT {α : Type u} [Inhabited α] [DecidableEq α] : 𝐊𝐃 ≤ₛ 𝐊𝐓

theorem LO.Modal.Standard.KD_strictlyWeakerThan_KT {α : Type u} [Inhabited α] [DecidableEq α] : 𝐊𝐃 <ₛ 𝐊𝐓

theorem LO.Modal.Standard.K4_weakerThan_S4 {α : Type u} [Inhabited α] [DecidableEq α] : 𝐊𝟒 ≤ₛ 𝐒𝟒

theorem LO.Modal.Standard.K4_strictlyWeakerThan_S4 {α : Type u} [Inhabited α] [DecidableEq α] : 𝐊𝟒 <ₛ 𝐒𝟒

theorem LO.Modal.Standard.S4_weakerThan_S5 {α : Type u} [Inhabited α] [DecidableEq α] : 𝐒𝟒 ≤ₛ 𝐒𝟓

theorem LO.Modal.Standard.S4_strictlyWeakerThan_S5 {α : Type u} [Inhabited α] [DecidableEq α] : 𝐒𝟒 <ₛ 𝐒𝟓

theorem LO.Modal.Standard.equiv_S5_KT4B {α : Type u} [Inhabited α] [DecidableEq α] : 𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁