Nuprl Definition : valuation
valuation(v0;x;f) == ∀a:{a:formula()| a ⊆ x} . f a = extend-val(v0;f;a)
Definitions occuring in Statement :
extend-val: extend-val(v0;g;x),
psub: a ⊆ b,
formula: formula(),
bool: 𝔹,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
formula: formula(),
psub: a ⊆ b,
equal: s = t ∈ T,
bool: 𝔹,
apply: f a,
extend-val: extend-val(v0;g;x)
FDL editor aliases :
valuation
Latex:
valuation(v0;x;f) == \mforall{}a:\{a:formula()| a \msubseteq{} x\} . f a = extend-val(v0;f;a)
Date html generated:
2016_05_15-PM-07_15_36
Last ObjectModification:
2015_09_23-AM-08_13_38
Theory : general
Home
Index