Nuprl Definition : FOL-proveable
FOL-proveable(s) ==  proveable(mFOL-sequent();FOLRule();λsr.FOLeffect(sr);s)
Definitions occuring in Statement : 
FOLeffect: FOLeffect(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]
, 
FOLeffect: FOLeffect(sr)
FDL editor aliases : 
FOL-proveable
Latex:
FOL-proveable(s)  ==    proveable(mFOL-sequent();FOLRule();\mlambda{}sr.FOLeffect(sr);s)
Date html generated:
2016_05_15-PM-10_28_35
Last ObjectModification:
2015_09_23-AM-08_25_48
Theory : minimal-first-order-logic
Home
Index