Standard and Nonstandard Numbers

Fol­lowup to: Log­i­cal Pinpointing

“Oh! Hello. Back again?”

Yes, I’ve got an­other ques­tion. Ear­lier you said that you had to use sec­ond-or­der logic to define the num­bers. But I’m pretty sure I’ve heard about some­thing called ‘first-or­der Peano ar­ith­metic’ which is also sup­posed to define the nat­u­ral num­bers. Go­ing by the name, I doubt it has any ‘sec­ond-or­der’ ax­ioms. Hon­estly, I’m not sure I un­der­stand this sec­ond-or­der busi­ness at all.

“Well, let’s start by ex­am­in­ing the fol­low­ing model:”

“This model has three prop­er­ties that we would ex­pect to be true of the stan­dard num­bers - ‘Every num­ber has a suc­ces­sor’, ‘If two num­bers have the same suc­ces­sor they are the same num­ber’, and ‘0 is the only num­ber which is not the suc­ces­sor of any num­ber’. All three of these state­ments are true in this model, so in that sense it’s quite num­ber­like—”

And yet this model clearly is not the num­bers we are look­ing for, be­cause it’s got all these mys­te­ri­ous ex­tra num­bers like C and −2*. That C thing even loops around, which I cer­tainly wouldn’t ex­pect any num­ber to do. And then there’s that in­finite-in-both-di­rec­tions chain which isn’t cor­rected to any­thing else.

“Right, so, the differ­ence be­tween first-or­der logic and sec­ond-or­der logic is this: In first-or­der logic, we can get rid of the ABC—make a state­ment which rules out any model that has a loop of num­bers like that. But we can’t get rid of the in­finite chain un­der­neath it. In sec­ond-or­der logic we can get rid of the ex­tra chain.”

I would ask you to ex­plain why that was true, but at this point I don’t even know what sec­ond-or­der logic is.

“Bear with me. First, con­sider that the fol­low­ing for­mula de­tects 2-ness:”

x + 2 = x * 2

In other words, that’s a for­mula which is true when x is equal to 2, and false ev­ery­where else, so it sin­gles out 2?

“Ex­actly. And this is a for­mula which de­tects odd num­bers:”

∃y: x=(2*y)+1

Um… okay. That for­mula says, ‘There ex­ists a y, such that x equals 2 times y plus one.’ And that’s true when x is 1, be­cause 0 is a num­ber, and 1=(2*0)+1. And it’s true when x is 9, be­cause there ex­ists a num­ber 4 such that 9=(2*4)+1… right. The for­mula is true at all odd num­bers, and only odd num­bers.

“In­deed. Now sup­pose we had some way to de­tect the ex­is­tence of that ABC-loop in the model—a for­mula which was true at the ABC-loop and false ev­ery­where else. Then I could adapt the nega­tion of this state­ment to say ‘No ob­jects like this are al­lowed to ex­ist’, and add that as an ax­iom alongside ‘Every num­ber has a suc­ces­sor’ and so on. Then I’d have nar­rowed down the pos­si­ble set of mod­els to get rid of mod­els that have an ex­tra ABC-loop in them.”

Um… can I rule out the ABC-loop by say­ing ¬∃x:(x=A)?

“Er, only if you’ve told me what A is in the first place, and in a logic which has ruled out all mod­els with loops in them, you shouldn’t be able to point to a spe­cific ob­ject that doesn’t ex­ist—”

Right. Okay… so the idea is to rule out loops of suc­ces­sors… hm. In the num­bers 0, 1, 2, 3..., the num­ber 0 isn’t the suc­ces­sor of any num­ber. If I just took a group of num­bers start­ing at 1, like {1, 2, 3, …}, then 1 wouldn’t be the suc­ces­sor of any num­ber in­side that group. But in A, B, C, the num­ber A is the suc­ces­sor of C, which is the suc­ces­sor of B, which is the suc­ces­sor of A. So how about if I say: ‘There’s no group of num­bers G such that for any num­ber x in G, x is the suc­ces­sor of some other num­ber y in G.’

