Documentation

Foundation.Propositional.Kripke2.Hilbert.F_Sym

source
instance LO.Propositional.Kripke2.instIsSymmetricTrivialFrame :
trivialFrame.IsSymmetric
source
instance LO.Propositional.HilbertF.F_Sym.soundKripke2 :
Sound HilbertF.F_Sym {F : Kripke2.Frame | F.IsSymmetric}
source
instance LO.Propositional.HilbertF.F_Sym.instConsistentFormulaNat :
Entailment.Consistent HilbertF.F_Sym
source
instance LO.Propositional.instStrictlyWeakerThanFormulaNatHilbertFFF_Sym :
HilbertF.F ⪱ HilbertF.F_Sym