Documentation
LeanPool
.
Incompleteness
.
Foundation
.
Modal
.
Kripke
.
Hilbert
.
Ver
Search
return to top
source
Imports
Init
LeanPool.Incompleteness.Foundation.Modal.Hilbert.WellKnown
LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomVer
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Soundness
Imported by
LO
.
Modal
.
Kripke
.
instCanonicalIsolatedFrameClass
LO
.
Modal
.
Hilbert
.
Ver
.
Kripke
.
sound
LO
.
Modal
.
Hilbert
.
Ver
.
Kripke
.
consistent
LO
.
Modal
.
Hilbert
.
Ver
.
Kripke
.
complete
Ver
#
source
instance
LO
.
Modal
.
Kripke
.
instCanonicalIsolatedFrameClass
{
S
:
Type
u_1}
[
Entailment
(
Formula
ℕ
)
S
]
{
𝓢
:
S
}
[
Entailment.Consistent
𝓢
]
[
Entailment.Ver
𝓢
]
:
Canonical
𝓢
IsolatedFrameClass
source
instance
LO
.
Modal
.
Hilbert
.
Ver
.
Kripke
.
sound
:
Sound
Hilbert.Ver
Kripke.IsolatedFrameClass
source
instance
LO
.
Modal
.
Hilbert
.
Ver
.
Kripke
.
consistent
:
Entailment.Consistent
Hilbert.Ver
source
instance
LO
.
Modal
.
Hilbert
.
Ver
.
Kripke
.
complete
:
Complete
Hilbert.Ver
Kripke.IsolatedFrameClass