The power set of every infinite set is uncountable. An infinite set (as an element of the power set) cannot be defined by writing the infinite sequence of its elements but only by a finite formula. By lexical ordering of finite formulas we see that the set of finite formulas is countable. So it is impossible to define all elements of the uncountable power set. The power set axiom seems doubtful. Therefore my question.

8$\begingroup$ @Andy: I think you've misunderstood his question. There are only countably many formulas in the language of set theory, hence for any set $x$ there are only countably many subsets of $x$ which can be explicitly defined by a formula. $\endgroup$ – Nik Weaver Jun 13 '13 at 6:16

2$\begingroup$ @Andy: I think that is not a matter of belief, There is the axiom that all elements of the power set of, say, N exist. The first question is: Where do they exist. And the second question is: If someone does not accept the existence of elements that cannot be defined in our language, what can nevertheless be proved in mathematics in our language? $\endgroup$ – user34913 Jun 13 '13 at 6:22

6$\begingroup$ I'm not quite certain that this is what you're looking for, but there is a nice paper in the arXiv about models of ZFC (ZFC without the power set axiom) that can be found here: arxiv.org/abs/1110.2430 $\endgroup$ – Shehzad Ahmed Jun 13 '13 at 6:33

6$\begingroup$ I expect the explanation for this one will cover welltrodden philosophical ground, but it's not as naive as these comments make it sound, so I think it should not be closed. $\endgroup$ – Ryan Reich Jun 13 '13 at 9:15

2$\begingroup$ Regarding the claims about the existence of nondefinable sets, my answer at mathoverflow.net/questions/44102/… may show another perspective on the matter. $\endgroup$ – Joel David Hamkins Jun 13 '13 at 10:01
This is a real question.
You're not the only one who find the power set axiom dubious. At the time of the great foundational controversies, Russell and Weyl both expressed a similar view. It is now known, from work of Weyl, Wang, Feferman, the reverse mathematics school, and others, that the vast bulk of mainstream mathematics can be developed without power sets. You can effectively treat objects like $\mathcal{P}(\mathbb{N})$ and $\mathbb{R}$ as proper classes.
You might be interested in looking at my paper on "Mathematical conceptualism" at arxiv:math/0509246. Here's a direct link: http://arxiv.org/pdf/math/0509246.pdf

6$\begingroup$ The point can be made more strongly. Eliminating the power set axiom results in the loss of a vast realm of uncountable pathology, so that the result is a universe which provides a much better fit with actual mathematical practice. $\endgroup$ – Nik Weaver Jun 13 '13 at 6:34

2$\begingroup$ And how do we make you denounce excluded middle as well? ;) $\endgroup$ – Andrej Bauer Jun 13 '13 at 6:36

$\begingroup$ Thank you, Nik, I know your work very well. I also know some of Feferman, namely his "in the light of logic" where he says something about math without Cantor, but have not everything understood there. Here my question aims more to find concrete formulas or parts of math which will remain provable. (As soon as I will be able to do so, I will vote up your answer.) $\endgroup$ – user34913 Jun 13 '13 at 6:36

$\begingroup$ @Andrej: I think here are different things in question. Excluded middle can be dobted, if you like to do so. But it is without any doubt that it is impossible to define with finite amounts of bits all elements of a power set of an infinity set. So the last question seems at least more pressing than the first. $\endgroup$ – user34913 Jun 13 '13 at 6:41

$\begingroup$ @albino: you can find very concrete details in, e.g., my paper "Analysis in $J_2$" (arxiv.org/pdf/math/0509245.pdf) $\endgroup$ – Nik Weaver Jun 13 '13 at 6:45
Words are not magic. Just because you have given something a name it does not necessarily exist, and conversely, a thing may exist without having a name.
Let me explain this. You say that the powerset of an infinite set is questionable because it must have some undefinable elements. You are presuming that the subsets of a set must all be distinguishable by you, or some entity whose only access to powersets is through formal language. But why is such an assumption warranted? What makes you think that a thing does not exist unless you can define it? Is existence a personal belief?
Now, to answer your question about mathematics without powerset. This is sometimes called predicative mathematics. We can do practically all mathematics without the axiom of powerset. Of course, instead we postulate other constructions that allow us to generate infinite objects, but in a controlled way, such as inductive definitions.
A particular form of predicative mathematics is type theory. You may be interested to see what can be done in it. For example, have a look at the Coq standard libarary or the user contributions, these are formalizations of mathematics in type theory. And this stuff is written mostly by computer scientists. If mathematicians moved onto the proofassistant bandwagon, there would be much more.

