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