Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.S4Dot3

Imports

Init
LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomDot3
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.S4

Imported by

LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass

LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass.DefinedByS4Dot3Axioms

LO.Modal.instIsNonemptyReflexiveTransitiveConnectedFrameClass

LO.Modal.Hilbert.S4Dot3.Kripke.sound

LO.Modal.Hilbert.S4Dot3.Kripke.consistent

LO.Modal.Hilbert.S4Dot3.Kripke.canonical

LO.Modal.Hilbert.S4Dot3.Kripke.complete

S4Dot3 #

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass :

Imported declaration from the Incompleteness formalization.

Equations

LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass = {F : LO.Modal.Kripke.Frame | Std.Refl F.Rel ∧ IsTrans F.World F.Rel ∧ Connected F.Rel}

Instances For

instance LO.Modal.Kripke.ReflexiveTransitiveConnectedFrameClass.DefinedByS4Dot3Axioms :

ReflexiveTransitiveConnectedFrameClass.DefinedBy Hilbert.S4Dot3.axioms

instance LO.Modal.instIsNonemptyReflexiveTransitiveConnectedFrameClass :

Kripke.ReflexiveTransitiveConnectedFrameClass.IsNonempty

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

Sound Hilbert.S4Dot3 Kripke.ReflexiveTransitiveConnectedFrameClass

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

Entailment.Consistent Hilbert.S4Dot3

instance LO.Modal.Hilbert.S4Dot3.Kripke.canonical :

Kripke.Canonical Hilbert.S4Dot3 Kripke.ReflexiveTransitiveConnectedFrameClass

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

Complete Hilbert.S4Dot3 Kripke.ReflexiveTransitiveConnectedFrameClass