Trying to download this paper, the connection timed out.
I just found that amusing, given the subject matter.
Anyway. I don’t see how you could possibly believe that axioms 1 through 4 are meaningful and axiom 5 is too infinite to be meaningful. If you deny infinity then you should deny that axioms 1 through 4 are together meaningful, because they only have infinite models. 5 just restricts that infinity to the smallest one, the intersection of all the models that match 1 through 4.
I don’t see how you could possibly believe that axioms 1 through 4 are meaningful and axiom 5 is too infinite to be meaningful.
Nelson does not believe that axiom 5 is any less meaningful than axioms 1-4. He believes that, granting axioms 1-4, axiom 5 is false.
If you deny infinity then you should deny that axioms 1 through 4 are together meaningful, because they only have infinite models.
Yes all models, in the sense of model theory, of axioms 1-4 are infinite. But why would you require a model of PA before regarding PA as meaningful? After all no one actually possesses such an infinite model, or any other infinite set.
Model theory is based on set theory. With a powerful enough set theory (including ZF) one can actually prove that arithmetic is consistent. Nelson believes that such strong forms of set theory are inconsistent.
5 just restricts that infinity to the smallest one, the intersection of all the models that match 1 through 4.
You’re mistaken. There exist nonstandard models of Peano arithmetic.
You’re mistaken. There exist nonstandard models of Peano arithmetic.
I? Mistaken? You should notice your confusion a little harder before postulating anything so improbable.
There are nonstandard models of Peano arithmetic when the induction axiom is a first-order axiom schema covering all first-order formulas. If you have a single second-order axiom over all predicates, as in the wording “all properties” above, then the model is unique, and can be proven unique in second-order logic.
If you have a single second-order axiom over all predicates, as in the wording “all properties” above, then the model is unique, and can be proven unique in second-order logic.
The model is unique within any given model of set theory, but isn’t there more than one model of set theory? Or, to ask the same question in different terms, isn’t there more than one second-order logic?
I guess it means that one can have a privileged platonic model for second-order logic, just like for natural numbers. The analogy would go, “If you believe in natural numbers, then you believe that there is only one notion of natural numbers”. There are other models, but this is the one you really want to think about (even if you don’t know what it is). Normatively objective, introspectively inaccessible. You just test consequences of formal theories against your intuition.
Seeing as Eliezer called himself an “infinite set atheist” before, I’d be surprised to see him subscribe to such strong platonism now—e.g. thinking that the continuum hypothesis has a definite truth value “out there somewhere”. So I guess he meant something else, but I can’t figure out what.
It is a theorem of second order Peano arithmetic that all models are uniquely isomorphic. Note that Eliezer does not say that he believes in second order logic, but only makes a conditional statement. The problem with second order logic is that it refers to the undefined term “property.” Properties are pretty close to sets, so if one believes that this term is sensible, one seems to believe in a preferred model of set theory. One could talk about second-order logic only relative to a first order theory of set theory, but then one only has a relative uniqueness statement.
Eliezer seems to have brought up second-order arithmetic not because he thinks it’s a good idea, but because he thinks Nelson is using it. In fact, Nelson is nervous about set theory, so he interprets induction not for arbitrary properties, but only for formulas of the language. Then induction becomes a first-order axiom scheme and Gödel says that there are many models.
Platonism refers to the inference system component of the human decision problem, while the notion of things being real refers to the outcome (reality) concept (defined with respect to this inference system). People could turn out being able to reason about infinite, but without the infinite being real (i.e. reality being infinite). Infinite could, for example, help to model uncertainty about the world.
“Uniqueness” of the natural numbers means that for any two models of the axioms, there is an isomorphism between them that preserves the successor function and identity of zero. “Uniqueness” for second order logic would be similar, though I am less familiar with the formalization, so I won’t list all the things the isomorphism should preserve.
“Uniqueness” of the natural numbers means that for any two models of the axioms, there is an isomorphism between them that preserves the successor function and identity of zero.
If you manage to find axioms that capture your intuitive notion. The idea is, even if induction fails, there is still a “unique” notion of natural numbers, it just isn’t adequately described using induction. When you are presented with a convincing argument for a given axiomatic definition not capturing your concept, you just find what assumptions led to the disagreement and change them to obtain a better description.
If you believe in second-order logic then you believe there’s only one second-order logic.
I’m not sure whether to interpret that as a novel form of other-optimization, or as an ironic take on the idea that if one believes in arithmetic ( or set theory, for that matter) one also believes that the subject matter is unique.
In any case, my personal favorite higher order logic is the internal language of the free topos, which is, in fact, unique up to isomorphism. But far from universally accepted.
I? Mistaken? You should notice your confusion a little harder before postulating anything so improbable.
I’m not sure how to interpret this. Do you intend this to be taken together with a wink of an eye? Or are you making a serious claim that the probability that you’re mistaken in any given instance is very low?
I didn’t read it as joking (more as a form of “Ha ha only serious”), so we should probably update our probabilities …
I know that if I was disagreeing with Eliezer over maths, I would think twice before deciding he’s mistaken, though I haven’t followed enough of the details of this case to tell who is right and who is wrong (it’s a case of “Was Eliezer justified in thinking that Sewing-Machine was not justified in thinking that Eliezer was mistaken”).
That doesn’t mean I think Eliezer is always right, but rather that I think misunderstanding and subtle differences in use of terminology are more likely explanations.
I didn’t read that line as having a strong connection to the rest of the conversation; it seemed like a (self-deprecating) one-liner preceding something more serious. I usually assume that Eliezer isn’t being self-aggrandizing, due to e.g. this comment.
I’m definitely in the same boat as you are when it comes to the prospect of disagreeing with Eliezer about math.
Hold on, I’m confused. Self-deprecation is criticism of oneself and self-deprecating humor involves making jokes at one’s own expense. Eliezer was exaggerating his opinion of himself as a way of poking fun at the very high esteem that some people hold him in, a state of affairs with which he is at the very least uncomfortable. Does it not make sense to say that he was making a self-deprecating joke about his reputation?
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.
I haven’t unpacked your new claim but your old claim is still mistaken. There is a model of axioms 1-5 that is not the intersection of all models of axioms 1-4.
There are models of axioms 1-5 that are not the intersection of all models of axioms 1-4.
In second-order logic I believe your statement above to be simply false. It’s false just for using the plural “models”; there is only one model of the second-order axioms 1-5.
Do you claim your statement is true in second-order logic?
I see. Yes inside a given model of ZFC, or maybe just ZF, there is only one model of second-order Peano arithmetic. There are many models of first-order Peano arithmetic.
I wasn’t careful about the distinction between first- and second-order in my post, but Nelson is in his article. For instance his axioms have rules for addition and multiplication built in.
I’ll repeat my question, which was not rhetorical: why would you require a model of PA before regarding PA as meaningful?
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.
Trying to download this paper, the connection timed out.
I just found that amusing, given the subject matter.
Anyway. I don’t see how you could possibly believe that axioms 1 through 4 are meaningful and axiom 5 is too infinite to be meaningful. If you deny infinity then you should deny that axioms 1 through 4 are together meaningful, because they only have infinite models. 5 just restricts that infinity to the smallest one, the intersection of all the models that match 1 through 4.
Try the new link.
Nelson does not believe that axiom 5 is any less meaningful than axioms 1-4. He believes that, granting axioms 1-4, axiom 5 is false.
Yes all models, in the sense of model theory, of axioms 1-4 are infinite. But why would you require a model of PA before regarding PA as meaningful? After all no one actually possesses such an infinite model, or any other infinite set.
Model theory is based on set theory. With a powerful enough set theory (including ZF) one can actually prove that arithmetic is consistent. Nelson believes that such strong forms of set theory are inconsistent.
You’re mistaken. There exist nonstandard models of Peano arithmetic.
I? Mistaken? You should notice your confusion a little harder before postulating anything so improbable.
There are nonstandard models of Peano arithmetic when the induction axiom is a first-order axiom schema covering all first-order formulas. If you have a single second-order axiom over all predicates, as in the wording “all properties” above, then the model is unique, and can be proven unique in second-order logic.
The model is unique within any given model of set theory, but isn’t there more than one model of set theory? Or, to ask the same question in different terms, isn’t there more than one second-order logic?
If you believe in second-order logic then you believe there’s only one second-order logic.
I don’t understand this statement, please explain.
I guess it means that one can have a privileged platonic model for second-order logic, just like for natural numbers. The analogy would go, “If you believe in natural numbers, then you believe that there is only one notion of natural numbers”. There are other models, but this is the one you really want to think about (even if you don’t know what it is). Normatively objective, introspectively inaccessible. You just test consequences of formal theories against your intuition.
Seeing as Eliezer called himself an “infinite set atheist” before, I’d be surprised to see him subscribe to such strong platonism now—e.g. thinking that the continuum hypothesis has a definite truth value “out there somewhere”. So I guess he meant something else, but I can’t figure out what.
It is a theorem of second order Peano arithmetic that all models are uniquely isomorphic. Note that Eliezer does not say that he believes in second order logic, but only makes a conditional statement. The problem with second order logic is that it refers to the undefined term “property.” Properties are pretty close to sets, so if one believes that this term is sensible, one seems to believe in a preferred model of set theory. One could talk about second-order logic only relative to a first order theory of set theory, but then one only has a relative uniqueness statement.
Eliezer seems to have brought up second-order arithmetic not because he thinks it’s a good idea, but because he thinks Nelson is using it. In fact, Nelson is nervous about set theory, so he interprets induction not for arbitrary properties, but only for formulas of the language. Then induction becomes a first-order axiom scheme and Gödel says that there are many models.
Um, of course I know all that.
If that’s really all there is to Eliezer’s statement, then okay. I was hoping there’d be something more, something new to me...
Platonism refers to the inference system component of the human decision problem, while the notion of things being real refers to the outcome (reality) concept (defined with respect to this inference system). People could turn out being able to reason about infinite, but without the infinite being real (i.e. reality being infinite). Infinite could, for example, help to model uncertainty about the world.
“Uniqueness” of the natural numbers means that for any two models of the axioms, there is an isomorphism between them that preserves the successor function and identity of zero. “Uniqueness” for second order logic would be similar, though I am less familiar with the formalization, so I won’t list all the things the isomorphism should preserve.
If you manage to find axioms that capture your intuitive notion. The idea is, even if induction fails, there is still a “unique” notion of natural numbers, it just isn’t adequately described using induction. When you are presented with a convincing argument for a given axiomatic definition not capturing your concept, you just find what assumptions led to the disagreement and change them to obtain a better description.
I’m not sure whether to interpret that as a novel form of other-optimization, or as an ironic take on the idea that if one believes in arithmetic ( or set theory, for that matter) one also believes that the subject matter is unique.
In any case, my personal favorite higher order logic is the internal language of the free topos, which is, in fact, unique up to isomorphism. But far from universally accepted.
That doesn’t even have a model of PA in it!
I’m not sure how to interpret this. Do you intend this to be taken together with a wink of an eye? Or are you making a serious claim that the probability that you’re mistaken in any given instance is very low?
He’s joking, p > .99
I didn’t read it as joking (more as a form of “Ha ha only serious”), so we should probably update our probabilities …
I know that if I was disagreeing with Eliezer over maths, I would think twice before deciding he’s mistaken, though I haven’t followed enough of the details of this case to tell who is right and who is wrong (it’s a case of “Was Eliezer justified in thinking that Sewing-Machine was not justified in thinking that Eliezer was mistaken”).
That doesn’t mean I think Eliezer is always right, but rather that I think misunderstanding and subtle differences in use of terminology are more likely explanations.
I didn’t read that line as having a strong connection to the rest of the conversation; it seemed like a (self-deprecating) one-liner preceding something more serious. I usually assume that Eliezer isn’t being self-aggrandizing, due to e.g. this comment.
I’m definitely in the same boat as you are when it comes to the prospect of disagreeing with Eliezer about math.
That word, “self-deprecating” — I do not think it means what you think it means. ;)
(But, more seriously: no, I think I do know what you mean.)
Hold on, I’m confused. Self-deprecation is criticism of oneself and self-deprecating humor involves making jokes at one’s own expense. Eliezer was exaggerating his opinion of himself as a way of poking fun at the very high esteem that some people hold him in, a state of affairs with which he is at the very least uncomfortable. Does it not make sense to say that he was making a self-deprecating joke about his reputation?
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.”
My thoughts on the matter are thoroughly exhausted, so you have nothing further to fear from me in this regard.
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.
I haven’t unpacked your new claim but your old claim is still mistaken. There is a model of axioms 1-5 that is not the intersection of all models of axioms 1-4.
In second-order logic I believe your statement above to be simply false. It’s false just for using the plural “models”; there is only one model of the second-order axioms 1-5.
Do you claim your statement is true in second-order logic?
I see. Yes inside a given model of ZFC, or maybe just ZF, there is only one model of second-order Peano arithmetic. There are many models of first-order Peano arithmetic.
I wasn’t careful about the distinction between first- and second-order in my post, but Nelson is in his article. For instance his axioms have rules for addition and multiplication built in.
I’ll repeat my question, which was not rhetorical: why would you require a model of PA before regarding PA as meaningful?
Theories with no models are not talking about anything, and semantically imply all consequences.
In first-order logic, every theory with no models syntactically proves a contradiction in a finite number of steps.
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.
You are using strong theories to reason about Peano arithmetic. If Nelson doubts the consistency of PA, he’s not going to buy your argument.