Stronger versions of the Power Set Axiom? In this article on Skolem's Paradox, it gives the Power Set Axiom as an example where models may badly misinterpret the axioms (compared to the "intention" of the axiom). While originally I thought that the axiom guaranteed the presence of all subsets of a set, in fact it just seems to guarantee that there's a set containing whichever subsets happen to be present in a model.
My understanding is that because of the Löwenheim–Skolem theorem, we'll never be able to come up with an axiom which guarantees that a model will have e.g. all "actual" subsets of $\mathbb{N}$. It seems unfortunate that we can never get models to behave as we intend.
Are there other axioms which still do a better job than the Power Set Axiom at requiring models to contain subsets of each of their sets? What about when we consider other logical systems, or maybe allow proofs of infinite length?
 A: I think the question is based on a (common) misunderstanding of the purpose of the power set axiom. The role of this axiom is not to ensure that all subsets of a set $X$ exist. In fact, it says nothing at all about which or how many subsets $X$ has. All it says is that there is a set whose elements are exactly the subsets of $X$. That is, we can gather up all those sets which happen to be subsets of $X$ into a new set $\mathcal{P}(X)$.
It's the axiom schema of comprehension (or separation, or specification, as you prefer) that has the job of ensuring that a set $X$ has "lots" of subsets. The version of comprehension in ZFC says roughly that for any property $P(x)$ which is definable in the first-order language of set theory, we can form the subset $\{a\in X\mid P(a)\}$. You can get "more" subsets provably existing by strengthening the logic in which the property $P$ is expressed. But the cost of this is that your foundational set theory is no longer a first-order theory, and logics stronger than first-order tend to lack convenient properties (like nice sound and complete proof systems).
