Documentation
Foundation
.
Modal
.
Kripke
.
Logic
.
KB4
Search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Logic.K45
Foundation.Modal.Kripke.Logic.KB
Imported by
LO
.
Modal
.
Kripke
.
Frame
.
IsKB4
LO
.
Modal
.
Kripke
.
FrameClass
.
KB4
LO
.
Modal
.
Kripke
.
instIsK45OfIsKB4
LO
.
Modal
.
instSoundLogicNatFormulaFrameClassKB4KB4
LO
.
Modal
.
instConsistentFormulaNatLogicKB4
LO
.
Modal
.
instCanonicalLogicNatKB4KB4
LO
.
Modal
.
instCompleteLogicNatFormulaFrameClassKB4KB4
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicK45KB4
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicKBKB4
source
class
LO
.
Modal
.
Kripke
.
Frame
.
IsKB4
(
F
:
Frame
)
extends
Std.Symm
F
.
Rel
,
IsTrans
F
.
World
F
.
Rel
:
Prop
symm
(
a
b
:
F
.
World
)
:
F
.
Rel
a
b
→
F
.
Rel
b
a
trans
(
a
b
c
:
F
.
World
)
:
F
.
Rel
a
b
→
F
.
Rel
b
c
→
F
.
Rel
a
c
Instances
source
@[reducible, inline]
abbrev
LO
.
Modal
.
Kripke
.
FrameClass
.
KB4
:
FrameClass
Equations
LO.Modal.Kripke.FrameClass.KB4
=
{
F
:
LO.Modal.Kripke.Frame
|
F
.
IsKB4
}
Instances For
source
instance
LO
.
Modal
.
Kripke
.
instIsK45OfIsKB4
{
F
:
Frame
}
[
F
.
IsKB4
]
:
F
.
IsK45
source
instance
LO
.
Modal
.
instSoundLogicNatFormulaFrameClassKB4KB4
:
Sound
Modal.KB4
Kripke.FrameClass.KB4
source
instance
LO
.
Modal
.
instConsistentFormulaNatLogicKB4
:
Entailment.Consistent
Modal.KB4
source
instance
LO
.
Modal
.
instCanonicalLogicNatKB4KB4
:
Kripke.Canonical
Modal.KB4
Kripke.FrameClass.KB4
source
instance
LO
.
Modal
.
instCompleteLogicNatFormulaFrameClassKB4KB4
:
Complete
Modal.KB4
Kripke.FrameClass.KB4
source
instance
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicK45KB4
:
Modal.K45
⪱
Modal.KB4
source
instance
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicKBKB4
:
Modal.KB
⪱
Modal.KB4