Nuprl Definition : mFOL-abstract

The abstract meaning of a mFOL() formula defined inductively.
Alpha-equal formulas define the same abstract formula.⋅

mFOL-abstract(fmla) ==
  mFOL_ind(fmla;
           mFOatomic(R,vars)⇒ AbstractFOAtomic(R;vars);
           mFOconnect(knd,a,b)⇒ r1,r2.FOConnective(knd) r1 r2;
           mFOquant(isall,x,body)⇒ r.FOQuantifier(isall) x r)

Definitions occuring in Statement : mFOL_ind: mFOL_ind, FOQuantifier: FOQuantifier(isall), FOConnective: FOConnective(knd), AbstractFOAtomic: AbstractFOAtomic(n;L), apply: f a
FDL editor aliases : mFOL-abstract
mFOL-abstract(fmla) == mFOL\_ind(fmla; mFOatomic(R,vars){}\mRightarrow{} AbstractFOAtomic(R;vars); mFOconnect(knd,a,b){}\mRightarrow{} r1,r2.FOConnective(knd) r1 r2; mFOquant(isall,x,body){}\mRightarrow{} r.FOQuantifier(isall) x r) Date html generated: 2015_07_17-AM-07_54_22 Last ObjectModification: 2012_09_11-PM-05_39_25 Home Index