Nuprl Definition : note-is-function
note-is-function(A;hnum;M) == if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= `function`] else M fi
Definitions occuring in Statement :
modelAdd: M[n:= lbl,i,j],
mFOLisAll: mFOLisAll(A),
mFOLisImp: mFOLisImp(A),
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
natural_number: $n,
token: "$token"
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
bor: p ∨bq,
mFOLisImp: mFOLisImp(A),
mFOLisAll: mFOLisAll(A),
modelAdd: M[n:= lbl,i,j],
token: "$token",
natural_number: $n
FDL editor aliases :
note-is-function
Latex:
note-is-function(A;hnum;M) == if mFOLisImp(A) \mvee{}\msubb{}mFOLisAll(A) then M[hnum:= `function`] else M fi
Date html generated:
2016_05_15-PM-10_32_40
Last ObjectModification:
2015_09_23-AM-08_26_28
Theory : minimal-first-order-logic
Home
Index