@[reducible, inline]

abbrev LO.Axioms.DiaDuality {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] : F

◇ is duality of □.

Equations

• LO.Axioms.DiaDuality φ = ◇φ ⭤ ∼□(∼φ)

@[reducible, inline]

abbrev LO.Axioms.DiaDuality.set {F : Type u_1} [BasicModalLogicalConnective F] [Dia F] : Set F

Equations

• LO.Axioms.DiaDuality.set = {x : F | ∃ (φ : F), LO.Axioms.DiaDuality φ = x}

@[reducible, inline]

abbrev LO.Axioms.K {F : Type u_1} [BasicModalLogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.K φ ψ = □(φ ➝ ψ) ➝ □φ ➝ □ψ

@[reducible, inline]

abbrev LO.Axioms.K.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗞 = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.K φ ψ = x}

def LO.Axioms.«term𝗞» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗞» = Lean.ParserDescr.node `LO.Axioms.«term𝗞» 1024 (Lean.ParserDescr.symbol "𝗞")

@[reducible, inline]

abbrev LO.Axioms.T {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.T φ = □φ ➝ φ

@[reducible, inline]

abbrev LO.Axioms.T.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗧 = {x : F | ∃ (φ : F), LO.Axioms.T φ = x}

def LO.Axioms.«term𝗧» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗧» = Lean.ParserDescr.node `LO.Axioms.«term𝗧» 1024 (Lean.ParserDescr.symbol "𝗧")

@[reducible, inline]

abbrev LO.Axioms.B {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] : F

Equations

• LO.Axioms.B φ = φ ➝ □◇φ

@[reducible, inline]

abbrev LO.Axioms.B.set {F : Type u_1} [BasicModalLogicalConnective F] [Dia F] : Set F

Equations

• 𝗕 = {x : F | ∃ (φ : F), LO.Axioms.B φ = x}

def LO.Axioms.«term𝗕» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗕» = Lean.ParserDescr.node `LO.Axioms.«term𝗕» 1024 (Lean.ParserDescr.symbol "𝗕")

@[reducible, inline]

abbrev LO.Axioms.B₂ {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

□-only version of axiom 𝗕.

Equations

• LO.Axioms.B₂ φ = □φ ➝ □(∼□(∼φ))

@[reducible, inline]

abbrev LO.Axioms.B₂.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗕(□) = {x : F | ∃ (φ : F), LO.Axioms.B₂ φ = x}

def LO.Axioms.«term𝗕(□)» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗕(□)» = Lean.ParserDescr.node `LO.Axioms.«term𝗕(□)» 1024 (Lean.ParserDescr.symbol "𝗕(□)")

@[reducible, inline]

abbrev LO.Axioms.D {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] : F

Equations

• LO.Axioms.D φ = □φ ➝ ◇φ

@[reducible, inline]

abbrev LO.Axioms.D.set {F : Type u_1} [BasicModalLogicalConnective F] [Dia F] : Set F

Equations

• 𝗗 = {x : F | ∃ (φ : F), LO.Axioms.D φ = x}

def LO.Axioms.«term𝗗» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗗» = Lean.ParserDescr.node `LO.Axioms.«term𝗗» 1024 (Lean.ParserDescr.symbol "𝗗")

@[reducible, inline]

abbrev LO.Axioms.P {F : Type u_1} [BasicModalLogicalConnective F] : F

Equations

• LO.Axioms.P = ∼□⊥

@[reducible, inline]

abbrev LO.Axioms.P.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗣 = {x : F | LO.Axioms.P = x}

def LO.Axioms.«term𝗣» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗣» = Lean.ParserDescr.node `LO.Axioms.«term𝗣» 1024 (Lean.ParserDescr.symbol "𝗣")

@[simp]

theorem LO.Axioms.P.set.def {F : Type u_1} [BasicModalLogicalConnective F] : 𝗣 = {∼□⊥}

@[reducible, inline]

