What would remain of current mathematics without axiom of power set? 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.
 A: 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
A: 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 members-of-members 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 Kripke-Platek 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 well-founded 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 well-founded infinite-time writable relation on $\omega$, and $L_\zeta$ are the sets coded by a well-founded infinite-time 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 set-theoretic 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. 
A: 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 proof-assistant bandwagon, there would be much more.