“Ah! Very clever. But it so hap­pens that you just used sec­ond-or­der logic, be­cause you talked about groups or col­lec­tions of en­tities, whereas first-or­der logic only talks about in­di­vi­d­ual en­tities. Like, sup­pose we had a logic talk­ing about kit­tens and whether they’re in­no­cent. Here’s a model of a uni­verse con­tain­ing ex­actly three dis­tinct kit­tens who are all in­no­cent:”

Er, what are those ‘prop­erty’ thin­gies?

“They’re all pos­si­ble col­lec­tions of kit­tens. They’re la­beled prop­er­ties be­cause ev­ery col­lec­tion of kit­tens cor­re­sponds to a prop­erty that some kit­tens have and some kit­tens don’t. For ex­am­ple, the col­lec­tion on the top right, which con­tains only the grey kit­ten, cor­re­sponds to a pred­i­cate which is true at the grey kit­ten and false ev­ery­where else, or to a prop­erty which the grey kit­ten has which no other kit­ten has. Ac­tu­ally, for now let’s just pre­tend that ‘prop­erty’ just says ‘col­lec­tion’.”

Okay. I un­der­stand the con­cept of a col­lec­tion of kit­tens.

“In first-or­der logic, we can talk about in­di­vi­d­ual kit­tens, and how they re­late to other in­di­vi­d­ual kit­tens, and whether or not any kit­ten bear­ing a cer­tain re­la­tion ex­ists or doesn’t ex­ist. For ex­am­ple, we can talk about how the grey kit­ten adores the brown kit­ten. In sec­ond-or­der logic, we can talk about col­lec­tions of kit­tens, and whether or not those col­lec­tions ex­ist. So in first-or­der logic, I can say, ‘There ex­ists a kit­ten which is in­no­cent’, or ‘For ev­ery in­di­vi­d­ual kit­ten, that kit­ten is in­no­cent’, or ‘For ev­ery in­di­vi­d­ual kit­ten, there ex­ists an­other in­di­vi­d­ual kit­ten which adores the first kit­ten.’ But it re­quires sec­ond-or­der logic to make state­ments about col­lec­tions of kit­tens, like, ‘There ex­ists no col­lec­tion of kit­tens such that ev­ery kit­ten in it is adored by some other kit­ten in­side the col­lec­tion.’”

I see. So when I tried to say that you couldn’t have any group of num­bers, such that ev­ery num­ber in the group was a suc­ces­sor of some other num­ber in the group...

″...you quan­tified over the ex­is­tence or nonex­is­tence of col­lec­tions of num­bers, which means you were us­ing sec­ond-or­der logic. How­ever, in this par­tic­u­lar case, it’s eas­ily pos­si­ble to rule out the ABC-loop of num­bers us­ing only first-or­der logic. Con­sider the for­mula:”

x=SSSx

x plus 3 is equal to it­self?

“Right. That’s a first-or­der for­mula, since it doesn’t talk about col­lec­tions. And that for­mula is false at 0, 1, 2, 3… but true at A, B, and C.”

What does the ‘+’ mean?

“Er, by ‘+’ I was try­ing to say, ‘this for­mula works out to True’ and similarly ‘¬’ was sup­posed to mean the for­mula works out to False. The gen­eral idea is that we now have a for­mula for de­tect­ing 3-loops, and dis­t­in­guish­ing them from stan­dard num­bers like 0, 1, 2 and so on.”

I see. So by adding the new ax­iom, ¬∃x:x=SSSx, we could rule out all the mod­els con­tain­ing A, B, and C or any other 3-loop of non­stan­dard num­bers.

“Right.”

But this seems like a rather ar­bi­trary sort of ax­iom to add to a fun­da­men­tal the­ory of ar­ith­metic. I mean, I’ve never seen any at­tempt to de­scribe the num­bers which says, ‘No num­ber is equal to it­self plus 3’ as a ba­sic premise. It seems like it should be a the­o­rem, not an ax­iom.

