[FOM] Excluded middle & cardinality of the reals

[jvoosten@math.uu.nl]

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