Nuprl Definition : mFOL-proveable
Provability of mFOL() sequent s.⋅
mFOL-proveable(s) == proveable(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr);s)
Definitions occuring in Statement :
mFOLeffect: mFOLeffect(sr),
mFOL-sequent: mFOL-sequent(),
mFOLRule: mFOLRule(),
lambda: λx.A[x],
proveable: proveable(Sequent;Rule;effect;s)
FDL editor aliases :
mFOL-proveable
mFOL-proveable(s) == proveable(mFOL-sequent();mFOLRule();\mlambda{}sr.mFOLeffect(sr);s)
Date html generated:
2015_07_17-AM-07_56_53
Last ObjectModification:
2012_09_11-PM-05_47_40
Home
Index