FOM: finite choice

Kanovei kanovei at
Sun Mar 1 12:49:21 EST 1998

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

<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 

Vladimir Kanovei

More information about the FOM mailing list