[FOM] question about intuitionistic set theory corr. to my prev
T.Forster at dpmms.cam.ac.uk
Tue Mar 9 03:50:23 EST 2010
I think Aczel's point was that you can't do this for arbitrary X, since X
might not have two distinct inhabitants. For the naturals it might work,
since constructive naturals are all distinct.
On Mon, 8 Mar 2010, jbell at uwo.ca wrote:
> 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
> FOM mailing list
> FOM at cs.nyu.edu
URL: www.dpmms.cam.ac.uk/~tf; DPMMS ph: +44-1223-337981;
UEA ph: +44-1603-593588 mobile in UK +44-7887-701-562;
(Currently in the UK but mobile in NZ +64-210580093.
Canterbury office fone: +64-3-3642987 x 8152)
More information about the FOM