Exponentiation goes wrong first
The great Catholic mathematician Edward Nelson does not believe in completed infinity, and does not believe that arithmetic is likely to be consistent. These beliefs are partly motivated by his faith: he says arithmetic is a human invention, and compares believing (too strongly) in its consistency to idolatry. He also has many sound mathematical insights in this direction—I’ll summarize one of them here.
http://www.mediafire.com/file/z3detbt6int7a56/warn.pdf
Nelson’s arguments flow from the idea that, contra Kronecker, numbers are man-made. He therefore does not expect inconsistencies to have consequences that play out in natural or divine processes. For instance, he does not expect you to be able to count the dollars in a stack of 100 dollars and arrive at 99 dollars. But it’s been known for a long time that if one can prove any contradiction, then one can also prove that a stack of 100 dollars has no more than 99 dollars in it. The way he resolves this is interesting.
The Peano axioms for the natural numbers are these:
1. Zero is a number
2. The successor of any number is a number
3. Zero is not the successor of any number
4. Two different numbers have two different successors
5. If a given property holds for zero, and if it holds for the succesor of x whenever it holds for x, then it holds for all numbers.
Nelson rejects the fifth axiom, induction. It’s the most complicated of the axioms, but it has another thing going against it: it is the only one that seems like a claim that could be either true or false. The first four axioms read like someone explaining the rules of a game, like how the pieces in chess move. Induction is more similar to the fact that the bishop in chess can only move on half the squares—this is a theorem about chess, not one of the rules. Nelson believes that the fifth axiom needs to be, and cannot be, supported.
A common way to support induction is via the monologue: “It’s true for zero. Since it’s true for zero it’s true for one. Since it’s true for one it’s true for two. Continuing like this we can show that it’s true for one hundred and for one hundred thousand and for every natural number.” It’s hard to imagine actually going through this proof for very large numbers—this is Nelson’s objection.
What is arithmetic like if we reject induction? First, we may make a distinction between numbers we can actually count to (call them counting numbers) and numbers that we can’t. Formally we define counting numbers as follows: 0 is a counting number, and if x is a counting number then so is its successor. We could use the induction axiom to establish that every number is a counting number, but without it we cannot.
A small example of a number so large we might not be able to count that high is the sum of two counting numbers. In fact without induction we cannot establish that x+y is a counting number from the facts that x and y are counting numbers. So we cut out a smaller class of numbers called additionable numbers: x is additionable if x + y is a counting number whenever y is a counting number. We can prove theorems about additionable numbers: for instance every additionable number is a counting number, the successor of an additionable number is additionable, and in fact the sum of two additionable numbers is an additionable number.
If we grant the induction axiom, these theorems lose their interest: every number is a counting number and an additionable number. Paraphrasing Nelson: the significance of these theorems is that addition is unproblematic even if we are skeptical of induction.
We can go further. It cannot be proved that the product of two additionable numbers is additionable. We therefore introduce the smaller class of multiplicable numbers. If whenever y is an additionable number x.y is also additionable, then we say that x is a multiplicable number. It can be proved that the sum and product of any two multiplicable numbers is multiplicable. Nelson closes the article I linked to:
The proof of the last theorem [that the product of two multiplicable numbers is multiplicable] uses the associativity of multiplication. The significance of all this is that addition and multiplication are unproblematic. We have defined a new notion, that of a multiplicable number, that is stronger than the notion of counting number, and proved that multiplicable numbers not only have successors that are multiplicable numbers, and hence counting numbers, but that the same is true for sums and products of multiplicable numbers. For any specific numeral SSS. . . 0 we can quickly prove that it is a multiplicable number.
But now we come to a halt. If we attempt to define “exponentiable number” in the same spirit, we are unable to prove that if x and y are exponentiable numbers then so is x ↑y. There is a radical difference between addition and multiplication on the one hand and exponentiation, superexponentiation [what is commonly denoted ^^ here], and so forth, on the other hand. The obstacle is that exponentiation is not associative; for example, (2↑2)↑3 = 4↑3 = 64 whereas 2↑(2↑3) = 2↑8 = 256. For any specific numeral SSS...0 we can indeed prove that it is an exponentiable number, but we cannot prove that the world of exponentiable numbers is closed under exponentiation. And superexponentiation leads us entirely away from the world of counting numbers.
The belief that exponentiation, superexponentiation, and so forth, applied to numerals yield numerals is just that—a belief.
I’ve omitted his final sentence.
FYI, I went ahead and checked this by hand. It turns out that the natural numbers stop at 67*10^11288764. Once you get there you have to go back the way you came.
Oh, good, I can stop torturing this guy then.
Actually, for moderately large numbers it’s easy:
“Since it’s true for numbers one higher than numbers it’s true for, it’s true for numbers two higher than numbers it’s true for.” ”....two....four....” ”....four....eight...” ”....eight....sixteen...”
Of course, if that’s not fast enough you can try:
“Since it’s true for gaps double the size of gaps it’s true for, it’s true for gaps quadruple the size it’s true for” ”...quadruple… sixteen times...” ”...sixteen times...256 times...”
So, we’ve gone from N repetitions proving it for numbers up to N, to N repititions proving it for numbers up to 2^N, to N repititions proving it for numbers up to 2^(2^N). And we could continue.
Very nice. It’s interesting to think about how hard it would be to prove the proposition “3^^^3 is a counting number” using your trick but not using induction.
You’d have to meta my trick (apply it to itself) at least once. Probably several times.
ponders
Let’s go with 4s instead of 2s.
“Since it’s true for gaps of one, and 1+1+1+1 equals four, it’s true for gaps of four” ”....4....16....” ”....16....64...” So that’s 4^N
“Since it’s true for gaps 4 times larger than it’s true for, it’s true for gaps 444*4=256 times larger” ”...256...4 294 967 296...” so that’s 4^(4^N)
“Since it’s true for gaps the fourth power of gaps it’s true for, it’s true for the 256th power of gaps it’s true for” ”...256th power....4 294 967 296th power...”
That’s 4^(4^(4^N), or 4^^4 if N=4.
But I’m really struggling to get from that to 4^^^4
A side note of possible interest. Under ZF, as well as ZFC, one can actually prove that induction works, via Tarski’s fixed point theorem. Thus, if you think that induction seems a little weird as an axiom,, but set theory is cool, you still get to use induction.
It’s always the fifth postulate...
I just realized Nelson numbers them differently, building in + and x at the start and giving two axioms explaining how they work. Induction is number 7 on his list. I hope this doesn’t create confusion; I think it would create more if I changed the OP.
Huh, I didn’t know Wikipedia has SSL. Thanks. (The day may come when looking up Unpopular_Person_or_Event, even on WP, ends me up on some Interpol watchlist.)
HTTPS Everywhere is a Firefox extension that automatically loads the HTTPS version of several websites, including Wikipedia and Google.
A lot of things are trivially and obviously true on arbitrarily large but finite domains. People tend to assume that it will naturally transfer to countable domains. It doesn’t look that different. But very often it breaks there.
On finite domains, everything is trivially decidable. On infinite domains, nearly everything is undecidable.
It doesn’t feel like “does Riemann hypothesis have a proof in less than 1TB” and “does Riemann hypothesis have a proof” are entirely different categories of statements. The first must be true or false. We don’t know, but the truth exists. Just ask a perfect Bayesian.
Drop the space requirement, and now you have to deal with some theorems being true but unprovable. There’s this third emergent state between provably true and provably false. Everyone has their pet way of dealing with it, usually involving a lot of handwaving and then pretending nothing changed. For example—perfect Bayesians are no longer possible. There is just no self-consistent assignment of probabilities possible.
You can handwave some deeper notion of “truth” beyond computability without much clue how it would work like so many, or you can insist uncomputable things don’t exist like intuitionists, or even just say huge numbers don’t exist.
It all sucks one way or the other.
Rather just ask a tree searching algorithm running on a fast machine, in this case.
Really? Do you have an example? I’d be interested in seeing one.
(What do you mean here by “self-consistent”?)
Making this statement more precise is difficult. To make things easy I’m going to assume that probabilities live between 0 and 1 and that our general system of axioms is first order R with first order Q.
Now, our probability assignments are consistent iff they don’t lead to a contradiction. So, assign our probabilities, then whatever you do, I note that by Robinson’s theorems, I can describe PA using our axioms (this isn’t precisely true but is close enough to be true for our purposes.) I then invoke the contradiction we have in PA. No matter what initial probability assignment you choose I can do this.
Note that this argument might not work if we just have first order reals as our axiomatic system because that’s not sufficient to define PA in R, assuming that PA is consistent (to see this note that we have a decision procedure for first order reals and so if we could we’d have a way of deciding claims in PA.). I don’t think there’s any way to import contradictions in PA into first order R and I suspect this can’t be done in general. (I suspect that I’m missing some technical details here so take this with a handful of salt.)
There are formal systems that can’t construct exponentiation but still have weak versions of induction. in mainstream language, they have proof-theoretic ordinal ω^2. That exponentiation leads to proof theoretic ordinal ω^3 gives a precise way of saying that this is a natural place to stop. Ultrafinitists like Nelson appear to want something even more restrictive, but they refuse to talk in this language, so it’s hard to tell. I don’t blame them for wanting their own axiomatization, but their failure to even mention these systems makes me suspicious of them. Here is a Math Overflow discussion of ultrafinitist foundations.
The Buss axiom mentioned on Math Overflow is very cool.
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.
As a quick heuristic, Edward Nelson has done some very impressive stuff. But a) his investigation into this question is by his own account motivated by pre-existing beliefs and b) he was 84 at the time he wrote this essay. The two of those don’t give me a great amount of confidence in the likelyhood that this is correct.
As a more direct issue, saying that induction doesn’t hold in general is akin to saying that I can have an infinite chain of dominoes such that each one will cause the next to fall if it falls over, and that the first has fallen, but all the dominoes won’t eventually fall. That’s an essentially physical representation of induction. If that’s not valid then things are very weird.
The mathematics he is summarizing is utterly correct. Actually the small things I singled out I think are due to Godel and not to Nelson. But my summary is much more likely to have errors.
The dominoes analogy is revealing. If you lay out one million actual dominoes as usual and push over the first one I think it’s very unlikely that the millionth one will fall.
Yes, the basic math is correct. That’s not the point. Nelson’s objection is to say that the axiom of induction is not supported in the same way as the others. That’s not a math issue, that’s an issue of what intuition and evidence tell us. In that sense, the evidence is overwhelming that induction is fine. Almost anyone who thinks for even a short period of time will be ok with it, unless, like Nelson, they have an external motive to be uncomfortable with it.
Incidentally, if one started with the assumption that PA has a contradiction, and asked me given that assumption who would I think is most likely to find the contradiction, Nelson would be very high up on the list simply given his work in foundations. The fact that he has a special motive to find such and still hasn’t found it is additional evidence that the system is really consistent.
The only real upshot of this essay is that a contradiction in PA might not result in a contradiction in a sufficiently weakened form of PA that we can still do most forms of useful arithmetic.
Thinking about motives and contradictions, you might find this interesting:
http://video.ias.edu/voevodsky-80th
I hope you are referring to my essay and not Nelson’s, which is a gem.
No, I was talking about Nelson’s essay. There’s nothing in that essay that wouldn’t be covered in a basic course in foundations, aside from his ramblings on the nature of monotheistic faith and the meaning of “I AM WHO I AM” (capitalization in the original). The point that there’s a distinction between how addition and multiplication behave and how exponentiation and higher analogs behave is not new either, although some sections of the essay might be worth explaining some concepts if one removes the theology.
I’m open to the possibility that PA might be inconsistent, although I assign this claim a very low probability. If one asked the question about some broader useful foundational system, such as ZF, I’d assign a much higher but still low probability.
If you think that either of these claims is wrong, I’d be happy to discuss making some form of wager over the likelyhood of an inconsistency being found within some fixed timespan (say 5 years or a decade?).
I’ve heard that Nelson has a standing bet with a colleague: he pays one dollar each year until an inconsistency is found in ZF, is paid one hundred dollars each year after an inconsistency is found.
I might take a more domino-oriented bet.
Do you mean one that focuses on PA? Do you care to suggest a specific bet? (For what matters, I’d estimate around a 10^-6 chance that PA is inconsistent.)
I’m teasing. I don’t think your domino argument can be used to support induction.
Ok. So joking aside, do you want to make a bet on an inconsistency being found in PA in the next five years? 10 years?
I am fairly certain that no inconsistency will be found in the next 10 years.
Incidentally, I’m a little put off by your bringing up betting so early in the conversation. Isn’t it clear that I’m interested in talking about this stuff? That should be enough, especially before you’ve even located a place where you and I disagree.
I’ll mention that if PA is inconsistent, then a consistent prior probability distribution must have P(PA is inconsistent) = 1. (This might not be true if PA is consistent.) Developing a formalism for handling uncertainty about mathematical truths is a line of research in the same ballpark as developing mathematics without induction.
Hmm, I’m not sure why that would be off-putting. There must be some theory of mind issue I’m missing (possibly some sort of implication by suggesting bets that has some sort of negative connotation that I’m not picking up).
Yes, hence making time-based estimates makes more sense.
Ok. So what is your reasoning behind this conclusion?
That you don’t think the other party is capable of marshaling arguments to make you update, or of updating on your arguments.
An estimate of how much progress is made on this sort of problem per man-hour, and of how many man-hours will be devoted to the problem in the next ten years. But I am simply agnostic about whether or not a contradiction can be found “in principle.”
The LW community probably considers betting on a disputed proposition to be much more normal, natural, and non-confrontational than most people do. This is likely because of our Overcoming Bias heritage and Robin Hanson’s work on prediction markets. Betting seems like a good quick way to get people to publicly quantify the probabilities that they assign to propositions. And this, ideally, could help the disputants approach Aumann agreement more quickly.
Ah, I see. That’s not an intended implication. I prefer constructing bets because it forces one (myself) to think carefully about how confident I actually am for a claim. But I see how one might think that.
Ah, that makes a lot of sense.
That make a lot of sense. Presumably this issue is connected to the problem that no one seems to have any idea how one would go about finding such a contradiction.
Incidentally, seriously thinking about these sorts of issues brings up strange issues of equiconsistency. I’m particularly now wondering about the equiconsistency statuses of Robinson arithmetic, the arithmetic hierarchy and, and PA. I don’t know of any result that says something morally like contradictions in PA can be imported into contradictions in Robinson arithmetic (or some extension via the arithmetic hierarchy), but this is pushing the bounds of my knowledge on these issues. Does anyone know if there are any results of that flavor or results in the other direction?
For models for which axiom 3 (0 is not a successor of any number) is false, but the others, including induction, hold, look at modular arithmetic.
Consider the set {n / 2 : n is a natural number } which follows all axioms except induction.
I think pointing out that modular arithmetic violates axiom 3 is akin to pointing out that in yahtzee, four-in-a-row beats three-of-a-kind. You’re not really disputing the rules of poker. I’m speaking gut-wise, not mathematically here.
The point is that that axiom 3 and induction both exclude some models while allowing others. They are both part of defining the natural numbers.
I can’t tell if you’re arguing with me. One of the points of the post is that if you reject axiom 5 you are left with something that strongly resembles the natural numbers—in fact I would agree with Nelson and say that they are what people thought of as natural numbers before induction was codified.
That doesn’t work. If you reject induction, your remaining four axioms also describes the set {(n,m) such that n and m are natural numbers}, where (0, 0) is the zero element and the successor of (n, m) is (n, m + 1). That seems a bit different than the natural numbers, because I added, without violating the first four axioms, additional elements that are not the successor of any element.
I think you’re correct. It is more accurate to say that the counting numbers strongly resemble the natural numbers, than it is to say that every element of every model of axioms 1-4 resembles a natural number.
Note that one can create “weird” models of axioms 1-5 as well.
There are a lot of systems that look almost like the natural numbers but clearly are not. I claim that even if you replace 5 with a succession of weaker axioms you can still get objects that are clearly not the natural numbers.
Consider for example the much weaker claim that every element in N is either 0 or the successor of some other element. It is still easy to see that one can have things that don’t look at all like N. And one can keep adding additional theorems about what N needs to satisfy and still get objects that are pretty concrete and don’t look like what we want the natural numbers to satisfy.
You can actually get some other very weird systems if you want to play around. For example, if you have some underlying set theory and replace induction with the well-ordering principle (which is equivalent modulo some minor technicalities) you can then look at some very interesting systems. For example, well-ordering is second-order, and applies to all sets, so this is in some sense stronger than some first order descriptions of PA where you replace induction with a separate induction axiom for each definable predicate. So one obvious system then is to restrict your well-ordering claim so that it quantifies not over all subsets but over all subsets of some form. Visualizing what such weakened versions of N look like can be quite hard.
I didn’t yet read the paper, but it occurs to me that the direction he seems to want to go in (based on your summary) would be better achieved not by directly weakening/removing induction, but by removing axiom 2.
This would “cut off” induction after a certain point while being more directly in the spirit of ultrafinitism. Also, it seems less “brain breaking” to me. (I don’t reject axiom 2, but the notion of rejecting 2 seems less WTF to me then rejecting 5.)
Can you upload the paper somewhere (I suggest MediaFire)? This interests me, but I can’t download the .pdf.
Done