FOM: finite choice

[Kanovei]

>Date: Sun, 01 Mar 1998 08:51:47 +0000
>From: Vaughan Pratt <pratt at cs.stanford.edu>

<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.)

Finite choice is a "single theorem" of ZF and Z, 
easily provable by induction on the number of 
the non-empty sets considered. See any relevant 
textbook. 

Vladimir Kanovei