Nuprl Definition : mFOL-proveable
Provability of mFOL() sequent s.⋅
mFOL-proveable(s) == proveable(mFOL-sequent();FOLRule();λsr.mFOLeffect(sr);s)
Definitions occuring in Statement :
mFOLeffect: mFOLeffect(sr),
mFOL-sequent: mFOL-sequent(),
FOLRule: FOLRule(),
proveable: proveable(Sequent;Rule;effect;s),
lambda: λx.A[x]
Definitions occuring in definition :
proveable: proveable(Sequent;Rule;effect;s),
mFOL-sequent: mFOL-sequent(),
FOLRule: FOLRule(),
lambda: λx.A[x],
mFOLeffect: mFOLeffect(sr)
FDL editor aliases :
mFOL-proveable
Latex:
mFOL-proveable(s) == proveable(mFOL-sequent();FOLRule();\mlambda{}sr.mFOLeffect(sr);s)
Date html generated:
2016_07_08-PM-05_22_20
Last ObjectModification:
2015_09_23-PM-06_53_47
Theory : minimal-first-order-logic
Home
Index