Documentation

Foundation.Propositional.FMT.Hilbert.VF_Ser

source
instance LO.Propositional.FMT.instIsNTSerialTrivialFrame :
trivialFrame.IsNTSerial
source
instance LO.Propositional.HilbertVF.VF_Ser.soundFMT :
Sound HilbertVF.VF_Ser {F : FMT.Frame | F.IsNTSerial}
source
instance LO.Propositional.HilbertVF.VF_Ser.instConsistentFormulaNat :
Entailment.Consistent HilbertVF.VF_Ser
source
instance LO.Propositional.HilbertVF.VF_Ser.completeFMT :
Complete HilbertVF.VF_Ser {F : FMT.Frame | F.IsNTSerial}
source
instance LO.Propositional.instStrictlyWeakerThanFormulaNatHilbertVFVFVF_Ser :
HilbertVF.VF ⪱ HilbertVF.VF_Ser