Would it be possible to give a high level explanation of what is going on to give Hrbacek's Paradox (and why it is called a Paradox)?
"No infinite internal set X can be well ordered nor does it have a power set. Moreover, there is no set P containing all sets Y $\subset$ X of standard size?
(Internally presumably the power set and well orderings exist, so this looks like something is going on in the external Metatheory?).
The following is a bit informal, but I think explains what's going on decently well. Basically, Hrbacek's "paradox" is just overspill phrased in a complicated way (see the end of this answer for some discussion of this).
Let $T$ be an "appropriate" theory of nonstandard analysis. Working in $T$, we have an "internal universe" $\mathbb{I}$ and a "standard universe" $\mathbb{S}$. The first observation to make is that each of these construed on its own is a model of ZFC, and in particular AC and Powerset.
Nonetheless, Hrbacek's paradox says that in some sense both AC and Powerset "break" in $\mathbb{I}$. So, what gives?
The key is:
Let's look at Powerset. If $X\in\mathbb{I}$ then there is some $Y\in\mathbb{I}$ which $\mathbb{I}\models$ "$Y$ is the powerset of $X$." This $Y$ consists exactly of the subsets of $X$ which are in $\mathbb{I}$. But those aren't all the subsets there are! For example, take $X={}^*\mathbb{N}$. Then $\mathbb{N}\subseteq{}^*\mathbb{N}$ but $\mathbb{N}\not\in \mathbb{I}$ (this is just overspill). Indeed, this can't be avoided: if $X\in\mathbb{I}$ then either $X$ is (truly) finite or there are subsets of $X$ not in $\mathbb{I}$.
The same thing happens re: AC. If $\trianglelefteq$ is a linear ordering of some (truly) infinite $X\in\mathbb{I}$ then there is some $Y\subseteq X$ with no $\trianglelefteq$-least element, but we don't necessarily have such a $Y$ in $\mathbb{I}$: just because $\mathbb{I}$ thinks something is a well-ordering doesn't mean that it is, and in fact - as with Powerset - $\mathbb{I}$ will never correctly think that something is a well-ordering (excepting the trivial case where it's finite).
So that's Hrbacek's "paradox" (I personally think that's a bit strong language). Basically, $\mathbb{I}$ doesn't just have "extra" stuff, it also has "missing" stuff - if it didn't, other things we want would break - and this means that $\mathbb{I}$ satisfies some of the ZFC "in the wrong way."
Actually, though, I think this whole language is complicating things unnecessarily. Really, we're making a basic observation about nonstandard models of set theory, which I think is clearer since it has less "ontological baggage."
Even more generally, we have: