[FOM] question about intuitionistic set theory

[jbell@uwo.ca]

I wonder if anyone could shed some light on the following question: is the 
existence of an injection of N^N into N (the set of natural numbers) 
consistent with intuitionistic set theory?  Diagonalization shows that there 
can't be a bijection, in fact that there can be no surjection of N onto N^N. 
But it is consistent with IST that there a subset U of N and a surjection 
from U to N^N since this holds in the effective topos. If N^N were 
injectible into N, then N^N would have to be decidable (and this does not 
hold in the effective topos) but I can't see that this in itself would yield 
enough excluded middle to make the existence of an injection of N^N into N 
impossible. But maybe I'm missing something obvious!

-- John Bell


Professor John L. Bell
Department of Philosophy
University of Western Ontario
London, Ontario N6A 3K7
Canada

http://publish.uwo.ca/%7Ejbell/