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