Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KDB

Imports

Init
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Geach

Imported by

LO.Modal.Kripke.SerialSymmetricFrameClass

LO.Modal.Hilbert.KDB.Kripke.sound

LO.Modal.Hilbert.KDB.Kripke.consistent

LO.Modal.Hilbert.KDB.Kripke.complete

KDB #

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialSymmetricFrameClass :

Imported declaration from the Incompleteness formalization.

Equations

LO.Modal.Kripke.SerialSymmetricFrameClass = {F : LO.Modal.Kripke.Frame | Serial F.Rel ∧ IsSymmetric F.Rel}

Instances For

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

Sound Hilbert.KDB Kripke.SerialSymmetricFrameClass

instance LO.Modal.Hilbert.KDB.Kripke.consistent :

Entailment.Consistent Hilbert.KDB

instance LO.Modal.Hilbert.KDB.Kripke.complete :

Complete Hilbert.KDB Kripke.SerialSymmetricFrameClass