[FOM] P(N) and the reals (was Re: Question for Nik Weaver)

[Bas Spitters]

On Thursday 23 February 2006 10:11, Andrej Bauer wrote:
> On Thursday 23 February 2006 06:01, Bill Taylor wrote:
> > Nik, you made this comment in an article yesterday...
> >
> > > it is possible to treat things like
> > > the real line and the power set of N essentially as proper classes
> >
> > Presumably this apposition implies that you do NOT think of P(N) and R
> > as being essentially isomorphic? (OC one should remove the finite sets
> > from P(N) to do this most conveniently.)
>
> For examples of such treatments see Formal Topology (a predicative and
> constructive treatment of topology)

Dear Andrej,

I am glad to see that you are interested in formal topology!
However, IMO this is better explained in terms of constructive set theory (or 
type theory). 
First we should remark that constructively there is a difference between P(N) 
and 2^N, the latter one correspond to the decidable subsets. To construct the 
reals one does not need a very strong system. 
 However, adding powersets usually blows-up the proof-theoretical strength.
[I'll be a little imprecise.]

Suppose that we have an exponentiation axiom in our set theory (which is 
usually assumed). Then P(A)=P(1)^A. So we can restrict our attention to the 
class P(1), 1 denoting a one-element set. 
P(1) is usually called Omega, the subobject classifier, in topos theory and
Prop, the type of Propositions, in type theory.

Suppose that P(1) is a set, as opposed to a proper class, and suppose that we 
have the propositions-as-types interpretation (i.e. Prop=Set). Then we would 
have a set of all sets. We all know that we should be careful with this.
[However, see Jesper Carlstrom's discussion of a set of all sets in 
Martin-L"of type theory:
http://www.math.su.se/~jesper/research/setofsets/]
So, this indicates that we should be careful with the powerset axiom.

The proof-theoretical strength of IZF, intuitionistic ZF,  is much bigger than 
that of CST, constructive set theory. IZF is CST plus the powerset axiom.
See 
http://www.ml.kva.se/preprints/meta/AczelMon_Sep_24_09_16_56.rdf.html
Notes on Constructive Set Theory, by Peter Aczel and Michael Rathjen 
for a survey.


These issues are currently very active. There is a quest of a good theory of 
"predicative topoi", i.e. topoi without a power-set construction.

Best,

Bas