def LO.Modal.GLPlusBoxBot (n : ℕ∞) : Logic ℕ

Equations

• LO.Modal.GLPlusBoxBot (some n_2) = LO.Modal.GL.sumQuasiNormal {□^[n_2]⊥}
• LO.Modal.GLPlusBoxBot none = LO.Modal.GL

@[implicit_reducible]

instance LO.Modal.instIsQuasiNormalNatGLPlusBoxBot {n : ℕ∞} : (Modal.GLPlusBoxBot n).IsQuasiNormal

Equations

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

instance LO.Modal.instWeakerThanFormulaNatLogicGLGLPlusBoxBot {n : ℕ∞} : Modal.GL ⪯ Modal.GLPlusBoxBot n

@[simp]

theorem LO.Modal.Logic.GLPlusBoxBot.boxbot {n : ℕ} : Modal.GLPlusBoxBot ↑n ⊢ □^[n]⊥

theorem LO.Modal.iff_provable_GLPlusBoxBot_provable_GL {n : ℕ} {φ : Formula ℕ} : Modal.GLPlusBoxBot ↑n ⊢ φ ↔ Modal.GL ⊢ □^[n]⊥ 🡒 φ

@[simp]

theorem LO.Modal.eq_GLPlusBoxBot_omega_GL : Modal.GLPlusBoxBot ⊤ = Modal.GL

theorem LO.Modal.Logic.GLPlusBoxBot.weakerThan_succ {n : ℕ} : Modal.GLPlusBoxBot (↑n + 1) ⪯ Modal.GLPlusBoxBot ↑n

theorem LO.Modal.Logic.GLPlusBoxBot.weakerThan_add {n k : ℕ} : Modal.GLPlusBoxBot (↑n + ↑k) ⪯ Modal.GLPlusBoxBot ↑n

theorem LO.Modal.Logic.GLPlusBoxBot.weakerThan_lt {n m : ℕ} (hmn : m > n) : Modal.GLPlusBoxBot ↑m ⪯ Modal.GLPlusBoxBot ↑n