Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KD

Imports

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

Imported by

LO.Modal.Kripke.SerialFrameClass

LO.Modal.Hilbert.KD.Kripke.sound

LO.Modal.Hilbert.KD.Kripke.consistent

LO.Modal.Hilbert.KD.Kripke.complete

KD #

@[reducible, inline]

abbrev LO.Modal.Kripke.SerialFrameClass :

Imported declaration from the Incompleteness formalization.

Equations

LO.Modal.Kripke.SerialFrameClass = {F : LO.Modal.Kripke.Frame | Serial F.Rel}

Instances For

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

Sound Hilbert.KD Kripke.SerialFrameClass

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

Entailment.Consistent Hilbert.KD

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

Complete Hilbert.KD Kripke.SerialFrameClass