Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Grz.Soundness

Soundness #

source
instance LO.Modal.Kripke.instDefinedByReflexiveTransitiveAntiSymmetricFiniteFrameClassInsertFormulaNatSetKAtomOfNatSingletonGrz :
ReflexiveTransitiveAntiSymmetricFiniteFrameClass.DefinedBy {Axioms.K (Formula.atom 0) (Formula.atom 1), Axioms.Grz (Formula.atom 0)}
source
instance LO.Modal.Kripke.instIsNonemptyReflexiveTransitiveAntiSymmetricFiniteFrameClass :
ReflexiveTransitiveAntiSymmetricFiniteFrameClass.IsNonempty
source
instance LO.Modal.Hilbert.Grz.Kripke.sound :
Sound Hilbert.Grz Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass
source
instance LO.Modal.Hilbert.Grz.Kripke.consistent :
Entailment.Consistent Hilbert.Grz