If you can prove that a theory has no models, then you can prove a contradiction in a finite number of steps. It’s interesting to contemplate the minimum number of steps—these are busy-beaver type numbers.
In the language of model theory, Nelson believes that one can prove that Peano arithmetic has no models. He does not believe one can prove that Peano arithmetic minus induction has no models.
But we do not have to have a model, or even to know any model theory, to “talk about something.”
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.
In the language of model theory, Nelson believes that one can prove that Peano arithmetic has no models. He does not believe one can prove that Peano arithmetic minus induction has no models.
That… is a very strange combination of beliefs. I honestly cannot imagine what he could possibly be thinking. It’s like someone sat around thinking, “Hm, what could I come up with that would be even dumber than believing PA to be inconsistent?” Indeed, I notice my own confusion and suspect that you may have misunderstood something that was stupid but not quite that stupid.
But we do not have to have a model, or even to know any model theory, to “talk about something.”
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.
In the language of model theory, Nelson believes that one can prove that Peano arithmetic has no models.
Are you sure about that? I didn’t see that in the Nelson paper linked in the OP. Could you provide a link or point to where he says that in the paper?
All I saw was the apparent claim that one can consistently believe there are no models. Maybe he was also saying that one ought to believe there are no models. But I’m pretty sure he was not claiming that there is a finite proof from axioms that models don’t exist.
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.
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.
But we do not have to have a model, or even to know any model theory, to “talk about something.”
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? An untutored person may have no real opinion on the relationship between his words and reality, but one nevertheless exists.
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.
If you can prove that a theory has no models, then you can prove a contradiction in a finite number of steps. It’s interesting to contemplate the minimum number of steps—these are busy-beaver type numbers.
In the language of model theory, Nelson believes that one can prove that Peano arithmetic has no models. He does not believe one can prove that Peano arithmetic minus induction has no models.
But we do not have to have a model, or even to know any model theory, to “talk about something.”
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.
That… is a very strange combination of beliefs. I honestly cannot imagine what he could possibly be thinking. It’s like someone sat around thinking, “Hm, what could I come up with that would be even dumber than believing PA to be inconsistent?” Indeed, I notice my own confusion and suspect that you may have misunderstood something that was stupid but not quite that stupid.
Then what is it talking about?
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.
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.
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.
Are you sure about that? I didn’t see that in the Nelson paper linked in the OP. Could you provide a link or point to where he says that in the paper?
All I saw was the apparent claim that one can consistently believe there are no models. Maybe he was also saying that one ought to believe there are no models. But I’m pretty sure he was not claiming that there is a finite proof from axioms that models don’t exist.
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.
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.
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? An untutored person may have no real opinion on the relationship between his words and reality, but one nevertheless exists.
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.