Nuprl Definition : FOQuantifier+
FOQuantifier+(isall) ==
  λx,fmla,Dom,S,a. if isall
                  then (∀v:Dom. Dom,S,a[x := v] +|= fmla) ⋃ (S "false" [])
                  else (∃v:Dom. Dom,S,a[x := v] +|= fmla) ⋃ (S "false" [])
                  fi 
Definitions occuring in Statement : 
FOSatWith+: Dom,S,a +|= fmla
, 
update-assignment: a[x := v]
, 
nil: []
, 
b-union: A ⋃ B
, 
ifthenelse: if b then t else f fi 
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
apply: f a
, 
lambda: λx.A[x]
, 
token: "$token"
Definitions occuring in definition : 
lambda: λx.A[x]
, 
ifthenelse: if b then t else f fi 
, 
all: ∀x:A. B[x]
, 
b-union: A ⋃ B
, 
exists: ∃x:A. B[x]
, 
FOSatWith+: Dom,S,a +|= fmla
, 
update-assignment: a[x := v]
, 
apply: f a
, 
token: "$token"
, 
nil: []
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)  \mcup{}  (S  "false"  [])
                                    else  (\mexists{}v:Dom.  Dom,S,a[x  :=  v]  +|=  fmla)  \mcup{}  (S  "false"  [])
                                    fi 
Date html generated:
2016_05_15-PM-10_12_41
Last ObjectModification:
2015_09_23-AM-08_22_48
Theory : minimal-first-order-logic
Home
Index