[FOM] What do you lose if you ditch Powerset?

[sambin@math.unipd.it]

Reply to: "Timothy Y. Chow" <tchow at alum.mit.edu>:

> Sorry if this is a dumb question with a well-known answer, but...
> 
> What sorts of theorems are lost if we delete from (say) ZFC the assumption
> that every infinite set has a powerset?
> 
> Perhaps more precisely, what sorts of theorems of "classical" mathematics
> are there that (1) do not, on the surface at least, require the existence
> of powersets of infinite sets for one to make sense of their statements,
> but (2) cannot be proved without the powerset axiom or something similar?

The answer, as far as I know, is not short: one just has to analyse case by case. What I know is that in the case of topology, it is quite possible to give definitions (and theorems, of course) which make no use of the powerset. The result is commonly called formal topology, and it is developed over a basic type theory. Understood, one cannot prove all theorems of classical topology, but surely eenough results to make it inteeresting.
Even more interesting is the fact that a predicative (= without powerset) development often requires a completely new understanding, and it may lead to new mathematics. This has been the case with what I calll the basic picture, a generalization of topology based on logical duality and symmetry.
More information can be found in the survey "Some points in formal topology" (by myself) recently appeared in Theoretical Computer Science (precisely, number 305 (2003), pp. 347-408) .

> This question was posed to me by a friend who is not a mathematician but
> enjoys mathematics and who has some constructivist intuitions.  Curiously,
> he does not seem to be too bothered by Infinity or Choice, but does not
> like the notion of an arbitrary set of integers or an arbitrary decimal
> expansion. 

 The paper mentioned above is meant for specialists in constructive topology, but perhaps your friend can enjoy the third part, on the general philosophical principles accompanying a fully constructive (which to my opinion includes predicative) development of mathematics.
Your friend is probably a type-theorist by natural inclination: in Martin-Loef's type theory, you have of course infinite sets but also choice, and if you add powerset, you fall into classical logic.
You can give him my e-mail address, if he wants more information.

Giovanni Sambin




-------------------------------------------------
Mail inviata da IMP WebMailClient 1.

Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova