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.
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.