Documentation
Foundation
.
Modal
.
Modality
.
S5
Search
return to top
source
Imports
Init
Foundation.Modal.Modality.Basic
Foundation.Modal.Kripke.Logic.S5
Imported by
LO
.
Modal
.
S5
.
modalities
LO
.
Modal
.
S5
.
modal_reduction_0
LO
.
Modal
.
S5
.
modal_reduction_1
LO
.
Modal
.
S5
.
instS5LogicNatFormula
LO
.
Modal
.
S5
.
instS4LogicNatFormula
LO
.
Modal
.
S5
.
instEquivalenceBoxPbox
LO
.
Modal
.
S5
.
instEquivalenceBoxPdia
LO
.
Modal
.
S5
.
instEquivalenceDiaPdia
LO
.
Modal
.
S5
.
instEquivalenceDiaPbox
LO
.
Modal
.
S5
.
modal_reduction_2
LO
.
Modal
.
S5
.
instEquivalenceNegBoxPnegPdia
LO
.
Modal
.
S5
.
instEquivalenceNegBoxPbox
LO
.
Modal
.
S5
.
instEquivalenceNegDiaPdia
LO
.
Modal
.
S5
.
instEquivalenceNegBoxPdia
LO
.
Modal
.
S5
.
instEquivalenceNegDiaPbox
LO
.
Modal
.
S5
.
instEquivalenceDiaNegPnegPdia
LO
.
Modal
.
S5
.
instEquivalenceDiaNegPbox
LO
.
Modal
.
S5
.
instEquivalenceDiaNegPdia
LO
.
Modal
.
S5
.
instEquivalenceDiaBoxPbox
LO
.
Modal
.
S5
.
instEquivalenceDiaBoxPdia
LO
.
Modal
.
S5
.
instEquivalenceDiaBoxPnegNegPdia
LO
.
Modal
.
S5
.
instEquivalenceDiaPnegNegPbox
LO
.
Modal
.
S5
.
instEquivalenceDiaPbox_1
LO
.
Modal
.
S5
.
instEquivalenceDiaPdia_1
LO
.
Modal
.
S5
.
modal_reduction_3
LO
.
Modal
.
S5
.
modal_reduction
source
@[reducible, inline]
abbrev
LO
.
Modal
.
S5
.
modalities
:
Modalities
Equations
LO.Modal.S5.modalities
=
{
-
,
∼
,
□
,
◇
,
∼
□
,
∼
◇
}
Instances For
source
theorem
LO
.
Modal
.
S5
.
modal_reduction_0
:
ModalReduction
Modal.S5
0
S5.modalities
source
theorem
LO
.
Modal
.
S5
.
modal_reduction_1
:
ModalReduction
Modal.S5
1
S5.modalities
source
instance
LO
.
Modal
.
S5
.
instS5LogicNatFormula
:
Entailment.S5
Modal.S5
Equations
One or more equations did not get rendered due to their size.
source
instance
LO
.
Modal
.
S5
.
instS4LogicNatFormula
:
Entailment.S4
Modal.S5
Equations
One or more equations did not get rendered due to their size.
source
instance
LO
.
Modal
.
S5
.
instEquivalenceBoxPbox
:
(
□
□
)
≅[
Modal.S5
]
□
source
instance
LO
.
Modal
.
S5
.
instEquivalenceBoxPdia
:
(
□
◇
)
≅[
Modal.S5
]
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaPdia
:
(
◇
◇
)
≅[
Modal.S5
]
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaPbox
:
(
◇
□
)
≅[
Modal.S5
]
□
source
theorem
LO
.
Modal
.
S5
.
modal_reduction_2
:
ModalReduction
Modal.S5
2
S5.modalities
source
instance
LO
.
Modal
.
S5
.
instEquivalenceNegBoxPnegPdia
:
(
∼
□
∼
)
≅[
Modal.S5
]
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceNegBoxPbox
:
(
∼
□
□
)
≅[
Modal.S5
]
∼
□
source
instance
LO
.
Modal
.
S5
.
instEquivalenceNegDiaPdia
:
(
∼
◇
◇
)
≅[
Modal.S5
]
∼
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceNegBoxPdia
:
(
∼
□
◇
)
≅[
Modal.S5
]
∼
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceNegDiaPbox
:
(
∼
◇
□
)
≅[
Modal.S5
]
∼
□
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaNegPnegPdia
:
(
◇
∼
∼
)
≅[
Modal.S5
]
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaNegPbox
:
(
◇
∼
□
)
≅[
Modal.S5
]
∼
□
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaNegPdia
:
(
◇
∼
◇
)
≅[
Modal.S5
]
∼
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaBoxPbox
:
(
◇
□
□
)
≅[
Modal.S5
]
□
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaBoxPdia
:
(
◇
□
◇
)
≅[
Modal.S5
]
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaBoxPnegNegPdia
:
(
◇
□
∼
)
≅[
Modal.S5
]
∼
◇
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaPnegNegPbox
:
(
◇
◇
∼
)
≅[
Modal.S5
]
∼
□
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaPbox_1
:
(
◇
◇
□
)
≅[
Modal.S5
]
◇
□
source
instance
LO
.
Modal
.
S5
.
instEquivalenceDiaPdia_1
:
(
◇
◇
◇
)
≅[
Modal.S5
]
◇
source
theorem
LO
.
Modal
.
S5
.
modal_reduction_3
:
ModalReduction
Modal.S5
3
S5.modalities
source
theorem
LO
.
Modal
.
S5
.
modal_reduction
(
n
:
ℕ
)
:
ModalReduction
Modal.S5
n
S5.modalities