Yes, the description of true arithmetic is a bit realist; I'm not particularly sold on the realism of true arithmetic, and yes, it's mostly meant to illustrate a way of thinking about logical uncertainty. Basically, the question of logical uncertainty gets more interesting when you try to say "I have one particular model of PA in mind, but I can't compute which one; what should my prior be?"

Typo fixed; thanks.

The entire algorithm for assigning logical probability is, I think, the thing whose limit should be checked for the desiderata for uncomputable priors.

I agree.

I don't think one can usefully talk about the properties of a (actually computed) prior alone in the limit of large resources.

I see these desiderata more as a litmus test. I expect the approximation algorithm and the prior it's approximating will have to be developed hand-in-hand; these desiderata provide good litmus tests for whether an idea is worth looking into. I tend to think about the problem by looking for desirable limits with approximation in mind, but I agree that you could also attack the problem from the other direction.