[FOM] finite choice question

[A.P. Hazen]

Stephen Fenner writes:
>This is a basic question about ZF set theory.

...

>  is the following a theorem of ZF?
>
>"For any natural number n and any sequence <X1,...,Xn> of pairwise
>disjoint, nonempty sets, there is a set C such that (C intersect Xi) is a
>singleton for each i in {1,...,n}."
   Yes.  Lead quantifier is over natural numbers, so use mathematical 
induction (derivable in ZF).  Base case (every "sequence" of zero or 
one non-empty set(s)has an appropriate C)  trivial.  For induction, 
assume there is a C for every sequence, <x1,...,xn>, of n pairwise 
disjoint non-empty sets, and consider a sequence of n+1 such sets, 
<x1,...,xn,xn+1>.  By hypothesis of induction there is a choice-set C 
for the subsequence consisting of the first n sets.  So CU{y} for any 
y belonging to xn+1 will be a choice set for the whole sequence.
   Key thing, in making the proof possible, is that the finitude 
(inductiveness: having a natural number as cardinal) of the  sequence 
is explicitly STATED as part of the antecedent of the theorem.
   ((Something I don't know: In ZF without choice, can you prove the 
existence of a choice set for a Dedekind-finite [but in the absence 
of Choice not necessarily  inductive!] family of disjoint non-empty 
sets?  My guess would be NO, but i don't think I am a very good 
guesser.))
--
Allen Hazen
Philosophy Department
University of Melbourne