structure GeachTaple : Type

• i : ℕ
• j : ℕ
• m : ℕ
• n : ℕ

def GeachConfluent {α : Type u_1} (t : GeachTaple) (R : Rel α α) : Prop

Equations

• GeachConfluent t R = ∀ {x y z : α}, R.iterate t.i x y ∧ R.iterate t.j x z → ∃ (u : α), R.iterate t.m y u ∧ R.iterate t.n z u

theorem GeachConfluent.serial_def {α : Type u_1} {R : Rel α α} : Serial R ↔ GeachConfluent { i := 0, j := 0, m := 1, n := 1 } R

theorem GeachConfluent.reflexive_def {α : Type u_1} {R : Rel α α} : Reflexive R ↔ GeachConfluent { i := 0, j := 0, m := 1, n := 0 } R

theorem GeachConfluent.symmetric_def {α : Type u_1} {R : Rel α α} : Symmetric R ↔ GeachConfluent { i := 0, j := 1, m := 0, n := 1 } R

theorem GeachConfluent.transitive_def {α : Type u_1} {R : Rel α α} : Transitive R ↔ GeachConfluent { i := 0, j := 2, m := 1, n := 0 } R

theorem GeachConfluent.euclidean_def {α : Type u_1} {R : Rel α α} : Euclidean R ↔ GeachConfluent { i := 1, j := 1, m := 0, n := 1 } R

theorem GeachConfluent.confluent_def {α : Type u_1} {R : Rel α α} : Confluent R ↔ GeachConfluent { i := 1, j := 1, m := 1, n := 1 } R

theorem GeachConfluent.extensive_def {α : Type u_1} {R : Rel α α} : Extensive R ↔ GeachConfluent { i := 0, j := 1, m := 0, n := 0 } R

theorem GeachConfluent.functional_def {α : Type u_1} {R : Rel α α} : Functional R ↔ GeachConfluent { i := 1, j := 1, m := 0, n := 0 } R

theorem GeachConfluent.dense_def {α : Type u_1} {R : Rel α α} : Dense R ↔ GeachConfluent { i := 0, j := 1, m := 2, n := 0 } R

@[simp]

theorem GeachConfluent.satisfies_eq {α : Type u_1} {t : GeachTaple} : GeachConfluent t fun (x x_1 : α) => x = x_1

def MultiGeachConfluent {α : Type u_1} (ts : List GeachTaple) (R : Rel α α) : Prop

Equations

• MultiGeachConfluent [] R = True
• MultiGeachConfluent [t] R = GeachConfluent t R
• MultiGeachConfluent (t :: ts_2) R = (GeachConfluent t R ∧ MultiGeachConfluent ts_2 R)

@[simp]

theorem MultiGeachConfluent.iff_nil : ∀ {α : Type u_1} {R : Rel α α}, MultiGeachConfluent [] R

@[simp]

theorem MultiGeachConfluent.iff_singleton {t : GeachTaple} : ∀ {α : Type u_1} {R : Rel α α}, MultiGeachConfluent [t] R ↔ GeachConfluent t R

theorem MultiGeachConfluent.iff_cons {ts : List GeachTaple} {t : GeachTaple} : ∀ {α : Type u_1} {R : Rel α α}, ts ≠ [] → (MultiGeachConfluent (t :: ts) R ↔ GeachConfluent t R ∧ MultiGeachConfluent ts R)

@[simp]

theorem MultiGeachConfluent.satisfies_eq {α : Type u_1} {ts : List GeachTaple} : MultiGeachConfluent ts fun (x x_1 : α) => x = x_1

@[reducible, inline]

abbrev LO.Axioms.Geach {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] (t : GeachTaple) (p : F) : F

Equations

• LO.Axioms.Geach t p = ◇^[t.i](□^[t.m]p) ➝ □^[t.j](◇^[t.n]p)

@[reducible, inline]

abbrev LO.Axioms.Geach.set {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] (t : GeachTaple) : Set F

Equations

• 𝗴𝗲(t) = {x : F | ∃ (p : F), LO.Axioms.Geach t p = x}

def LO.Axioms.«term𝗴𝗲(_)» : Lean.ParserDescr

Equations

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

theorem LO.Axioms.Geach.T_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 0, j := 0, m := 1, n := 0 }) = 𝗧

theorem LO.Axioms.Geach.B_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 0, j := 1, m := 0, n := 1 }) = 𝗕

theorem LO.Axioms.Geach.D_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 0, j := 0, m := 1, n := 1 }) = 𝗗

theorem LO.Axioms.Geach.Four_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 0, j := 2, m := 1, n := 0 }) = 𝟰

theorem LO.Axioms.Geach.Five_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 1, j := 1, m := 0, n := 1 }) = 𝟱

theorem LO.Axioms.Geach.Dot2_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 1, j := 1, m := 1, n := 1 }) = .𝟮

theorem LO.Axioms.Geach.C4_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 0, j := 1, m := 2, n := 0 }) = 𝗖𝟰

theorem LO.Axioms.Geach.CD_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 1, j := 1, m := 0, n := 0 }) = 𝗖𝗗

theorem LO.Axioms.Geach.Tc_def {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗴𝗲({ i := 0, j := 1, m := 0, n := 0 }) = 𝗧𝗰

class LO.Axioms.IsGeach {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] (Ax : Set F) : Type

• taple : GeachTaple
• char : Ax = 𝗴𝗲(LO.Axioms.IsGeach.taple Ax)

Instances

• LO.Axioms.instIsGeachSet
• LO.Axioms.instIsGeachSet_1
• LO.Axioms.instIsGeachSet_2
• LO.Axioms.instIsGeachSet_3
• LO.Axioms.instIsGeachSet_4
• LO.Axioms.instIsGeachSet_5
• LO.Axioms.instIsGeachSet_6
• LO.Axioms.instIsGeachSet_7
• LO.Axioms.instIsGeachSet_8

theorem LO.Axioms.IsGeach.char {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] {Ax : Set F} [self : LO.Axioms.IsGeach Ax] : Ax = 𝗴𝗲(LO.Axioms.IsGeach.taple Ax)

instance LO.Axioms.instIsGeachSet {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝗧

Equations

• LO.Axioms.instIsGeachSet = { taple := { i := 0, j := 0, m := 1, n := 0 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_1 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝗕

Equations

• LO.Axioms.instIsGeachSet_1 = { taple := { i := 0, j := 1, m := 0, n := 1 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_2 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝗗

Equations

• LO.Axioms.instIsGeachSet_2 = { taple := { i := 0, j := 0, m := 1, n := 1 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_3 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝟰

Equations

• LO.Axioms.instIsGeachSet_3 = { taple := { i := 0, j := 2, m := 1, n := 0 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_4 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝟱

Equations

• LO.Axioms.instIsGeachSet_4 = { taple := { i := 1, j := 1, m := 0, n := 1 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_5 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach .𝟮

Equations

• LO.Axioms.instIsGeachSet_5 = { taple := { i := 1, j := 1, m := 1, n := 1 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_6 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝗖𝟰

Equations

• LO.Axioms.instIsGeachSet_6 = { taple := { i := 0, j := 1, m := 2, n := 0 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_7 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝗖𝗗

Equations

• LO.Axioms.instIsGeachSet_7 = { taple := { i := 1, j := 1, m := 0, n := 0 }, char := ⋯ }

instance LO.Axioms.instIsGeachSet_8 {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : LO.Axioms.IsGeach 𝗧𝗰

Equations

• LO.Axioms.instIsGeachSet_8 = { taple := { i := 0, j := 1, m := 0, n := 0 }, char := ⋯ }

def LO.Axioms.MultiGeach {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : List GeachTaple → Set F

Equations

• 𝗚𝗲([]) = ∅
• 𝗚𝗲(t :: ts) = 𝗴𝗲(t) ∪ 𝗚𝗲(ts)

def LO.Axioms.«term𝗚𝗲(_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.Axioms.MultiGeach.def_nil {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] : 𝗚𝗲([]) = ∅

@[simp]

theorem LO.Axioms.MultiGeach.iff_cons {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] {x : GeachTaple} {l : List GeachTaple} : 𝗚𝗲(x :: l) = 𝗴𝗲(x) ∪ 𝗚𝗲(l)

theorem LO.Axioms.MultiGeach.mem {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] {x : GeachTaple} {l : List GeachTaple} (h : x ∈ l) : 𝗴𝗲(x) ⊆ 𝗚𝗲(l)

@[reducible, inline]

abbrev LO.Modal.Geach {α : Type u_1} (l : List GeachTaple) : LO.Modal.Hilbert α

Equations

• 𝐆𝐞(l) = 𝝂𝗚𝗲(l)

Instances For

• LO.Modal.Kripke.instConsistentFormulaHilbertGeach
• LO.Modal.Kripke.sound_Geach

def LO.Modal.«term𝐆𝐞(_)» : Lean.ParserDescr

Equations

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

class LO.Modal.Hilbert.IsGeach {α : Type u_1} (L : LO.Modal.Hilbert α) (ts : List GeachTaple) : Type

• char : L = 𝐆𝐞(ts)

Instances

• LO.Modal.IsGeach.instIsGeachK4ConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachKDConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachKNilGeachTaple
• LO.Modal.IsGeach.instIsGeachKT4BConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachKTBConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachKTConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachS4ConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachS4Dot2ConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachS5ConsGeachTapleMkOfNatNatNil
• LO.Modal.IsGeach.instIsGeachTrivConsGeachTapleMkOfNatNatNil

@[simp]

theorem LO.Modal.Hilbert.IsGeach.char {α : Type u_1} {L : LO.Modal.Hilbert α} {ts : List GeachTaple} [self : L.IsGeach ts] : L = 𝐆𝐞(ts)

theorem LO.Modal.IsGeach.ax {α : Type u_1} {ts : List GeachTaple} {Λ : LO.Modal.Hilbert α} [geach : Λ.IsGeach ts] : Ax(Λ) = 𝗞 ∪ 𝗚𝗲(ts)

instance LO.Modal.IsGeach.instIsGeachKNilGeachTaple {α : Type u_1} : 𝐊.IsGeach []

Equations

• LO.Modal.IsGeach.instIsGeachKNilGeachTaple = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachKDConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐊𝐃.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }]

Equations

• LO.Modal.IsGeach.instIsGeachKDConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachKTConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐊𝐓.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }]

Equations

• LO.Modal.IsGeach.instIsGeachKTConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachKTBConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐊𝐓𝐁.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]

Equations

• LO.Modal.IsGeach.instIsGeachKTBConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachK4ConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐊𝟒.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }]

Equations

• LO.Modal.IsGeach.instIsGeachK4ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachS4ConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐒𝟒.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }]

Equations

• LO.Modal.IsGeach.instIsGeachS4ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachS4Dot2ConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐒𝟒.𝟐.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 }]

Equations

• LO.Modal.IsGeach.instIsGeachS4Dot2ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachS5ConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐒𝟓.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]

Equations

• LO.Modal.IsGeach.instIsGeachS5ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachKT4BConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐊𝐓𝟒𝐁.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 }]

Equations

• LO.Modal.IsGeach.instIsGeachKT4BConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.IsGeach.instIsGeachTrivConsGeachTapleMkOfNatNatNil {α : Type u_1} : 𝐓𝐫𝐢𝐯.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 0 }]

Equations

• LO.Modal.IsGeach.instIsGeachTrivConsGeachTapleMkOfNatNatNil = { char := ⋯ }