4$\begingroup$ I gave you the mathematical answer as well, and it was you who laced the question with philosophy. You can do practically all of mathematics without powersets. Both notions of continuity work. $\endgroup$ – Andrej Bauer Jun 13 '13 at 6:59

3$\begingroup$ Also, you are confusing "distinguishable" with "distinguishable by a formula". $\endgroup$ – Andrej Bauer Jun 13 '13 at 7:00

3$\begingroup$ Words are not magic. You got that part right. So when mathematicians write down the power set axiom "There exist a set with such and such property", these words do not cause such a set to magically come into existence. $\endgroup$ – JHI Jun 13 '13 at 7:18

2$\begingroup$ @albino: the FeitThompson/OddOrder theorem would still hold, I believe  see the reasonably recent news about the formalisation of this in Coq. This is definitely real mathematics. $\endgroup$ – David Roberts Jun 13 '13 at 8:17

2$\begingroup$ @JHI: Indeed, and no selfrespecting logician would think so. Why exactly are you pointing this out, I do not understand what you are getting at. Can you be a bit more explicit? $\endgroup$ – Andrej Bauer Jun 13 '13 at 13:23
Several standard theories intensely studied by set theorists do not have the power set axiom.
One of these is the theory ZFC without the power set axiom, usually denoted $\text{ZFC}^$. One should take care with the proper axiomatization of this theory, as we discuss in What is the theory ZFC without the powerset?, V. Gitman, J.D. Hamkins, T. Johnstone; the main point being that one should use collection+separation and not just replacement, since these are no longer equivalent without the power set axiom.
Part of the attraction of $\text{ZFC}^$, which is much stronger than the theory KP discussed below, but still lacks power set, is an abundance of natural models, such as the following:
HC, the universe of hereditarily countable sets. This is the land of the countable, where everything is countable. The sets in HC are precisely those sets that are countable and have only countable members and membersofmembers and so on. Quite a bit of mathematics can be fruitfully undertaken in HC.
More generally, $H_{\kappa^+}$, the universe of sets of hereditarily size at most $\kappa$. This universe satisfies $\text{ZFC}^$, but can have some power sets, namely, as long as the power set has size at most $\kappa$. But meanwhile, there is a largest cardinal in this univese, $\kappa$ itself, and the powerset of $\kappa$ does not exist.
More generally, $H_\delta$ for any regular cardinal $\delta$. When $\delta$ is an inaccessible cardinal, this is the same as $V_\delta$, the rank initial segment of the universe in the von Neumann hierarchy, and in this case it is a model of ZFC and a Grothendieck universe.
These models and other models of $\text{ZFC}^$ are used in arguments throughout set theory, from iterated ultrapowers in large cardinals to their use in forcing axioms and elsewhere.
Another commonly studied theory without the power set axiom is KripkePlatek set theory KP, which is a very weak set theory at the heart of the subject known as admissible set theory, in which an enormous amount of classical mathematics can be undertaken. There are numerous natural models of KP, such as:
The hyperarithmetic universe $L_{\omega_1^{CK}}$, of sets that are coded by wellfounded hyperarithemtic relations on the natural numbers. This is the smallest admissible set, the smallest transitive model of KP. One interesting thing about this world is that every ordinal is not only hyperarithmetic, but actually computable.
There are many other admissible ordinals $\alpha$, ordinals for which $L_\alpha\models$KP.
One can relativize the admissibility concept to oracles $x$, forming $\omega_1^x$, the least admissible ordinal in $x$, so that $L_{\omega_1^x}[x]$ is the smallest model of KP containing $x$.
The universes $L_\lambda$ and $L_\zeta$ arising in the theory of infinite time Turing machines, where $L_\lambda$ is the collection of sets coded by a wellfounded infinitetime writable relation on $\omega$, and $L_\zeta$ are the sets coded by a wellfounded infinitetime eventually writable relation. These universes both satisfy natural strengthenings of KP, but not the power set axiom.
And there are numerous other set theories without the power set axioms, including various strengthenings of KP that still lack the power set axiom and have natural models that are used for various purposes.
All these models are intensely studied, and set theorists pay detailed attention to what is or is not possible to achieve in the models, depending on how strong it is. The crux of many arguments is whether the given model is strong enough to undertake a given settheoretic construction or not. For example, one will often pay attention to the details of a mathematical construction to find out if it can be performed using only $\Sigma_1$collection instead of, say, $\Sigma_2$collection, in order to know whether or not it can be performed inside one of these models.
Let me add that although set theorists are giving enormous attention to these set theories without the power axiom, the reason isn't usually because of doubt about the truth of the power set axiom, but rather it is just that they want to undertake certain constructions inside these natural models, and so they need to know whether these models are strong enough to undertake that construction or not.
So one can be interested in set theory without the power set axiom without having doubt about that axiom. We study set theories without power set, while retaining it in our main background theory, because we want to know what is possible to achieve without power sets in those models.
Lastly, concerning your remarks about definability, I refer you as I mentioned in the comments to an answer I wrote to a similar proposal, which I believe show that naive treatment of the concept of definability is ultimately flawed.

