Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.K

Imports

Init
LeanPool.Incompleteness.Foundation.Modal.Hilbert.K
LeanPool.Incompleteness.Foundation.Modal.Kripke.Completeness
LeanPool.Incompleteness.Foundation.Modal.Kripke.Filteration
LeanPool.Incompleteness.Foundation.Modal.Kripke.FiniteFrame
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Soundness

Imported by

LO.Modal.Hilbert.K.Kripke.sound

LO.Modal.Hilbert.K.instConsistentFormulaNat

LO.Modal.Hilbert.K.instCanonicalNatAllFrameClass

LO.Modal.Hilbert.K.Kripke.completeAll

LO.Modal.Hilbert.K.Kripke.completeAllFinite

K #

instance LO.Modal.Hilbert.K.Kripke.sound :

Sound Hilbert.K Kripke.AllFrameClass

instance LO.Modal.Hilbert.K.instConsistentFormulaNat :

Entailment.Consistent Hilbert.K

instance LO.Modal.Hilbert.K.instCanonicalNatAllFrameClass :

Kripke.Canonical Hilbert.K Kripke.AllFrameClass

instance LO.Modal.Hilbert.K.Kripke.completeAll :

Complete Hilbert.K Kripke.AllFrameClass

instance LO.Modal.Hilbert.K.Kripke.completeAllFinite :

Complete Hilbert.K Kripke.AllFiniteFrameClass