[FOM] question about intuitionistic set theory corr. to my prev

[Thomas Forster]

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.
  sorry
    tf



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
> Canada
>
> http://publish.uwo.ca/%7Ejbell/
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>


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)