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.System.Axioms.Geach {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] (l : GeachTaple) (p : F) : F

Equations

• LO.System.Axioms.Geach l p = ◇^[l.i](□^[l.m]p) ⟶ □^[l.j](◇^[l.n]p)

@[reducible, inline]

abbrev LO.Modal.Standard.AxiomSet.Geach {α : Type u_1} (l : GeachTaple) : LO.Modal.Standard.AxiomSet α

Equations

• 𝗴𝗲(l) = {x : LO.Modal.Standard.Formula α | ∃ (p : LO.Modal.Standard.Formula α), LO.System.Axioms.Geach l p = x}

def LO.Modal.Standard.AxiomSet.«term𝗴𝗲(_)» : Lean.ParserDescr

Equations

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

theorem LO.Modal.Standard.AxiomSet.Geach.T_def {α : Type u_1} : 𝗴𝗲({ i := 0, j := 0, m := 1, n := 0 }) = 𝗧

theorem LO.Modal.Standard.AxiomSet.Geach.B_def {α : Type u_1} : 𝗴𝗲({ i := 0, j := 1, m := 0, n := 1 }) = 𝗕

theorem LO.Modal.Standard.AxiomSet.Geach.D_def {α : Type u_1} : 𝗴𝗲({ i := 0, j := 0, m := 1, n := 1 }) = 𝗗

theorem LO.Modal.Standard.AxiomSet.Geach.Four_def {α : Type u_1} : 𝗴𝗲({ i := 0, j := 2, m := 1, n := 0 }) = 𝟰

theorem LO.Modal.Standard.AxiomSet.Geach.Five_def {α : Type u_1} : 𝗴𝗲({ i := 1, j := 1, m := 0, n := 1 }) = 𝟱

theorem LO.Modal.Standard.AxiomSet.Geach.Dot2_def {α : Type u_1} : 𝗴𝗲({ i := 1, j := 1, m := 1, n := 1 }) = .𝟮

theorem LO.Modal.Standard.AxiomSet.Geach.C4_def {α : Type u_1} : 𝗴𝗲({ i := 0, j := 1, m := 2, n := 0 }) = 𝗖𝟰

theorem LO.Modal.Standard.AxiomSet.Geach.CD_def {α : Type u_1} : 𝗴𝗲({ i := 1, j := 1, m := 0, n := 0 }) = 𝗖𝗗

theorem LO.Modal.Standard.AxiomSet.Geach.Tc_def {α : Type u_1} : 𝗴𝗲({ i := 0, j := 1, m := 0, n := 0 }) = 𝗧𝗰

class LO.Modal.Standard.AxiomSet.IsGeach {α : Type u_1} (Ax : LO.Modal.Standard.AxiomSet α) : Type

• taple : GeachTaple
• char : Ax = 𝗴𝗲(LO.Modal.Standard.AxiomSet.IsGeach.taple Ax)

theorem LO.Modal.Standard.AxiomSet.IsGeach.char {α : Type u_1} {Ax : LO.Modal.Standard.AxiomSet α} [self : Ax.IsGeach] : Ax = 𝗴𝗲(LO.Modal.Standard.AxiomSet.IsGeach.taple Ax)

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝗧

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula = { taple := { i := 0, j := 0, m := 1, n := 0 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_1 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝗕

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_1 = { taple := { i := 0, j := 1, m := 0, n := 1 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_2 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝗗

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_2 = { taple := { i := 0, j := 0, m := 1, n := 1 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_3 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝟰

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_3 = { taple := { i := 0, j := 2, m := 1, n := 0 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_4 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝟱

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_4 = { taple := { i := 1, j := 1, m := 0, n := 1 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_5 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach .𝟮

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_5 = { taple := { i := 1, j := 1, m := 1, n := 1 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_6 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝗖𝟰

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_6 = { taple := { i := 0, j := 1, m := 2, n := 0 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_7 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝗖𝗗

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_7 = { taple := { i := 1, j := 1, m := 0, n := 0 }, char := ⋯ }

instance LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_8 {α : Type u_1} : LO.Modal.Standard.AxiomSet.IsGeach 𝗧𝗰

Equations

• LO.Modal.Standard.AxiomSet.instIsGeachSetFormula_8 = { taple := { i := 0, j := 1, m := 0, n := 0 }, char := ⋯ }

def LO.Modal.Standard.AxiomSet.MultiGeach {α : Type u_1} : List GeachTaple → LO.Modal.Standard.AxiomSet α

Equations

• 𝗚𝗲([]) = ∅
• 𝗚𝗲(x_1 :: xs) = 𝗴𝗲(x_1) ∪ 𝗚𝗲(xs)

def LO.Modal.Standard.AxiomSet.«term𝗚𝗲(_)» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.Modal.Standard.AxiomSet.MultiGeach.def_nil {α : Type u_1} : 𝗚𝗲([]) = ∅

@[simp]

theorem LO.Modal.Standard.AxiomSet.MultiGeach.iff_cons {α : Type u_1} {x : GeachTaple} {l : List GeachTaple} : 𝗚𝗲(x :: l) = 𝗴𝗲(x) ∪ 𝗚𝗲(l)

theorem LO.Modal.Standard.AxiomSet.MultiGeach.mem {α : Type u_1} {x : GeachTaple} {l : List GeachTaple} (h : x ∈ l) : 𝗴𝗲(x) ⊆ 𝗚𝗲(l)

@[reducible, inline]

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

Equations

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

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

Equations

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

class LO.Modal.Standard.DeductionParameter.IsGeach {α : Type u_1} (L : LO.Modal.Standard.DeductionParameter α) (taples : List GeachTaple) : Type

• char : L = 𝐆𝐞(taples)

@[simp]

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

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

instance LO.Modal.Standard.DeductionParameter.IsGeach.instKNilGeachTaple {α : Type u_1} : 𝐊.IsGeach []

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instKNilGeachTaple = { char := ⋯ }

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

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instKDConsGeachTapleMkOfNatNatNil = { char := ⋯ }

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

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instKTConsGeachTapleMkOfNatNatNil = { char := ⋯ }

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

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instKTBConsGeachTapleMkOfNatNatNil = { char := ⋯ }

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

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instK4ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

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

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instS4ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instS4Dot2ConsGeachTapleMkOfNatNatNil {α : 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.Standard.DeductionParameter.IsGeach.instS4Dot2ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

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

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instS5ConsGeachTapleMkOfNatNatNil = { char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instKT4BConsGeachTapleMkOfNatNatNil {α : 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.Standard.DeductionParameter.IsGeach.instKT4BConsGeachTapleMkOfNatNatNil = { char := ⋯ }

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

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instTrivConsGeachTapleMkOfNatNatNil = { char := ⋯ }