Documentation
Foundation
.
Modal
.
Logic
.
GLPlusBoxBot
.
Basic
Search
return to top
source
Imports
Init
Foundation.Modal.Logic.SumQuasiNormal
Foundation.Modal.Maximal.Unprovability
Mathlib.Data.ENat.Basic
Foundation.Modal.Kripke.Logic.GL.Completeness
Imported by
LO
.
Modal
.
GLPlusBoxBot
LO
.
Modal
.
instIsQuasiNormalNatGLPlusBoxBot
LO
.
Modal
.
instWeakerThanFormulaNatLogicGLGLPlusBoxBot
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
boxbot
LO
.
Modal
.
iff_provable_GLPlusBoxBot_provable_GL
LO
.
Modal
.
eq_GLPlusBoxBot_omega_GL
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
weakerThan_succ
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
weakerThan_add
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
weakerThan_lt
source
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
Instances For
source
instance
LO
.
Modal
.
instIsQuasiNormalNatGLPlusBoxBot
{
n
:
ℕ∞
}
:
(
Modal.GLPlusBoxBot
n
)
.
IsQuasiNormal
Equations
One or more equations did not get rendered due to their size.
source
instance
LO
.
Modal
.
instWeakerThanFormulaNatLogicGLGLPlusBoxBot
{
n
:
ℕ∞
}
:
Modal.GL
⪯
Modal.GLPlusBoxBot
n
source
@[simp]
theorem
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
boxbot
{
n
:
ℕ
}
:
Modal.GLPlusBoxBot
↑
n
⊢
□^[
n
]
⊥
source
theorem
LO
.
Modal
.
iff_provable_GLPlusBoxBot_provable_GL
{
n
:
ℕ
}
{
φ
:
Formula
ℕ
}
:
Modal.GLPlusBoxBot
↑
n
⊢
φ
↔
Modal.GL
⊢
□^[
n
]
⊥
➝
φ
source
@[simp]
theorem
LO
.
Modal
.
eq_GLPlusBoxBot_omega_GL
:
Modal.GLPlusBoxBot
⊤
=
Modal.GL
source
theorem
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
weakerThan_succ
{
n
:
ℕ
}
:
Modal.GLPlusBoxBot
(
↑
n
+
1
)
⪯
Modal.GLPlusBoxBot
↑
n
source
theorem
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
weakerThan_add
{
n
k
:
ℕ
}
:
Modal.GLPlusBoxBot
(
↑
n
+
↑
k
)
⪯
Modal.GLPlusBoxBot
↑
n
source
theorem
LO
.
Modal
.
Logic
.
GLPlusBoxBot
.
weakerThan_lt
{
n
m
:
ℕ
}
(
hmn
:
m
>
n
)
:
Modal.GLPlusBoxBot
↑
m
⪯
Modal.GLPlusBoxBot
↑
n