Documentation

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

Soundness #

source
instance LO.Modal.Kripke.instDefinedByTransitiveIrreflexiveFiniteFrameClassInsertFormulaNatSetKAtomOfNatSingletonL :
TransitiveIrreflexiveFiniteFrameClass.DefinedBy {Axioms.K (Formula.atom 0) (Formula.atom 1), Axioms.L (Formula.atom 0)}
source
instance LO.Modal.Kripke.instIsNonemptyTransitiveIrreflexiveFiniteFrameClass :
TransitiveIrreflexiveFiniteFrameClass.IsNonempty
source
instance LO.Modal.Hilbert.GL.Kripke.finiteSound :
Sound Hilbert.GL Kripke.TransitiveIrreflexiveFiniteFrameClass
source
instance LO.Modal.Hilbert.GL.Kripke.consistent :
Entailment.Consistent Hilbert.GL