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]
Definitions occuring in definition :  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  FOSatWith: Dom,S,a |= fmla,  update-assignment: a[x := v]
FDL editor aliases :  FOQuantifier
Latex:
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: 2016_05_15-PM-10_12_38
Last ObjectModification: 2015_09_23-AM-08_22_47

Theory : minimal-first-order-logic


Home Index