FOM: finite and constructive choice (was: Mitteilungen der DMV)
Stephen G Simpson
simpson at math.psu.edu
Sun Mar 1 13:12:01 EST 1998
Vaughan Pratt 01 Mar 1998 08:51:47 writes:
> choice is a theorem of Z for any given finite sequence of nonempty
> sets. (But not uniformly: there is no single such theorem of ZF
> covering all finite lengths, otherwise one could prove that the
> reals can be well-ordered.)
Huh? The choice principle for all finite sequences of nonempty sets
is well known and easily seen to be a single theorem of ZF (or of Z
for that matter).
[ Here I assume that "finite" means "indexed by a finite ordinal
number". Pratt's remark and mine probably both fail if you take
"finite" in some other sense, e.g. perhaps what the set theorists
sometimes call D-finite. Are there any experts here who can confirm
this? A set is said to be D-finite if it is not in 1-1 correspondence
with any proper subset of itself. ]
Incidentally, the set-theoretic axiom of choice may not be what White
is actually using in his posting of Feb 1998 20:26:51. There are
constructive choice principles along the following lines: If we know
constructively that <A_i : i in I> is an indexed family of nonempty
sets, then our construction must automatically provide a function f on
I which witnesses each instance of nonemptiness, i.e. f(i) in A_i
uniformly in i, so f is a constructive choice function.
-- Steve
More information about the FOM
mailing list