[FOM] Excluded middle & cardinality of the reals

[Matthew Frank]

About Michael Carroll's post:

One can prove constructively, without the principle of excluded
middle, that the reals are not in 1-1 correspondence with the integers.
This is an exercise in ch 1 of Bishop and Bridges's Constructive
Analysis.

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.

--Matt