[FOM] Excluded middle & cardinality of the reals

[Keith Brian Johnson]

I have two questions about the post quoted below:

(a) What is IZF?

(b) Perhaps the answer to (a) will render (b) null and void, but...how
is it possible to prove that the reals are not in 1-1 correspondence
with the integers (and hence that there is no bijection between the
reals and the natural numbers) but for there to be an injection--and,
hence, a bijection--from the reals to the natural numbers?

Keith Brian Johnson

--- Matthew Frank <mfrank at math.uchicago.edu> wrote:
> 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.



	
		
__________________________________
Do you Yahoo!?
New and Improved Yahoo! Mail - 100MB free storage!
http://promotions.yahoo.com/new_mail