Axioms

@[reducible, inline]

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

◇ is duality of □.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termKAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termKAx = Lean.ParserDescr.node `LO.Axioms.termKAx 1024 (Lean.ParserDescr.symbol "KAx")

@[reducible, inline]

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

Axiom for reflexive

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termTAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termTAx = Lean.ParserDescr.node `LO.Axioms.termTAx 1024 (Lean.ParserDescr.symbol "TAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.DiaTc φ = φ ==> ◇φ

@[reducible, inline]

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

Axiom for symmetric

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termBAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termBAx = Lean.ParserDescr.node `LO.Axioms.termBAx 1024 (Lean.ParserDescr.symbol "BAx")

@[reducible, inline]

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

□-only version of axiom BAx.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termBBoxAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termBBoxAx = Lean.ParserDescr.node `LO.Axioms.termBBoxAx 1024 (Lean.ParserDescr.symbol "BBoxAx")

@[reducible, inline]

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

Axiom for serial

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termDAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termDAx = Lean.ParserDescr.node `LO.Axioms.termDAx 1024 (Lean.ParserDescr.symbol "DAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.P = ∼□⊥

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termPAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termPAx = Lean.ParserDescr.node `LO.Axioms.termPAx 1024 (Lean.ParserDescr.symbol "PAx")

@[simp]

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

@[reducible, inline]

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

Axiom for transivity

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Axiom for euclidean

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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) : F

Axiom for confluency

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Axiom for density

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termC4Ax : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termC4Ax = Lean.ParserDescr.node `LO.Axioms.termC4Ax 1024 (Lean.ParserDescr.symbol "C4Ax")

@[reducible, inline]

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

Axiom for functionality

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termCDAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termCDAx = Lean.ParserDescr.node `LO.Axioms.termCDAx 1024 (Lean.ParserDescr.symbol "CDAx")

@[reducible, inline]

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

Axiom for coreflexivity

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termTcAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termTcAx = Lean.ParserDescr.node `LO.Axioms.termTcAx 1024 (Lean.ParserDescr.symbol "TcAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.DiaT φ = ◇φ ==> φ

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.Ver φ = □φ

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termVerAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termVerAx = Lean.ParserDescr.node `LO.Axioms.termVerAx 1024 (Lean.ParserDescr.symbol "VerAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termGrzAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termGrzAx = Lean.ParserDescr.node `LO.Axioms.termGrzAx 1024 (Lean.ParserDescr.symbol "GrzAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termMAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termMAx = Lean.ParserDescr.node `LO.Axioms.termMAx 1024 (Lean.ParserDescr.symbol "MAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termLAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termLAx = Lean.ParserDescr.node `LO.Axioms.termLAx 1024 (Lean.ParserDescr.symbol "LAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.H φ = □(□φ <=> φ) ==> □φ

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.termHAx : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Axioms.termHAx = Lean.ParserDescr.node `LO.Axioms.termHAx 1024 (Lean.ParserDescr.symbol "HAx")

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

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 : Geachean.Taple) : Set F

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Axioms.«termGeachAx(_)» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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