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.
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.
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.
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.
I arrived at [Nelson believes PA has no models] 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.
Your reasoning is not quite valid. To reach that conclusion, you also need c) Nelson believes a). There is reason to think that he does not believe a) since that proof you cite assumes the consistency of ZF.
If ZF is inconsistent, then there is a proof in ZF that PA has no models. Nelson believes this!
It’s because Nelson doubts ZF that I didn’t bring up the converse implication: that if there is a proof in ZF that PA has no models, then PA is inconsistent.
If Nelson believes there is a proof in ZF that PA has no models, that doesn’t imply that Nelson believes that PA has no models. Obviously, Nelson will judge a ‘proof’ produced within an inconsistent system as an invalid proof.
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.
Ok, I can see now that, careful as we have been, there has been an ambiguity in our conversation regarding the meaning of the word “proof”. Two possible meanings:
a valid and convincing argument
a structure in a formal system which is equivalent to a valid and convincing argument (if one assumes the truth of the axioms and the validity of the rules in that formal system).
I have sometimes been using one of those meanings and sometimes the other.
I suspect the best thing to do with this conversation is to simply shut it down. But before doing so, I’d like to thank you for making this posting. I just recently stumbled upon Nelson’s work on “internal set theory” and non-standard analysis. Good stuff! I’m less impressed with ultrafinitism - I’m more of a intuitionist or constructivist—but it certainly is fascinating.
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.
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.
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.
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.
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.
Your reasoning is not quite valid. To reach that conclusion, you also need c) Nelson believes a). There is reason to think that he does not believe a) since that proof you cite assumes the consistency of ZF.
If ZF is inconsistent, then there is a proof in ZF that PA has no models. Nelson believes this!
It’s because Nelson doubts ZF that I didn’t bring up the converse implication: that if there is a proof in ZF that PA has no models, then PA is inconsistent.
If Nelson believes there is a proof in ZF that PA has no models, that doesn’t imply that Nelson believes that PA has no models. Obviously, Nelson will judge a ‘proof’ produced within an inconsistent system as an invalid proof.
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:
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
might appear dubious (but meaningful) to Nelson. That makes it a failure—I chose it as a formalist-friendly rewording of Yudkowsky’s statement
but no dice. I don’t know if there’s an “effective” version of this theorem whose semantic content formalists would endorse.
Ok, I can see now that, careful as we have been, there has been an ambiguity in our conversation regarding the meaning of the word “proof”. Two possible meanings:
a valid and convincing argument
a structure in a formal system which is equivalent to a valid and convincing argument (if one assumes the truth of the axioms and the validity of the rules in that formal system).
I have sometimes been using one of those meanings and sometimes the other.
I suspect the best thing to do with this conversation is to simply shut it down. But before doing so, I’d like to thank you for making this posting. I just recently stumbled upon Nelson’s work on “internal set theory” and non-standard analysis. Good stuff! I’m less impressed with ultrafinitism - I’m more of a intuitionist or constructivist—but it certainly is fascinating.
Nice.
Up to you, I’m having a great time.