But I said "Nelson believes there is a proof that PA has no models" and not "Nelson believes that PA has no models." With the amount of care we're speaking with now I think that Nelson does not regard the second assertion as meaningful.

Nelson will not judge a proof within an inconsistent system as an invalid proof. Nelson:

Mathematicians of widely divergent views on the foundations of mathematics can and do agree as to whether a purported proof is indeed a proof; it is just a matter of checking.

But in some sense it's worse than you say. Nelson does not believe that valid proofs in formal systems, consistent or not, entail anything about the real world, e.g. that there exists or does not exist a model. A trivial exception: he believes that, in the real world, a valid proof in a formal system can be used to produce another valid proof in a stronger formal system. Basically, that's the structure of "if PA is inconsistent, then there is a proof that PA has no models."

Edit: But this sentence of mine from upthread

If you can prove that a theory has no models, then you can prove a contradiction in a finite number of steps.

might appear dubious (but meaningful) to Nelson. That makes it a failure -- I chose it as a formalist-friendly rewording of Yudkowsky's statement

In first-order logic, every theory with no models syntactically proves a contradiction in a finite number of steps

but no dice. I don't know if there's an "effective" version of this theorem whose semantic content formalists would endorse.