Nuprl Definition : p-selector
y is a "root" of the decidable property p
if p y = ff
(thinking of ff as being 0 and tt as non-zero).
x is a selector for decidable property p if
x is a root of p if and only if p has a root.
( a non-void, compact type T has a selector
see: compact-type-compact-type2)⋅
p-selector(T;x;p) == (∃y:T. p y = ff) ⇒ p x = ff
Definitions occuring in Statement :
bfalse: ff,
bool: 𝔹,
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
implies: P ⇒ Q,
exists: ∃x:A. B[x],
equal: s = t ∈ T,
bool: 𝔹,
apply: f a,
bfalse: ff
FDL editor aliases :
p-selector
Latex:
p-selector(T;x;p) == (\mexists{}y:T. p y = ff) {}\mRightarrow{} p x = ff
Date html generated:
2016_07_08-PM-04_55_02
Last ObjectModification:
2015_09_23-AM-07_37_04
Theory : basic
Home
Index