Geach

@[reducible, inline]

abbrev LO.Modal.Hilbert.Geach (G : Set Geachean.Taple) : Hilbert ℕ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.instHasKNatGeach {G : Set Geachean.Taple} : (Hilbert.Geach G).HasK

Equations

• LO.Modal.Hilbert.instHasKNatGeach = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatGeach._proof_1, mem_K := ⋯ }

@[implicit_reducible]

instance LO.Modal.Hilbert.instKNatFormulaGeach {G : Set Geachean.Taple} : Entailment.K (Hilbert.Geach G)

Equations

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

theorem LO.Modal.Hilbert.K4.eq_Geach : Hilbert.K4 = Hilbert.Geach {{ i := 0, j := 2, m := 1, n := 0 }}

theorem LO.Modal.Hilbert.K45.eq_Geach : Hilbert.K45 = Hilbert.Geach {{ i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.K5.eq_Geach : Hilbert.K5 = Hilbert.Geach {{ i := 1, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.KB.eq_Geach : Hilbert.KB = Hilbert.Geach {{ i := 0, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.KB4.eq_Geach : Hilbert.KB4 = Hilbert.Geach {{ i := 0, j := 1, m := 0, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }}

theorem LO.Modal.Hilbert.KB5.eq_Geach : Hilbert.KB5 = Hilbert.Geach {{ i := 0, j := 1, m := 0, n := 1 }, { i := 1, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.KD.eq_Geach : Hilbert.KD = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 1 }}

theorem LO.Modal.Hilbert.KD4.eq_Geach : Hilbert.KD4 = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }}

theorem LO.Modal.Hilbert.KD45.eq_Geach : Hilbert.KD45 = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.KD5.eq_Geach : Hilbert.KD5 = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 1 }, { i := 1, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.KDB.eq_Geach : Hilbert.KDB = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 1 }, { i := 0, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.KT.eq_Geach : Hilbert.KT = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 0 }}

theorem LO.Modal.Hilbert.KTB.eq_Geach : Hilbert.KTB = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.S4.eq_Geach : Hilbert.S4 = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }}

theorem LO.Modal.Hilbert.S5.eq_Geach : Hilbert.S5 = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.KT4B.eq_Geach : Hilbert.KT4B = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }}

theorem LO.Modal.Hilbert.S4Dot2.eq_Geach : Hilbert.S4Dot2 = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 1, n := 1 }}

theorem LO.Modal.Hilbert.Triv.eq_Geach : Hilbert.Triv = Hilbert.Geach {{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 0 }}

@[reducible]

def LO.Modal.Hilbert.HasTOfMem0010 {G : Set Geachean.Taple} (h : { i := 0, j := 0, m := 1, n := 0 } ∈ G) : (Hilbert.Geach G).HasT

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.HasTOfMem0010 h = { p := 0, mem_T := ⋯ }

@[reducible]

def LO.Modal.Hilbert.HasB_of_mem_0_1_0_1 {G : Set Geachean.Taple} (h : { i := 0, j := 1, m := 0, n := 1 } ∈ G) : (Hilbert.Geach G).HasB

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.HasB_of_mem_0_1_0_1 h = { p := 0, mem_B := ⋯ }

@[reducible]

def LO.Modal.Hilbert.HasD_of_mem_0_0_1_1 {G : Set Geachean.Taple} (h : { i := 0, j := 0, m := 1, n := 1 } ∈ G) : (Hilbert.Geach G).HasD

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.HasD_of_mem_0_0_1_1 h = { p := 0, mem_D := ⋯ }

@[reducible]

def LO.Modal.Hilbert.HasFourOfMem0210 {G : Set Geachean.Taple} (h : { i := 0, j := 2, m := 1, n := 0 } ∈ G) : (Hilbert.Geach G).HasFour

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.HasFourOfMem0210 h = { p := 0, mem_Four := ⋯ }

@[reducible]

def LO.Modal.Hilbert.HasFive_of_mem_1_1_0_1 {G : Set Geachean.Taple} (h : { i := 1, j := 1, m := 0, n := 1 } ∈ G) : (Hilbert.Geach G).HasFive

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.HasFive_of_mem_1_1_0_1 h = { p := 0, mem_Five := ⋯ }

@[reducible]

def LO.Modal.Hilbert.HasDot2_of_mem_1_1_1_1 {G : Set Geachean.Taple} (h : { i := 1, j := 1, m := 1, n := 1 } ∈ G) : (Hilbert.Geach G).HasDot2

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.HasDot2_of_mem_1_1_1_1 h = { p := 0, mem_Dot2 := ⋯ }

@[reducible]

def LO.Modal.Hilbert.HasTcOfMem0100 {G : Set Geachean.Taple} (h : { i := 0, j := 1, m := 0, n := 0 } ∈ G) : (Hilbert.Geach G).HasTc

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.HasTcOfMem0100 h = { p := 0, mem_Tc := ⋯ }