I don't know to what extent community norms around here allow me to make this request, but: can you guys start a new post on this topic, before my thoughtful and informative contribution turns into an area with 40 nice comments about Peano arithmetic and a thousand about Eliezer Yudkowsky?

Suggested title: "Remarks on a possibly arrogant comment made by Eliezer Yudkowsky."

Yeah, I got that you meant it that way. I was just referencing the fact that, on the surface level, declaring oneself practically infallible is not very self-deprecating at all.

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

No, if a first-order theory has no models, then you can prove a contradiction from it. Not, if it provably has no models. Just, if it has no models, period, then it proves a contradiction in a finite number of steps.

What I said is a true consequence of what you said, so why are you frustrated? I am trying to make statements that a formalist (such as Nelson) would endorse.

That... is a very strange combination of beliefs. I honestly cannot imagine what he could possibly be thinking.

Now you're confusing me. Induction does not follow from the other axioms, so one does not have to reject all of Peano arithmetic to reject induction. Why is it more stupid to reject only induction?

You might reply: because P(everything is wrong | induction is wrong) is large. (Though then you would be falling for the conjunction fallacy, which is something you would never do.) A lot of Nelson's work can be seen as arguing that it is not as large as you think.

Then what is it talking about?

It is very rare for someone speaking about numbers to be talking about a particular model of numbers inside a particular model of set theory. The very word "model" is chosen to contrast it with "the real thing."

Of course formalists reject the idea that there is a real thing.

I arrived at the declaration you quoted from the following: a) If PA is inconsistent, then there is a proof that PA has no models. b) Nelson believes that PA is inconsistent. I wouldn't have mentioned a), except that Yudkowsky seemed to think that model-theoretic considerations discredited Nelson. But a) is at least true. I have a weaker case for b) and am happy to qualify it: I can't think of a place where he has stated it explicitly.

In any case, it would seem that anyone denying the existence of a PA model would also have to deny the validity of the axiom of infinity in ZF. And if you allow Nelson to deny the axiom of infinity, then I would think that you have to accept his denial of an infinite PA model.

Let me try to untangle some different beliefs of Nelson. Note that I have never spoken to him, nor am I any kind of expert or professional, so you might take this with a grain of salt. But I don't think my interpretations of what he's written are strained.

1. Nelson is a formalist. He does not believe that syntactically correct and provable formulas of ZF, or of any other formal language, express facts about the real world. (I should probably weaken that to: he does not believe that every syntactically correct formula expresses a fact about the real world.) In particular he does not believe that the axiom of infinity expresses a fact about the real world.

2. More than that, he believes that the Zermelo-Frankel axioms are inconsistent, to the point that I have heard he has a wager with a colleague based on it. I don't have a reference for this wager, and concede that it might be a legend. I also don't know that he specifically thinks that the axiom of infinity will play a role in an inconsistency, but I think it's very likely.

3. He is skeptical of the consistency of PA. I don't know if he's wagered on it, and I don't know to what extent he believes that modern mathematicians are capable of finding a contradiction. All I really have are some suggestive quotations, e.g.

Godel’s second incompleteness theorem is that P [what we've been calling PA] cannot be proved consistent by means expressible in P, provided that P is consistent. This important proviso is often omitted. This theorem I take to be the second warning sign of trouble in contemporary mathematics. Its straightforward significance is this: perhaps P is inconsistent. But this is not how his profound result was received, due to the a priori conviction of just about everyone that P must be consistent.

Aren't you mixing up "having a model" in the sense of knowing and thinking about one, and having one in the sense of one existing?

You would have to tell me what you mean by "existing." There is a real (though often informal) distinction between constructive and non-constructive proofs, and this distinction exists in model theory also.