abbrev LO.Axioms.Four {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.Four φ = □φ ➝ □□φ

@[reducible, inline]

abbrev LO.Axioms.Four.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝟰 = {x : F | ∃ (φ : F), LO.Axioms.Four φ = x}

def LO.Axioms.«term𝟰» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝟰» = Lean.ParserDescr.node `LO.Axioms.«term𝟰» 1024 (Lean.ParserDescr.symbol "𝟰")

@[reducible, inline]

abbrev LO.Axioms.Five {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] : F

Equations

• LO.Axioms.Five φ = ◇φ ➝ □◇φ

@[reducible, inline]

abbrev LO.Axioms.Five.set {F : Type u_1} [BasicModalLogicalConnective F] [Dia F] : Set F

Equations

• 𝟱 = {x : F | ∃ (φ : F), LO.Axioms.Five φ = x}

def LO.Axioms.«term𝟱» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝟱» = Lean.ParserDescr.node `LO.Axioms.«term𝟱» 1024 (Lean.ParserDescr.symbol "𝟱")

@[reducible, inline]

abbrev LO.Axioms.Five₂ {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

□-only version of axiom 𝟱.

Equations

• LO.Axioms.Five₂ φ = ∼□φ ➝ □(∼□(∼φ))

@[reducible, inline]

abbrev LO.Axioms.Five₂.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝟱(□) = {x : F | ∃ (φ : F), LO.Axioms.Five₂ φ = x}

def LO.Axioms.«term𝟱(□)» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝟱(□)» = Lean.ParserDescr.node `LO.Axioms.«term𝟱(□)» 1024 (Lean.ParserDescr.symbol "𝟱(□)")

@[reducible, inline]

abbrev LO.Axioms.Dot2 {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] : F

Equations

• LO.Axioms.Dot2 φ = ◇□φ ➝ □◇φ

@[reducible, inline]

abbrev LO.Axioms.Dot2.set {F : Type u_1} [BasicModalLogicalConnective F] [Dia F] : Set F

Equations

• .𝟮 = {x : F | ∃ (φ : F), LO.Axioms.Dot2 φ = x}

def LO.Axioms.«term.𝟮» : Lean.ParserDescr

Equations

• LO.Axioms.«term.𝟮» = Lean.ParserDescr.node `LO.Axioms.«term.𝟮» 1024 (Lean.ParserDescr.symbol ".𝟮")

@[reducible, inline]

abbrev LO.Axioms.C4 {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.C4 φ = □□φ ➝ □φ

@[reducible, inline]

abbrev LO.Axioms.C4.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗖𝟰 = {x : F | ∃ (φ : F), LO.Axioms.C4 φ = x}

def LO.Axioms.«term𝗖𝟰» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗖𝟰» = Lean.ParserDescr.node `LO.Axioms.«term𝗖𝟰» 1024 (Lean.ParserDescr.symbol "𝗖𝟰")

@[reducible, inline]

abbrev LO.Axioms.CD {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] : F

Equations

• LO.Axioms.CD φ = ◇φ ➝ □φ

@[reducible, inline]

abbrev LO.Axioms.CD.set {F : Type u_1} [BasicModalLogicalConnective F] [Dia F] : Set F

Equations

• 𝗖𝗗 = {x : F | ∃ (φ : F), LO.Axioms.CD φ = x}

def LO.Axioms.«term𝗖𝗗» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗖𝗗» = Lean.ParserDescr.node `LO.Axioms.«term𝗖𝗗» 1024 (Lean.ParserDescr.symbol "𝗖𝗗")

@[reducible, inline]

abbrev LO.Axioms.Tc {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.Tc φ = φ ➝ □φ

@[reducible, inline]

abbrev LO.Axioms.Tc.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗧𝗰 = {x : F | ∃ (φ : F), LO.Axioms.Tc φ = x}

def LO.Axioms.«term𝗧𝗰» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗧𝗰» = Lean.ParserDescr.node `LO.Axioms.«term𝗧𝗰» 1024 (Lean.ParserDescr.symbol "𝗧𝗰")

@[reducible, inline]

abbrev LO.Axioms.Ver {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.Ver φ = □φ

@[reducible, inline]

abbrev LO.Axioms.Ver.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗩𝗲𝗿 = {x : F | ∃ (φ : F), LO.Axioms.Ver φ = x}

def LO.Axioms.«term𝗩𝗲𝗿» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗩𝗲𝗿» = Lean.ParserDescr.node `LO.Axioms.«term𝗩𝗲𝗿» 1024 (Lean.ParserDescr.symbol "𝗩𝗲𝗿")

@[reducible, inline]

abbrev LO.Axioms.Dot3 {F : Type u_1} [BasicModalLogicalConnective F] (φ ψ : F) : F

Equations

• LO.Axioms.Dot3 φ ψ = □(□φ ➝ ψ) ⋎ □(□ψ ➝ φ)

@[reducible, inline]

abbrev LO.Axioms.Dot3.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• .𝟯 = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Dot3 φ ψ = x}

def LO.Axioms.«term.𝟯» : Lean.ParserDescr

Equations

• LO.Axioms.«term.𝟯» = Lean.ParserDescr.node `LO.Axioms.«term.𝟯» 1024 (Lean.ParserDescr.symbol ".𝟯")

@[reducible, inline]

abbrev LO.Axioms.Grz {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.Grz φ = □(□(φ ➝ □φ) ➝ φ) ➝ φ

@[reducible, inline]

abbrev LO.Axioms.Grz.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗚𝗿𝘇 = {x : F | ∃ (φ : F), LO.Axioms.Grz φ = x}

def LO.Axioms.«term𝗚𝗿𝘇» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗚𝗿𝘇» = Lean.ParserDescr.node `LO.Axioms.«term𝗚𝗿𝘇» 1024 (Lean.ParserDescr.symbol "𝗚𝗿𝘇")

@[reducible, inline]

abbrev LO.Axioms.M {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) [Dia F] : F

Equations

• LO.Axioms.M φ = □◇φ ➝ ◇□φ

@[reducible, inline]

abbrev LO.Axioms.M.set {F : Type u_1} [BasicModalLogicalConnective F] [Dia F] : Set F

Equations

• 𝗠 = {x : F | ∃ (φ : F), LO.Axioms.M φ = x}

def LO.Axioms.«term𝗠» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗠» = Lean.ParserDescr.node `LO.Axioms.«term𝗠» 1024 (Lean.ParserDescr.symbol "𝗠")

@[reducible, inline]

abbrev LO.Axioms.L {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.L φ = □(□φ ➝ φ) ➝ □φ

@[reducible, inline]

abbrev LO.Axioms.L.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗟 = {x : F | ∃ (φ : F), LO.Axioms.L φ = x}

def LO.Axioms.«term𝗟» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗟» = Lean.ParserDescr.node `LO.Axioms.«term𝗟» 1024 (Lean.ParserDescr.symbol "𝗟")

@[reducible, inline]

abbrev LO.Axioms.H {F : Type u_1} [BasicModalLogicalConnective F] (φ : F) : F

Equations

• LO.Axioms.H φ = □(□φ ⭤ φ) ➝ □φ

@[reducible, inline]

abbrev LO.Axioms.H.set {F : Type u_1} [BasicModalLogicalConnective F] : Set F

Equations

• 𝗛 = {x : F | ∃ (φ : F), LO.Axioms.H φ = x}

def LO.Axioms.«term𝗛» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗛» = Lean.ParserDescr.node `LO.Axioms.«term𝗛» 1024 (Lean.ParserDescr.symbol "𝗛")

@[reducible, inline]

abbrev LO.Axioms.Geach {F : Type u_1} [BasicModalLogicalConnective F] (t : GeachConfluent.Taple) (φ : F) : F

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def LO.Axioms.MultiGeach.set {F : Type u_1} [BasicModalLogicalConnective F] : List GeachConfluent.Taple → 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} [BasicModalLogicalConnective F] : 𝗚𝗲([]) = ∅

theorem LO.Axioms.MultiGeach.def_one {F : Type u_1} [BasicModalLogicalConnective F] {t : GeachConfluent.Taple} : 𝗚𝗲([t]) = 𝗴𝗲(t)

theorem LO.Axioms.MultiGeach.def_two {F : Type u_1} [BasicModalLogicalConnective F] {t₁ t₂ : GeachConfluent.Taple} : 𝗚𝗲([t₁, t₂]) = 𝗴𝗲(t₁) ∪ 𝗴𝗲(t₂)

theorem LO.Axioms.MultiGeach.def_three {F : Type u_1} [BasicModalLogicalConnective F] {t₁ t₂ t₃ : GeachConfluent.Taple} : 𝗚𝗲([t₁, t₂, t₃]) = 𝗴𝗲(t₁) ∪ 𝗴𝗲(t₂) ∪ 𝗴𝗲(t₃)

@[simp]

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

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