1$\begingroup$ The natural constructivist tendency is to remove the powerset and replace it with something less powerful, but more controlled, e.g., inductive definitions. Is there such a thing for classical set theory? $\endgroup$ – Andrej Bauer Jun 13 '13 at 13:40

1$\begingroup$ Well, there is an entire hierarchy of set theories, so take your pick. KP pulls in with $\Sigma_1$collection, but one can have more, such as $\Sigma_2$collection, $\Sigma_n$collection and so on, or much more, up to $\text{ZFC}^$, which is actually quite strong. The theory $\text{ZFC}^$ itself has natural strengthenings in a hierarchy, depending on how much power set you get lower down in the universeperhaps you can take two powers of $\mathbb{R}$, but no more, or perhaps you can take more, and so on. These various theories arise naturally in light of the natural models I mentioned. $\endgroup$ – Joel David Hamkins Jun 13 '13 at 13:53

2$\begingroup$ Albino, I'm not sure to which logicians you are referring with your first comment. Meanwhile, yes, your remarks on definability are the usual naive position on definability. If you ever find yourself inclined to mount a serious analysis of definability, however, then I would suggest that you talk more with logicians. In particular, I would point you toward the initial part of my paper on pointwise definable models of set theory (de.arxiv.org/abs/1105.4597), where we deal with the "Math Tea argument", which is essentially the argument you are advancing. $\endgroup$ – Joel David Hamkins Jun 13 '13 at 15:30

5$\begingroup$ Oh, I'm very sorry to hear that you aren't interested in logical proof or logical conclusions. I'll leave you alone, then, to undertake your own kind of proof activity. $\endgroup$ – Joel David Hamkins Jun 15 '13 at 0:54

2$\begingroup$ @Joel, now you get unjust. I do accept logical proof! I accept the logical proof that it is impossible to define more than countably many objects including all numbers. This stands as solid as the proof that with three digits you cannot define more than $9^{9^9}$ numbers. I even accept nonconstructive proofs like Zermelo's, but not as deciding whether something can be constructed  as was Zermelo original intention. (Compare Fraenkel who said that hitherto nobody could wellorder the reals.) To be short: If your proof is correct, then you have found a contradiction. $\endgroup$ – user34913 Jun 15 '13 at 7:07