@[reducible, inline]

abbrev LO.Axioms.DiaDuality {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] : F

◇ is duality of □.

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Axioms.K {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) (q : F) : F

Equations

• LO.Axioms.K p q = □(p ➝ q) ➝ □p ➝ □q

@[reducible, inline]

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

Equations

• 𝗞 = {x : F | ∃ (p : F) (q : F), LO.Axioms.K p q = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet

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} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_1

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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

□-only version of axiom 𝗕.

Equations

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

@[reducible, inline]

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

Equations

• 𝗕(□) = {x : F | ∃ (p : F), LO.Axioms.B₂ p = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_2

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} [LO.LogicalConnective F] [LO.Box F] : F

Alternative form of axiom 𝗗. In sight of provability logic, this can be seen as consistency of theory.

Equations

• LO.Axioms.D₂ = ∼□⊥

@[reducible, inline]

abbrev LO.Axioms.D₂.set {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] : Set F

Equations

• 𝗗(⊥) = {x : 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 "𝗗(⊥)")

@[simp]

theorem LO.Axioms.D₂.set.def {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] : 𝗗(⊥) = {∼□⊥}

@[reducible, inline]

abbrev LO.Axioms.Four {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_3

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} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_4

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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

□-only version of axiom 𝟱.

Equations

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

@[reducible, inline]

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

Equations

• 𝟱(□) = {x : F | ∃ (p : F), LO.Axioms.Five₂ p = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_5

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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_6

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} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_7

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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Axioms.instIsGeachSet_8

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} [LO.Box F] (p : F) : F

Equations

• LO.Axioms.Ver p = □p

@[reducible, inline]

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

Equations

• 𝗩𝗲𝗿 = {x : F | ∃ (p : F), LO.Axioms.Ver p = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) (q : F) : F

Equations

• LO.Axioms.Dot3 p q = □(□p ➝ q) ⋎ □(□q ➝ p)

@[reducible, inline]

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

Equations

• .𝟯 = {x : F | ∃ (p : F) (q : F), LO.Axioms.Dot3 p q = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

Equations

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

@[reducible, inline]

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

Equations

• 𝗚𝗿𝘇 = {x : F | ∃ (p : F), LO.Axioms.Grz p = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) [LO.Dia F] : F

Equations

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

@[reducible, inline]

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

Equations

• 𝗠 = {x : F | ∃ (p : F), LO.Axioms.M p = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

Equations

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

@[reducible, inline]

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

Equations

• 𝗟 = {x : F | ∃ (p : F), LO.Axioms.L p = 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} [LO.LogicalConnective F] [LO.Box F] (p : F) : F

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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