Nuprl Definition : AbstractFOAtomic
If S is a structure (for a domain Dom), then ⌈S n ∈ (Dom List) ─→ ℙ⌉.
If a is an assignment on Dom, then ⌈map(a;L) ∈ Dom List⌉. Thus, the
meaning of the atomic formula ⌈n(L)⌉
(which is predicate symbol ⌈n ∈ Atom⌉ applied to variable list ⌈L ∈ ℤ List⌉)
is S n map(a;L)⋅
AbstractFOAtomic(n;L) == λDom,S,a. (S n map(a;L))
Definitions occuring in Statement :
map: map(f;as),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
AbstractFOAtomic
AbstractFOAtomic(n;L) == \mlambda{}Dom,S,a. (S n map(a;L))
Date html generated:
2015_07_17-AM-07_53_14
Last ObjectModification:
2014_06_16-PM-01_00_12
Home
Index