[FOM] finite choice question

[Peter Schuster]

Stephen Fenner asked whether the finite choice principle (FCP) 

>>"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}."

is a theorem of ZF, and Allen Hazen answered this question with "yes". 

In fact, FCP is equivalent to the law of excluded middle for restricted 
formulas (REM), where a formula of set theory is restricted (or bounded 
or Delta_0) whenever quantifiers occur in this formula - if at all - only 
as bounded by sets. The equivalence, moreover, holds over the elementary 
fragment CZF_0 of Constructive Zermelo-Fraenkel set theory (CZF), in 
which separation is restricted to restricted formulas. That FCP implies 
REM can easily be seen along the well-known arguments given in the 1970s 
by Goodman and Myhill, and by Diaconescu. For more details see 

P. Aczel, M. Rathjen, "Notes on Constructive Set Theory"

available via

http://www.ml.kva.se/preprints/meta/AczelMon_Sep_24_09_16_56.rdf.html



Peter Schuster
Mathematisches Institut
Universitaet Muenchen 





---


Stephen Fenner wrote: 

>>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}."

Allen Hazen then wrote: 

>Yes.  Lead quantifier is over natural numbers, so use mathematical 
>induction (derivable in ZF).  ...