# [FOM] finite choice question

Peter Schuster pschust at mathematik.uni-muenchen.de
Thu Nov 17 09:57:37 EST 2005

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

```