[FOM] Excluded middle & cardinality of the reals
jvoosten@math.uu.nl
jvoosten at math.uu.nl
Fri Jun 25 05:51:42 EDT 2004
There seems to be some confusion about this topic.
>
> However, it is compatible with constructive math (or at least, compatible
> with IZF) that every set has an injection into the natural numbers. See
>
> McCarty, Charles, Subcountability under realizability.
> Notre Dame J. Formal Logic 27 (1986), no. 2, 210--220.
>
This is wrong. Intuitionistically, there is no injective function from
P(N) into N. Proof:
Suppose F:P(N)\to N is such a function. Consider
A = {n in N | for all X in P(N) (n in X ==> n is not F(X))}
Let n=F(A). Clearly then, n is not in A from the definition
of A; on the other hand, if X in P(N) and n in X, then n=F(X)
implies X=A by injectivity of F, so n in A; contradiction.
So for all X with n in X, n is not F(X). So n in A all the
same; contradiction.
One can do this for every set instead of N.
Jaap van Oosten
More information about the FOM
mailing list