FOM: finite and constructive choice (was: Mitteilungen der DMV)

[Stephen G Simpson]

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