Nuprl Definition : FOQuantifier

FOQuantifier(isall) ==
  λx,fmla,Dom,S,a. if isall then ∀v:Dom. Dom,S,a[x := v] |= fmla else ∃v:Dom. Dom,S,a[x := v] |= fmla fi 


Definitions occuring in Statement :  FOSatWith: Dom,S,a |= fmla,  update-assignment: a[x := v],  ifthenelse: if b then t else f fi ,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  lambda: λx.A[x]
FDL editor aliases :  FOQuantifier
FOQuantifier(isall)  ==
    \mlambda{}x,fmla,Dom,S,a.  if  isall
                                    then  \mforall{}v:Dom.  Dom,S,a[x  :=  v]  |=  fmla
                                    else  \mexists{}v:Dom.  Dom,S,a[x  :=  v]  |=  fmla
                                    fi 


Date html generated: 2015_07_17-AM-07_53_17
Last ObjectModification: 2012_09_06-AM-01_27_20

Home Index