Documentation

ProvabilityLogic.Logic.GLPoint3OplusBoxBot.Basic

source
def LogicGLPoint3OplusBoxBot {α : Type u_1} :
ℕ∞ → Logic α

LogicGLPoint3OplusBoxBot n: the normal extension of LogicGLPoint3 by the boxbot axiom □^[n]⊥ for a finite n, and LogicGLPoint3 itself for n = ∞.

Equations
Instances For
    source
    @[simp]
    theorem LogicGLPoint3OplusBoxBot.eq_some {α : Type u_1} {n : ℕ} :
    LogicGLPoint3OplusBoxBot ↑n = (LogicGLPoint3 ⊕ᴸ {□^[n]⊥})

    LogicGLPoint3OplusBoxBot n unfolds to LogicGLPoint3 ⊕ᴸ {□^[n]⊥} for finite n.

    source
    theorem LogicGLPoint3OplusBoxBot.provable_of_provable_GLPoint3 {α : Type u_1} {n : ℕ} {A : Formula α} (h : A ∈ LogicGLPoint3) :
    A ∈ LogicGLPoint3OplusBoxBot ↑n

    Lift a LogicGLPoint3 theorem into LogicGLPoint3OplusBoxBot n.

    source
    theorem LogicGLPoint3OplusBoxBot.boxbot {α : Type u_1} {n : ℕ} :
    □^[n]⊥ ∈ LogicGLPoint3OplusBoxBot ↑n

    The boxbot axiom □^[n]⊥ is provable in LogicGLPoint3OplusBoxBot n.

    source
    theorem LogicGLPoint3OplusBoxBot.axiomNVer {α : Type u_1} [DecidableEq α] {n : ℕ} {A : Formula α} :
    □^[n]A ∈ LogicGLPoint3OplusBoxBot ↑n

    □^[n]A is provable in LogicGLPoint3OplusBoxBot n.

    source
    theorem LogicGLPoint3OplusBoxBot.of_GL {α : Type u_1} {n : ℕ} {A : Formula α} (h : A ∈ LogicGL) :
    A ∈ LogicGLPoint3OplusBoxBot ↑n

    Lift a GL theorem into LogicGLPoint3OplusBoxBot n.

    source
    theorem LogicGLPoint3OplusBoxBot.imp_trans {α : Type u_1} {n : ℕ} {A B C : Formula α} (hAB : A 🡒 B ∈ LogicGLPoint3OplusBoxBot ↑n) (hBC : B 🡒 C ∈ LogicGLPoint3OplusBoxBot ↑n) :
    A 🡒 C ∈ LogicGLPoint3OplusBoxBot ↑n

    Transitivity of implication inside LogicGLPoint3OplusBoxBot n.

    source
    theorem LogicGLPoint3OplusBoxBot.provable_CD {α : Type u_1} [DecidableEq α] {C : Formula α} :
    ◇C 🡒 □C ∈ LogicGLPoint3OplusBoxBot 2

    The axiom ◇C 🡒 □C is provable in LogicGLPoint3OplusBoxBot 2.

    source
    theorem LogicGLPoint3OplusBoxBot.provable_weakPoint2_in_2 {α : Type u_1} [DecidableEq α] {A B : Formula α} :
    ◇(□A ⋏ B) 🡒 □(◇A ⋎ B) ∈ LogicGLPoint3OplusBoxBot 2

    The convergence axiom .2 (WeakPoint2) is provable in LogicGLPoint3OplusBoxBot 2.

    source
    theorem eq_GLPoint3OplusBoxBot_2_GLPoint2 {α : Type u_1} [DecidableEq α] :
    LogicGLPoint3OplusBoxBot 2 = LogicGLPoint2

    LogicGLPoint3OplusBoxBot 2 = LogicGLPoint2.