That appears to be an axiom that probabilities go to zero enough faster than utilities that total utility converges (in a setting in which the sure outcomes are a countable set).
No, the axiom doesn't put any constraints on the probability distribution. It merely constrains preferences, specifically it says that preferences for infinite lotteries should be the 'limits' of the preference for finite lotteries. One can think of it as a slightly stronger version of the following:
Axiom (5'): Let L = Sum(i=0...infinity, p_i M_i) with Sum(i=0...infinity, p_i)=1. Then if for all i N>=M_I then N>=L. And similarly with the arrows reversed. (In other words if N is preferred over every element of a lottery then N is preferred over the lottery.)
In fact, I'm pretty sure that axiom (5') is strong enough, but I haven't worked out all the details.
It lacks something in precision of formulation (e.g. what is being quantified over, and in what order?)
Sorry, there were some formatting problems, hopefully it's better now.
(for which p_i M_i [formatting fixed] grows with busy beaver fastness)
The M_i's are lotteries that the agent has preferences over, not utility values. Thus it doesn't a priori make sense to talk about its growth rate.
I think I understand what the axiom is doing. I'm not sure it's strong enough, though. There is no guarantee that there is any N that is >= M_i for all i (or for all large enough i, a weaker version which I think is what is needed), nor an N that is <= them. But suppose there are such an upper Nu and a lower Nl, thus giving a continuous range between them of Np = p Nl + (1-p) Nu for all p in 0..1. There is no guarantee that the supremum of those p for which Np is a lower bound is equal to the infimum of those for which it is an upper bound. The axio...
Summary: the problem with Pascal's Mugging arguments is that, intuitively, some probabilities are just too small to care about. There might be a principled reason for ignoring some probabilities, namely that they violate an implicit assumption behind expected utility theory. This suggests a possible approach for formally defining a "probability small enough to ignore", though there's still a bit of arbitrariness in it.