structure LO.System.Axioms.Geach.Taple : Type

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

@[reducible, inline]

abbrev LO.System.Axioms.Geach {F : Type u_1} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] (l : LO.System.Axioms.Geach.Taple) (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 : LO.System.Axioms.Geach.Taple) : 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 : LO.System.Axioms.Geach.Taple
• 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 LO.System.Axioms.Geach.Taple → 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 : LO.System.Axioms.Geach.Taple} {l : List LO.System.Axioms.Geach.Taple} : 𝗚𝗲(x :: l) = 𝗴𝗲(x) ∪ 𝗚𝗲(l)

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

@[reducible, inline]

abbrev LO.Modal.Standard.DeductionParameter.Geach {α : Type u_1} (l : List LO.System.Axioms.Geach.Taple) : 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 α) : Type

• taples : List LO.System.Axioms.Geach.Taple
• char : L = 𝐆𝐞(LO.Modal.Standard.DeductionParameter.IsGeach.taples L)

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

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

instance LO.Modal.Standard.DeductionParameter.IsGeach.instIsNormal {α : Type u_1} {L : LO.Modal.Standard.DeductionParameter α} [geach : L.IsGeach] : L.IsNormal

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instIsNormal = ⋯.mpr inferInstance

instance LO.Modal.Standard.DeductionParameter.IsGeach.instK {α : Type u_1} : 𝐊.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instK = { taples := [], char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instKD {α : Type u_1} : 𝐊𝐃.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instKD = { taples := [{ i := 0, j := 0, m := 1, n := 1 }], char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instKT {α : Type u_1} : 𝐊𝐓.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instKT = { taples := [{ i := 0, j := 0, m := 1, n := 0 }], char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instKTB {α : Type u_1} : 𝐊𝐓𝐁.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instKTB = { taples := [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }], char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instK4 {α : Type u_1} : 𝐊𝟒.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instK4 = { taples := [{ i := 0, j := 2, m := 1, n := 0 }], char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instS4 {α : Type u_1} : 𝐒𝟒.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instS4 = { taples := [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }], char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instS4Dot2 {α : Type u_1} : 𝐒𝟒.𝟐.IsGeach

Equations

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

instance LO.Modal.Standard.DeductionParameter.IsGeach.instS5 {α : Type u_1} : 𝐒𝟓.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instS5 = { taples := [{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }], char := ⋯ }

instance LO.Modal.Standard.DeductionParameter.IsGeach.instKT4B {α : Type u_1} : 𝐊𝐓𝟒𝐁.IsGeach

Equations

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

instance LO.Modal.Standard.DeductionParameter.IsGeach.instTriv {α : Type u_1} : 𝐓𝐫𝐢𝐯.IsGeach

Equations

• LO.Modal.Standard.DeductionParameter.IsGeach.instTriv = { taples := [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 0 }], char := ⋯ }