“That’s be­cause it’s brought in us­ing a more gen­eral rule. In par­tic­u­lar, first-or­der ar­ith­metic has an in­finite ax­iom schema—an in­finite but com­putable scheme of ax­ioms. Each ax­iom in the schema says, for a differ­ent first-or­der for­mula Φ(x) - pro­nounced ‘phi of x’ - that:”

  1. If Φ is true at 0, i.e: Φ(0)

  2. And if Φ is true of the suc­ces­sor of any num­ber where it’s true, i.e: ∀x: Φ(x)→Φ(Sx)

  3. Then Φ is true of all num­bers: ∀n: Φ(n)

(Φ(0) ∧ (∀x: Φ(x) → Φ(Sx))) → (∀n: Φ(n))

“In other words, ev­ery for­mula which is true at 0, and which is true of the suc­ces­sor of any num­ber of which it is true, is true ev­ery­where. This is the in­duc­tion schema of first-or­der ar­ith­metic. As a spe­cial case we have the par­tic­u­lar in­duc­tive ax­iom:”

(0≠SSS0 ∧ (∀x: (x≠SSSx) → (Sx≠SSSSx)) → (∀n: n≠SSSn)

But that doesn’t say that for all n, n≠n+3. It gives some premises from which that con­clu­sion would fol­low, but we don’t know the premises.

“Ah, how­ever, we can prove those premises us­ing the other ax­ioms of ar­ith­metic, and hence prove the con­clu­sion. The for­mula (SSSx=x) is false at 0, be­cause 0 is not the suc­ces­sor of any num­ber, in­clud­ing SS0. Similarly, con­sider the for­mula SSSSx=Sx, which we can re­ar­range as S(SSSx)=S(x). If two num­bers have the same suc­ces­sor they are the same num­ber, so SSSx=x. If truth at Sx proves truth at x, then falsity at x proves falsity at Sx, modus po­nens to modus tol­lens. Thus the for­mula is false at zero, false of the suc­ces­sor of any num­ber where it’s false, and so must be false ev­ery­where un­der the in­duc­tion ax­iom schema of first-or­der ar­ith­metic. And so first-or­der ar­ith­metic can rule out mod­els like this:”

...er, I think I see? Be­cause if this model obeys all the other ax­ioms which which we already speci­fied, that didn’t filter it out ear­lier—ax­ioms like ‘zero is not the suc­ces­sor of any num­ber’ and ‘if two num­bers have the same suc­ces­sor they are the same num­ber’ - then we can prove that the for­mula x≠SSSx is true at 0, and prove that if the for­mula true at x it must be true at x+1. So once we then add the fur­ther ax­iom that if x≠SSSx is true at 0, and if x≠SSSx is true at Sy when it’s true at y, then x≠SSSx is true at all x...

“We already have the premises, so we get the con­clu­sion. ∀x: x≠SSSx, and thus we filter out all the 3-loops. Similar logic rules out N-loops for all N.”

So then did we get rid of all the non­stan­dard num­bers, and leave only the stan­dard model?

“No. Be­cause there was also that prob­lem with the in­finite chain … −2*, −1*, 0*, 1* and so on.”

Here’s one idea for get­ting rid of the model with an in­finite chain. All the non­stan­dard num­bers in the chain are “greater” than all the stan­dard num­bers, right? Like, if w is a non­stan­dard num­ber, then w > 3, w > 4, and so on?

“Well, we can prove by in­duc­tion that no num­ber is less than 0, and w isn’t equal to 0 or 1 or 2 or 3, so I’d have to agree with that.”

Okay. We should also be able to prove that if x > y then x + z > y + z. So if we take non­stan­dard w and ask about w + w, then w + w must be greater than w + 3, w + 4, and so on. So w + w can’t be part of the in­finite chain at all, and yet adding any two num­bers ought to yield a third num­ber.

“In­deed, that does prove that if there’s one in­finite chain, there must be two in­finite chains. In other words, that origi­nal, ex­act model in the pic­ture, can’t all by it­self be a model of first-or­der ar­ith­metic. But show­ing that the chain im­plies the ex­is­tence of yet other el­e­ments, isn’t the same as prov­ing that the chain doesn’t ex­ist. Similarly, since all num­bers are even or odd, we must be able to find v with v + v = w, or find v with v + v + 1 = w. Then v must be part of an­other non­stan­dard chain that comes be­fore the chain con­tain­ing w.”

But then that re­quires an in­finite num­ber of in­finite chains of non­stan­dard num­bers which are all greater than any stan­dard num­ber. Maybe we can ex­tend this logic to even­tu­ally reach a con­tra­dic­tion and rule out the ex­is­tence of an in­finite chain in the first place—like, we’d show that any com­plete col­lec­tion of non­stan­dard num­bers has to be larger than it­self -

“Good idea, but no. You end up with the con­clu­sion that if a sin­gle non­stan­dard num­ber ex­ists, it must be part of a chain that’s in­finite in both di­rec­tions, i.e., a chain that looks like an or­dered copy of the nega­tive and pos­i­tive in­te­gers. And that if an in­finite chain ex­ists, there must be in­finite chains cor­re­spond­ing to all ra­tio­nal num­bers. So some­thing that could ac­tu­ally be a non­stan­dard model of first-or­der ar­ith­metic, has to con­tain at least the stan­dard num­bers fol­lowed by a copy of the ra­tio­nal num­bers with each ra­tio­nal num­ber re­placed by a copy of the in­te­gers. But then that setup works just fine with both ad­di­tion and mul­ti­pli­ca­tion—we can’t prove that it has to be any larger than what we’ve already said.”

Okay, so how do we get rid of an in­finite num­ber of in­finite chains of non­stan­dard num­bers, and leave just the stan­dard num­bers at the be­gin­ning? What kind of state­ment would they vi­o­late—what sort of ax­iom would rule out all those ex­tra num­bers?

“We have to use sec­ond-or­der logic for that one.”

Hon­estly I’m still not 100% clear on the differ­ence.

“Okay… ear­lier you gave me a for­mula which de­tected odd num­bers.”

Right. ∃y: x=(2*y)+1, which was true at x=1, x=9 and so on, but not at x=0, x=4 and so on.

“When you think in terms of col­lec­tions of num­bers, well, there’s some col­lec­tions which can be defined by for­mu­las. For ex­am­ple, the col­lec­tion of odd num­bers {1, 3, 5, 7, 9, …} can be defined by the for­mula, with x free, ∃y: x=(2*y)+1. But you could also try to talk about just the col­lec­tion {1, 3, 5, 7, 9, …} as a col­lec­tion, a set of num­bers, whether or not there hap­pened to be any for­mula that defined it—”

Hold on, how can you talk about a set if you can’t define a for­mula that makes some­thing a mem­ber or a non-mem­ber? I mean, that seems a bit smelly from a ra­tio­nal­ist per­spec­tive -

“Er… re­mem­ber the ear­lier con­ver­sa­tion about kit­tens?”

“Sup­pose you say some­thing like, ‘There ex­ists a col­lec­tion of kit­tens, such that ev­ery kit­ten adores only other kit­tens in the col­lec­tion’. Give me a room full of kit­tens, and I can count through all pos­si­ble col­lec­tions, check your state­ment for each col­lec­tion, and see whether or not there’s a col­lec­tion which is ac­tu­ally like that. So the state­ment is mean­ingful—it can be falsified or ver­ified, and it con­strains the state of re­al­ity. But you didn’t give me a lo­cal for­mula for pick­ing up a sin­gle kit­ten and de­cid­ing whether or not it ought to be in this mys­te­ri­ous col­lec­tion. I had to iter­ate through all the col­lec­tions of kit­tens, find the col­lec­tions that matched your state­ment, and only then could I de­cide whether any in­di­vi­d­ual kit­ten had the prop­erty of be­ing in a col­lec­tion like that. But the state­ment was still falsifi­able, even though it was, in math­e­mat­i­cal par­lance, im­pred­ica­tive—that’s what we call it when you make a state­ment that can only be ver­ified by look­ing at many pos­si­ble col­lec­tions, and doesn’t start from any par­tic­u­lar col­lec­tion that you tell me how to con­struct.”

Ah… hm. What about in­finite uni­verses of kit­tens, so you can’t iter­ate through all pos­si­ble col­lec­tions in finite time?

“If you say, ‘There ex­ists a col­lec­tion of kit­tens which all adore each other’, I could ex­hibit a group of three kit­tens which adored each other, and so prove the state­ment true. If you say ‘There’s a col­lec­tion of four kit­tens who adore only each other’, I might come up with a con­struc­tive proof, given the other known prop­er­ties of kit­tens, that your state­ment was false; and any time you tried giv­ing me a group of four kit­tens, I could find a fifth kit­ten, adored by some kit­ten in your group, that falsified your at­tempt. But this is get­ting us into some rather deep parts of math we should prob­a­bly stay out of for now. The point is that even in in­finite uni­verses, there are sec­ond-or­der state­ments that you can prove or falsify in finite amounts of time. And once you ad­mit those par­tic­u­lar sec­ond-or­der state­ments are talk­ing about some­thing mean­ingful, well, you might as well just ad­mit that sec­ond-or­der state­ments in gen­eral are mean­ingful.”

...that sounds a lit­tle iffy to me, like we might get in trou­ble later on.

“You’re not the only math­e­mat­i­cian who wor­ries about that.”

But let’s get back to num­bers. You say that we can use sec­ond-or­der logic to rule out any in­finite chain.

“In­deed. In sec­ond-or­der logic, in­stead of us­ing an in­finite ax­iom schema over all for­mu­las Φ, we quan­tify over pos­si­ble col­lec­tions di­rectly, and say, in a sin­gle state­ment:”

∀P: P(0) ∧ (∀x: P(x) → P(Sx)) → (∀n: P(n))

“Here P is any pred­i­cate true or false of in­di­vi­d­ual num­bers. Any col­lec­tion of num­bers cor­re­sponds to a pred­i­cate that is true of num­bers in­side the col­lec­tion and false of num­bers out­side of it.”

Okay… and how did that rule out in­finite chains again?

“Be­cause in prin­ci­ple, whether or not there’s any first-or­der for­mula that picks them out, there’s the­o­ret­i­cally a col­lec­tion that con­tains the stan­dard num­bers {0, 1, 2, …} and only the stan­dard num­bers. And if you treat that col­lec­tion as a pred­i­cate P, then P is true at 0 - that is, 0 is in the stan­dard num­bers. And if 200 is a stan­dard num­ber then so is 201, and so on; if P is true at x, it’s true at x+1. On the other hand, if you treat the col­lec­tion ‘just the stan­dard num­bers’ as a pred­i­cate, it’s false at −2*, false at −1*, false at 0* and so on—those num­bers aren’t in this the­o­ret­i­cal col­lec­tion. So it’s vac­u­ously true that this pred­i­cate is true at 1* if it’s true at 0*, be­cause it’s not true at 0*. And so we end up with:”

“And so the sin­gle sec­ond-or­der ax­iom...”

∀P: P0 ∧ (∀x: Px → P(Sx)) → (∀n: Pn)

″...rules out any dis­con­nected chains, finite loops, and in­deed ev­ery non­stan­dard num­ber, in one swell foop.”

But what did that ax­iom mean, ex­actly? I mean, taboo the phrase ‘stan­dard num­bers’ for a mo­ment, pre­tend I’ve got no idea what those are, just ex­plain to me what the ax­iom ac­tu­ally says.

“It says that the model be­ing dis­cussed—the model which fits this ax­iom—makes it im­pos­si­ble to form any col­lec­tion closed un­der suc­ces­sion which in­cludes 0 and doesn’t in­clude ev­ery­thing. It’s im­pos­si­ble to have any col­lec­tion of ob­jects in this uni­verse such that 0 is in the col­lec­tion, and the suc­ces­sor of ev­ery­thing in the col­lec­tion is in the col­lec­tion, and yet this col­lec­tion doesn’t con­tain ev­ery­thing. So you can’t have a dis­con­nected in­finite chain—there would then ex­ist at least one col­lec­tion over ob­jects in this uni­verse that con­tained 0 and all its suc­ces­sor-de­scen­dants, yet didn’t con­tain the chain; and we have a shiny new ax­iom which says that can’t hap­pen.”

Can you per­haps op­er­a­tional­ize that in a more sen­so­ry­mo­tory sort of way? Like, if this is what I be­lieve about the uni­verse, then what do I ex­pect to see?

“If this is what you be­lieve about the math­e­mat­i­cal model that you live in… then you be­lieve that nei­ther you, nor any ad­ver­sary, nor yet a su­per­in­tel­li­gence, nor yet God, can con­sis­tently say ‘Yea’ or ‘Nay’ to ob­jects in such fash­ion that when you pre­sent them with 0, they say ‘Yea’, and when you pre­sent them with any other ob­ject, if they say ‘Yea’, they also say ‘Yea’ for the suc­ces­sor of that ob­ject; and yet there is some ob­ject for which they say ‘Nay’. You be­lieve this can never hap­pen, no mat­ter what. The way in which the ob­jects in the uni­verse are ar­ranged by suc­ces­sion, just doesn’t let that hap­pen, ever.”

Ah. So if, say, they said ‘Nay’ for 42, I’d go back and ask about 41, and then 40, and by the time I reached 0, I’d find ei­ther that they said ‘Nay’ about 0, or that they said ‘Nay’ for 41 and yet ‘Yea’ for 40. And what do I ex­pect to see if I be­lieve in first-or­der ar­ith­metic, with the in­finite ax­iom schema?

“In that case, you be­lieve there’s no neatly speci­fi­able, com­pactly de­scrib­able rule which be­haves like that. But if you be­lieve the sec­ond-or­der ver­sion, you be­lieve no­body can pos­si­bly be­have like that even if they’re an­swer­ing ran­domly, or branch­ing the uni­verse to an­swer differ­ent ways in differ­ent al­ter­nate uni­verses, and so on. And note, by the way, that if we have a finite uni­verse—i.e., we throw out the rule that ev­ery num­ber has a suc­ces­sor, and say in­stead that 256 is the only num­ber which has no suc­ces­sor—then we can ver­ify this ax­iom in finite time.”

I see. Still, is there any way to rule out in­finite chains us­ing first-or­der logic? I might find that eas­ier to deal with, even if it looks more com­pli­cated at first.

“I’m afraid not. One way I like to look at it is that first-or­der logic can talk about con­straints on how the model looks from any lo­cal point, while only sec­ond-or­der logic can talk about global qual­ities of chains, col­lec­tions, and the model as a whole. Whether ev­ery num­ber has a suc­ces­sor is a lo­cal prop­erty—a ques­tion of how the model looks from the van­tage point of any one num­ber. Whether a num­ber plus three, can be equal to it­self, is a ques­tion you could eval­u­ate at the lo­cal van­tage point of any one num­ber. Whether a num­ber is even, is a ques­tion you can an­swer by look­ing around for a sin­gle, in­di­vi­d­ual num­ber x with the prop­erty that x+x equals the first num­ber. But when you try to say that there’s only one con­nected chain start­ing at 0, by in­vok­ing the idea of con­nect­ed­ness and chains you’re try­ing to de­scribe non-lo­cal prop­er­ties that re­quire a logic-of-pos­si­ble-col­lec­tions to spec­ify.”

Huh. But if all the ‘lo­cal’ prop­er­ties are the same re­gard­less, why worry about global prop­er­ties? In first-or­der ar­ith­metic, any ‘lo­cal’ for­mula that’s true at zero and all of its ‘nat­u­ral’ suc­ces­sors would also have to be true of all the dis­con­nected in­finite chains… right? Or did I make an er­ror there? All the other in­finite chains be­sides the 0-chain—all ‘non­stan­dard num­bers’ - would have just the same prop­er­ties as the ‘nat­u­ral’ num­bers, right?

“I’m afraid not. The first-or­der ax­ioms of ar­ith­metic may fail to pin down whether or not a Tur­ing ma­chine halts—whether there ex­ists a time at which a Tur­ing ma­chine halts. Let’s say that from our per­spec­tive in­side the stan­dard num­bers, the Tur­ing ma­chine ‘re­ally doesn’t’ halt—it doesn’t halt on clock tick 0, doesn’t halt on clock tick 1, doesn’t halt on tick 2, and so on through all the stan­dard suc­ces­sors of the 0-chain. In non­stan­dard mod­els of the in­te­gers—mod­els with other in­finite chains—there might be some­where in­side a non­stan­dard chain where the Tur­ing ma­chine goes from run­ning to halted and stays halted there­after.”

“In this new model—which is fully com­pat­i­ble with the first-or­der ax­ioms, and can’t be ruled out by them—it’s not true that ‘for ev­ery num­ber t at which the Tur­ing ma­chine is run­ning, it will still be run­ning at t+1’. Even though if we could some­how re­strict our at­ten­tion to the ‘nat­u­ral’ num­bers, we would see that the Tur­ing ma­chine was run­ning at 0, 1, 2, and ev­ery time in the suc­ces­sor-chain of 0.”

Okay… I’m not quite sure what the prac­ti­cal im­pli­ca­tion of that is?

“It means that many Tur­ing ma­chines which in fact never halt at any stan­dard time, can’t be proven not to halt us­ing first-or­der rea­son­ing, be­cause their non-halt­ing-ness does not ac­tu­ally fol­low log­i­cally from the first-or­der ax­ioms. Logic is about which con­clu­sions fol­low from which premises, re­mem­ber? If there are mod­els which are com­pat­i­ble with all the first-or­der premises, but still falsify the state­ment ‘X runs for­ever’, then the state­ment ‘X runs for­ever’ can’t log­i­cally fol­low from those premises. This means you won’t be able to prove—shouldn’t be able to prove—that this Tur­ing ma­chine halts, us­ing only first-or­der logic.”

How ex­actly would this fail in prac­tice? I mean, where does the proof go bad?

“You wouldn’t get the sec­ond step of the in­duc­tion, ‘for ev­ery num­ber t at which the Tur­ing ma­chine is run­ning, it will still be run­ning at t+1’. There’d be non­stan­dard mod­els with some non­stan­dard t that falsifies the premise—a non­stan­dard time where the Tur­ing ma­chine goes from run­ning to halted. Even though if we could some­how re­strict our at­ten­tion to only the stan­dard num­bers, we would see that the Tur­ing ma­chine was run­ning at 0, 1, 2, and so on.”

But if a Tur­ing ma­chine re­ally ac­tu­ally halts, there’s got to be some par­tic­u­lar time when it halts, like on step 97 -

“In­deed. But 97 ex­ists in all non­stan­dard mod­els of ar­ith­metic, so we can prove its ex­is­tence in first-or­der logic. Any time 0 is a num­ber, ev­ery num­ber has a suc­ces­sor, num­bers don’t loop, and so on, there’ll ex­ist 97. Every non­stan­dard model has at least the stan­dard num­bers. So when­ever a Tur­ing ma­chine does halt, you can prove in first-or­der ar­ith­metic that it halts—it does in­deed fol­low from the premises. That’s kinda what you’d ex­pect, given that you can just watch the Tur­ing ma­chine for 97 steps. When some­thing ac­tu­ally does halt, you should be able to prove it halts with­out wor­ry­ing about un­bounded fu­ture times! It’s when some­thing doesn’t ac­tu­ally halt—in the stan­dard num­bers, that is—that the ex­is­tence of ‘non­stan­dard halt­ing times’ be­comes a prob­lem. Then, the con­clu­sion that the Tur­ing ma­chine runs for­ever may not ac­tu­ally fol­low from first-or­der ar­ith­metic, be­cause you can obey all the premises of first-or­der ar­ith­metic, and yet still be in­side a non­stan­dard model where this Tur­ing ma­chine halts at a non­stan­dard time.”

So sec­ond-or­der ar­ith­metic is more pow­er­ful than first-or­der ar­ith­metic in terms of what fol­lows from the premises?

“That fol­lows in­evitably from the abil­ity to talk about fewer pos­si­ble mod­els. As it is writ­ten, ‘What is true of one ap­ple may not be true of an­other ap­ple; thus more can be said about a sin­gle ap­ple than about all the ap­ples in the world.’ If you can re­strict your dis­course to a nar­rower col­lec­tion of mod­els, there are more facts that fol­low in­evitably, be­cause the more mod­els you might be talk­ing about, the fewer facts can pos­si­bly be true about all of them. And it’s also definitely true that sec­ond-or­der ar­ith­metic proves more the­o­rems than first-or­der ar­ith­metic—for ex­am­ple, it can prove that a Tur­ing ma­chine which com­putes Good­stein se­quences always reaches 0 and halts, or that Her­cules always wins the hy­dra game. But there’s a bit of con­tro­versy we’ll get into later about whether sec­ond-or­der logic is ac­tu­ally more pow­er­ful than first-or­der logic in gen­eral.”

Well, sure. After all, just be­cause no­body has ever yet in­vented a first-or­der for­mula to filter out all the non­stan­dard num­bers, doesn’t mean it can never, ever be done. To­mor­row some brilli­ant math­e­mat­i­cian might figure out a way to take an in­di­vi­d­ual num­ber x, and do lo­cal things to it us­ing ad­di­tion and mul­ti­pli­ca­tion and the ex­is­tence or nonex­is­tence of other in­di­vi­d­ual num­bers, which can tell us whether that num­ber is part of the 0-chain or some other in­finite-in-both-di­rec­tions chain. It’ll be as easy as (a=b*c) -

“Nope. Ain’t never gonna hap­pen.”

But maybe you could find some en­tirely differ­ent cre­ative way of first-or­der ax­io­m­a­tiz­ing the num­bers which has only the stan­dard model -

“Nope.”

Er… how do you know that, ex­actly? I mean, part of the Player Char­ac­ter Code is that you don’t give up when some­thing seems im­pos­si­ble. I can’t quite see yet how to de­tect in­finite chains us­ing a first-or­der for­mula. But then ear­lier I didn’t re­al­ize you could rule out finite loops, which turned out to be quite sim­ple once you ex­plained. After all, there’s two dis­tinct uses of the word ‘im­pos­si­ble’, one which in­di­cates pos­i­tive knowl­edge that some­thing can never be done, that no pos­si­ble chain of ac­tions can ever reach a goal, even if you’re a su­per­in­tel­li­gence. This kind of knowl­edge re­quires a strong, definite grasp on the sub­ject mat­ter, so that you can rule out ev­ery pos­si­ble av­enue of suc­cess. And then there’s an­other, much more com­mon use of the word ‘im­pos­si­ble’, which means that you thought about it for five sec­onds but didn’t see any way to do it, usu­ally used in the pres­ence of weak grasps on a sub­ject, sub­jects that seem sa­credly mys­te­ri­ous -

“Right. Rul­ing out an in­finite-in-both-di­rec­tions chain, us­ing a first-or­der for­mula, is the first kind of im­pos­si­bil­ity. We know that it can never be done.”

I see. Well then, what do you think you know, and how do you think you know it? How is this definite, pos­i­tive knowl­edge of im­pos­si­bil­ity ob­tained, us­ing your strong grasp on the non-mys­te­ri­ous sub­ject mat­ter?

“We’ll take that up next time.”

Part of the se­quence Highly Ad­vanced Episte­mol­ogy 101 for Beginners

Next post: “Godel’s Com­plete­ness and In­com­plete­ness The­o­rems

Pre­vi­ous post: “By Which It May Be Judged