Nuprl Definition : FOL-abstract

FOL-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
Definitions occuring in definition : mFOL_ind: mFOL_ind, AbstractFOAtomic+: AbstractFOAtomic+(n;L), FOConnective+: FOConnective+(knd), apply: f a, FOQuantifier+: FOQuantifier+(isall)
FDL editor aliases : FOL-abstract

Latex:
FOL-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: 2016_05_15-PM-10_16_39 Last ObjectModification: 2015_09_23-AM-08_23_15 Theory : minimal-first-order-logic Home Index