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]
Definitions occuring in definition : lambda: λx.A[x], apply: f a, map: map(f;as)
FDL editor aliases : AbstractFOAtomic

Latex:
AbstractFOAtomic(n;L) == \mlambda{}Dom,S,a. (S n map(a;L)) Date html generated: 2016_07_08-PM-05_19_23 Last ObjectModification: 2015_09_23-AM-08_22_45 Theory : minimal-first-order-logic Home Index