[FOM] A choice principle in Quine-Jensen set theory

[Ali Enayat]

Back in April, in an FOM posting, I posed the following question,
(inspired by a question of Linnebo).

>Let NFU be Jensen's urelement-version of Quine's NF. Does the
>axiom of choice (which for NFU is equivalent to global choice, since
>NFU has a universal set) follow from NFU plus the assumption "given
>any two sets A and B, there is either an injection of A to B or
>vice-versa" using an appropriate implementation of Hartogs' theorem?

Greg Kirmayer has kindly provided the following positive answer:

>Let  P(2,B) be the power set of the power set of B. Define P(n,A)
>by P1(0,A) is A and P1(m+1,A) is the one element subsets of P1(m,A) for
>m<4. Denote the the Cartesian product of A and B by AXB where we are using
>Kuratowski pairs.

>In NFU Hartogs' theorem can be expressed in the form there is a well-ordering
>of a subset of  P(2,AXA) which excedes in length any well-ordering of P1(4,A).

>If given any two sets  A and B, there must be an injection from one to the other,
>then for any set A  there must be a well-ordering of P1(4,A). This is equivalent to
>there being a well-ordering of A.

Regards,

Ali Enayat