Second-Order Logic: The Controversy

Fol­lowup to: Godel’s Com­plete­ness and In­com­plete­ness Theorems

“So the ques­tion you asked me last time was, ‘Why does any­one bother with first-or­der logic at all, if sec­ond-or­der logic is so much more pow­er­ful?’”

Right. If first-or­der logic can’t talk about finite­ness, or dis­t­in­guish the size of the in­te­gers from the size of the re­als, why even bother?

“The first thing to re­al­ize is that first-or­der the­o­ries can still have a lot of power. First-or­der ar­ith­metic does nar­row down the pos­si­ble mod­els by a lot, even if it doesn’t nar­row them down to a sin­gle model. You can prove things like the ex­is­tence of an in­finite num­ber of primes, be­cause ev­ery model of the first-or­der ax­ioms has an in­finite num­ber of primes. First-or­der ar­ith­metic is never go­ing to prove any­thing that’s wrong about the stan­dard num­bers. Any­thing that’s true in all mod­els of first-or­der ar­ith­metic will also be true in the par­tic­u­lar model we call the stan­dard num­bers.”

Even so, if first-or­der the­ory is strictly weaker, why bother? Un­less sec­ond-or­der logic is just as in­com­plete rel­a­tive to third-or­der logic, which is weaker than fourth-or­der logic, which is weaker than omega-or­der logic -

“No, sur­pris­ingly enough—there’s tricks for mak­ing sec­ond-or­der logic en­code any propo­si­tion in third-or­der logic and so on. If there’s a col­lec­tion of third-or­der ax­ioms that char­ac­ter­izes a model, there’s a col­lec­tion of sec­ond-or­der ax­ioms that char­ac­ter­izes the same model. Once you make the jump to sec­ond-or­der logic, you’re done—so far as any­one knows (so far as I know) there’s noth­ing more pow­er­ful than sec­ond-or­der logic in terms of which mod­els it can char­ac­ter­ize.”

Then if there’s one spoon which can eat any­thing, why not just use the spoon?

“Well… this gets into com­plex is­sues. There are math­e­mat­i­ci­ans who don’t be­lieve there is a spoon when it comes to sec­ond-or­der logic.”

Like there are math­e­mat­i­ci­ans who don’t be­lieve in in­finity?

“Kind of. Look, sup­pose you couldn’t use sec­ond-or­der logic—you be­longed to a species that doesn’t have sec­ond-or­der logic, or any­thing like it. Your species doesn’t have any na­tive men­tal in­tu­ition you could use to con­struct the no­tion of ‘all prop­er­ties’. And then sup­pose that, af­ter some­body used first-or­der set the­ory to prove that first-or­der ar­ith­metic had many pos­si­ble mod­els, you stood around shout­ing that you be­lieved in only one model, what you called the stan­dard model, but you couldn’t ex­plain what made this model differ­ent from any other model—”

Well… a lot of times, even in math, we make state­ments that gen­uinely mean some­thing, but take a while to figure out how to define. I think some­body who talked about ‘the num­bers’ would mean some­thing even be­fore sec­ond-or­der logic was in­vented.

“But here the hy­poth­e­sis is that you be­long to a species that can’t in­vent sec­ond-or­der logic, or think in sec­ond-or­der logic, or any­thing like it.”

Then I sup­pose you want me to draw the con­clu­sion that this hy­po­thet­i­cal alien is just stand­ing there shout­ing about stan­dard­ness, but its words don’t mean any­thing be­cause they have no way to pin down one model as op­posed to an­other one. And I ex­pect this species is also mag­i­cally for­bid­den from talk­ing about all pos­si­ble sub­sets of a set?

“Yeah. They can’t talk about the largest pow­er­set, just like they can’t talk about the small­est model of Peano ar­ith­metic.”

Then you could ar­guably deny that shout­ing about the ‘stan­dard’ num­bers would mean any­thing, to the mem­bers of this par­tic­u­lar species. You might as well shout about the ‘fleem’ num­bers, I guess.

“Right. Even if all the mem­bers of this species did have a built-in sense that there was a spe­cial model of first-or­der ar­ith­metic that was fleemer than any other model, if that fleem-ness wasn’t bound to any­thing else, it would be mean­ingless. Just a float­ing word. Or if all you could do was define fleem­ness as floob­ness and floob­ness as fleem­ness, you’d have a loop of float­ing words; and that might give you the im­pres­sion that each par­tic­u­lar word had a mean­ing, but the loop as a whole wouldn’t be con­nected to re­al­ity. That’s why it doesn’t help to say that the stan­dard model of num­bers is the small­est among all pos­si­ble mod­els of Peano ar­ith­metic, if you can’t define ‘small­est pos­si­ble’ any more than you can define ‘con­nected chain’ or ‘finite num­ber of pre­de­ces­sors’.”

But sec­ond-or­der logic does seem to have con­se­quences first-or­der logic doesn’t. Like, what about all that Godelian stuff? Doesn’t sec­ond-or­der ar­ith­metic se­man­ti­cally im­ply… its own Godel state­ment? Be­cause the unique model of sec­ond-or­der ar­ith­metic doesn’t con­tain any num­ber en­cod­ing a proof of a con­tra­dic­tion from sec­ond-or­der ar­ith­metic? Wait, now I’m con­fused.

“No, that’s cor­rect. It’s not para­dox­i­cal, be­cause there’s no effec­tive way of find­ing all the se­man­tic im­pli­ca­tions of a col­lec­tion of sec­ond-or­der ax­ioms. There’s no analogue of Godel’s Com­plete­ness The­o­rem for sec­ond-or­der logic—no syn­tac­tic sys­tem for de­riv­ing all the se­man­tic con­se­quences. Se­cond-or­der logic is sound, in the sense that any­thing syn­tac­ti­cally prov­able from a set of premises, is true in any model obey­ing those premises. But sec­ond-or­der logic isn’t com­plete; there are se­man­tic con­se­quences you can’t de­rive. If you take sec­ond-or­der logic at face value, there’s no effec­tively com­putable way of de­riv­ing all the con­se­quences of what you say you ‘be­lieve’… which is a ma­jor rea­son some math­e­mat­i­ci­ans are sus­pi­cious of sec­ond-or­der logic. What does it mean to be­lieve some­thing whose con­se­quences you can’t de­rive?”

But sec­ond-or­der logic clearly has some ex­pe­ri­en­tial con­se­quences first-or­der logic doesn’t. Sup­pose I build a Tur­ing ma­chine that looks for proofs of a con­tra­dic­tion from first-or­der Peano ar­ith­metic. If PA’s con­sis­tency isn’t prov­able in PA, then by the Com­plete­ness The­o­rem there must ex­ist non­stan­dard mod­els of PA where this ma­chine halts af­ter find­ing a proof of a con­tra­dic­tion. So first-or­der logic doesn’t tell me that this ma­chine runs for­ever—maybe it has non­stan­dard halt­ing times, i.e., it runs at all stan­dard N, but halts at −2* some­where along a dis­con­nected chain. Only sec­ond-or­der logic tells me there’s no proof of PA’s in­con­sis­tency and there­fore this ma­chine runs for­ever. Only sec­ond-or­der logic tells me I should ex­pect to see this ma­chine keep run­ning, and not ex­pect—note falsifi­a­bil­ity—that the ma­chine ever halts.

“Sure, you just used a sec­ond-or­der the­ory to de­rive a con­se­quence you didn’t get from a first-or­der the­ory. But that’s not the same as say­ing that you can only get that con­se­quence us­ing sec­ond-or­der logic. Maybe an­other first-or­der the­ory would give you the same pre­dic­tion.”

Like what?

“Well, for one thing, first-or­der set the­ory can prove that first-or­der ar­ith­metic has a model. Zer­melo-Fraenkel set the­ory can prove the ex­is­tence of a set such that all the first-or­der Peano ax­ioms are true about that set. It fol­lows within ZF that sound rea­son­ing on first-or­der ar­ith­metic will never prove a con­tra­dic­tion. And since ZF can prove that the syn­tax of clas­si­cal logic is sound—”

What does it mean for set the­ory to prove that logic is sound!?

“ZF can quote for­mu­las as struc­tured, and en­code mod­els as sets, and then rep­re­sent a finite ZF-for­mula which says whether or not a set of quoted for­mu­las is true about a model. ZF can then prove that no step of clas­si­cal logic goes from premises that are true in­side a set-model, to premises that are false in­side a set-model. In other words, ZF can rep­re­sent the idea ‘for­mula X is se­man­ti­cally true in model Y’ and ‘these syn­tac­tic rules never pro­duce se­man­ti­cally false state­ments from se­man­ti­cally true state­ments’.”

Wait, then why can’t ZF prove it­self con­sis­tent? If ZF be­lieves in all the ax­ioms of ZF, and it be­lieves that logic never pro­duces false state­ments from true state­ments -

“Ah, but ZF can’t prove that there ex­ists any set which is a model of ZF, so it can’t prove the ZF-ax­ioms are con­sis­tent. ZF shouldn’t be able to prove that some set is a model of ZF, be­cause that’s not true in all mod­els. Many mod­els of ZF don’t con­tain any in­di­vi­d­ual set well-pop­u­lated enough for that one set to be a model of ZF all by it­self.”

I’m kind of sur­prised in a Godelian sense that ZF can con­tain sets as large as the uni­verse of ZF. Doesn’t any given set have to be smaller than the whole uni­verse?

“In­side any par­tic­u­lar model of ZF, ev­ery set within that model is smaller than that model. But not all mod­els of ZF are the same size; in fact, mod­els of ZF of ev­ery size ex­ist, by the Lowen­heim-Skolem the­o­rem. So you can have some mod­els of ZF—some uni­verses in which all the el­e­ments col­lec­tively obey the ZF-re­la­tions—con­tain­ing in­di­vi­d­ual sets which are larger than other en­tire mod­els of ZF. A set that large is called a Grothendieck uni­verse and as­sum­ing it ex­ists is equiv­a­lent to as­sum­ing the ex­is­tence of ‘strongly in­ac­cessible car­di­nals’, sizes so large that you prov­ably can’t prove in­side set the­ory that any­thing that large ex­ists.”

Whoa.

(Pause.)

But...

“But?”

I agree you’ve shown that one ex­pe­ri­en­tial con­se­quence of sec­ond-or­der ar­ith­metic—namely that a ma­chine look­ing for proofs of in­con­sis­tency from PA, won’t be seen to halt—can be de­rived from first-or­der set the­ory. Can you get all the con­se­quences of sec­ond-or­der ar­ith­metic in some par­tic­u­lar first-or­der the­ory?

“You can’t get all the se­man­tic con­se­quences of sec­ond-or­der logic, taken at face value, in any the­ory or any com­putable rea­son­ing. What about the halt­ing prob­lem? Taken at face value, it’s a se­man­tic con­se­quence of sec­ond-or­der logic that any given Tur­ing ma­chine ei­ther halts or doesn’t halt—”

Per­son­ally I find it rather in­tu­itive to imag­ine that a Tur­ing ma­chine ei­ther halts or doesn’t halt. I mean, if I’m walk­ing up to a ma­chine and watch­ing it run, tel­ling me that its halt­ing or not-halt­ing ‘isn’t en­tailed by my ax­ioms’ strikes me as not de­scribing any ac­tual ex­pe­rience I can have with the ma­chine. Either I’ll see it halt even­tu­ally, or I’ll see it keep run­ning for­ever.

“My point is that the state­ments we can de­rive from the syn­tax of cur­rent sec­ond-or­der logic is limited by that syn­tax. And by the halt­ing prob­lem, we shouldn’t ever ex­pect a com­putable syn­tax that gives us all the se­man­tic con­se­quences. There’s no pos­si­ble the­ory you can ac­tu­ally use to get a cor­rect ad­vance pre­dic­tion about whether an ar­bi­trary Tur­ing ma­chine halts.”

Okay. I agree that no com­putable rea­son­ing, on sec­ond-or­der logic or any­thing else, should be able to solve the halt­ing prob­lem. Un­less time travel is pos­si­ble, but even then, you shouldn’t be able to solve the ex­panded halt­ing prob­lem for ma­chines that use time travel.

“Right, so the syn­tax of sec­ond-or­der logic can’t prove ev­ery­thing. And in fact, it turns out that, in terms of what you can prove syn­tac­ti­cally us­ing the stan­dard syn­tax, sec­ond-or­der logic is iden­ti­cal to a many-sorted first-or­der logic.”

Huh?

“Sup­pose you have a first-or­der logic—one that doesn’t claim to be able to quan­tify over all pos­si­ble pred­i­cates—which does al­low the uni­verse to con­tain two differ­ent sorts of things. Say, the logic uses lower-case let­ters for all type-1 ob­jects and up­per-case let­ters for all type-2 ob­jects. Like, ‘∀x: x = x’ is a state­ment over all type-1 ob­jects, and ‘∀Y: Y = Y’ is a state­ment over all type-2 ob­jects. But aside from that, you use the same syn­tax and proof rules as be­fore.”

Okay...

“Now add an el­e­ment-re­la­tion x∈Y, say­ing that x is an el­e­ment of Y, and add some first-or­der ax­ioms for mak­ing the type-2 ob­jects be­have like col­lec­tions of type-1 ob­jects, in­clud­ing ax­ioms for mak­ing sure that most de­scrib­able type-2 col­lec­tions ex­ist—i.e., the col­lec­tion X con­tain­ing just x is guaran­teed to ex­ist, and so on. What you can prove syn­tac­ti­cally in this the­ory will be iden­ti­cal to what you can prove us­ing the stan­dard syn­tax of sec­ond-or­der logic—even though the the­ory doesn’t claim that all pos­si­ble col­lec­tions of type-1s are type-2s, and the the­ory will have mod­els where many ‘pos­si­ble’ col­lec­tions are miss­ing from the type-2s.”

Wait, now you’re say­ing that sec­ond-or­der logic is no more pow­er­ful than first-or­der logic?

“I’m say­ing that the sup­posed power of sec­ond-or­der logic de­rives from in­ter­pret­ing it a par­tic­u­lar way, and tak­ing on faith that when you quan­tify over all prop­er­ties, you’re ac­tu­ally talk­ing about all prop­er­ties.”

But then sec­ond-or­der ar­ith­metic is no more pow­er­ful than first-or­der ar­ith­metic in terms of what it can ac­tu­ally prove?

“2nd-or­der ar­ith­metic is way more pow­er­ful than first-or­der ar­ith­metic. But that’s be­cause first-or­der set the­ory is more pow­er­ful than ar­ith­metic, and adding the syn­tax of sec­ond-or­der logic cor­re­sponds to adding ax­ioms with set-the­o­retic prop­er­ties. In terms of which con­se­quences can be syn­tac­ti­cally proven, sec­ond-or­der ar­ith­metic is more pow­er­ful than first-or­der ar­ith­metic, but weaker than first-or­der set the­ory. First-or­der set the­ory can prove the ex­is­tence of a model of sec­ond-or­der ar­ith­metic—ZF can prove there’s a col­lec­tion of num­bers and sets of num­bers which mod­els a many-sorted logic with syn­tax cor­re­spond­ing to sec­ond-or­der logic—and so ZF can prove sec­ond-or­der ar­ith­metic con­sis­tent.”

But first-or­der logic, in­clud­ing first-or­der set the­ory, can’t even talk about the stan­dard num­bers!

“Right, but first-or­der set the­ory can syn­tac­ti­cally prove more state­ments about ‘num­bers’ than sec­ond-or­der ar­ith­metic can prove. And when you com­bine that with the se­man­tic im­pli­ca­tions of sec­ond-or­der ar­ith­metic not be­ing com­putable, and with any sec­ond-or­der logic be­ing syn­tac­ti­cally iden­ti­cal to a many-sorted first-or­der logic, and first-or­der logic hav­ing neat prop­er­ties like the Com­plete­ness The­o­rem… well, you can see why some math­e­mat­i­ci­ans would want to give up en­tirely on this whole sec­ond-or­der busi­ness.”

But if you deny sec­ond-or­der logic you can’t even say the word ‘finite’. You would have to be­lieve the word ‘finite’ was a mean­ingless noise.

“You’d define finite­ness rel­a­tive to what­ever first-or­der model you were work­ing in. Like, a set might be ‘finite’ only on ac­count of the model not con­tain­ing any one-to-one map­ping from that set onto a smaller sub­set of it­self—”

But that set wouldn’t ac­tu­ally be finite. There wouldn’t ac­tu­ally be, like, only a billion ob­jects in there. It’s just that all the map­pings which could prove the set was in­finite would be mys­te­ri­ously miss­ing.

“Ac­cord­ing to some other model, maybe. But since there is no one true model—”

How is this not crazy talk along the lines of ‘there is no one true re­al­ity’? Are you say­ing there’s no re­ally small­est set of num­bers closed un­der suc­ces­sion, with­out all the ex­tra in­finite chains? Doesn’t talk­ing about how these the­o­ries have mul­ti­ple pos­si­ble mod­els, im­ply that those pos­si­ble mod­els are log­i­cal thin­gies and one of them ac­tu­ally does con­tain the largest pow­er­set and the small­est in­te­gers?

“The math­e­mat­i­ci­ans who deny sec­ond-or­der logic would see that rea­son­ing as in­vok­ing an im­plicit back­ground uni­verse of set the­ory. Every­thing you’re say­ing makes sense rel­a­tive to some par­tic­u­lar model of set the­ory, which would con­tain pos­si­ble mod­els of Peano ar­ith­metic as sets, and could look over those sets and pick out the small­est in that model. Similarly, that set the­ory could look over a pro­posed model for a many-sorted logic, and say whether there were any sub­sets within the larger uni­verse which were miss­ing from the many-sorted model. Ba­si­cally, your brain is in­sist­ing that it lives in­side some par­tic­u­lar model of set the­ory. And then, from that stand­point, you could look over some other set the­ory and see how it was miss­ing sub­sets that your the­ory had.”

Argh! No, damn it, I live in the set the­ory that re­ally does have all the sub­sets, with no mys­te­ri­ously miss­ing sub­sets or mys­te­ri­ous ex­tra num­bers, or de­nu­mer­able col­lec­tions of all pos­si­ble re­als that could like to­tally map onto the in­te­gers if the map­ping that did it hadn’t gone miss­ing in the Aus­tralian out­back -

“But ev­ery­body says that.”

Okay...

“Yeah?”

Screw set the­ory. I live in the phys­i­cal uni­verse where when you run a Tur­ing ma­chine, and keep watch­ing for­ever in the phys­i­cal uni­verse, you never ex­pe­rience a time where that Tur­ing ma­chine out­puts a proof of the in­con­sis­tency of Peano Arith­metic. Fur­ther­more, I live in a uni­verse where space is ac­tu­ally com­posed of a real field and space is ac­tu­ally in­finitely di­visi­ble and con­tains all the points be­tween A and B, rather than space only con­tain­ing a de­nu­mer­able num­ber of points whose ex­is­tence can be proven from the first-or­der ax­iom­a­ti­za­tion of the real num­bers. So to talk about physics—for­get about math­e­mat­ics—I’ve got to use sec­ond-or­der logic.

“Ah. You know, that par­tic­u­lar re­sponse is not one I have seen in the pre­vi­ous liter­a­ture.”

Yes, well, I’m not a pure math­e­mat­i­cian. When I ask whether I want an Ar­tifi­cial In­tel­li­gence to think in sec­ond-or­der logic or first-or­der logic, I won­der how that af­fects what the AI does in the ac­tual phys­i­cal uni­verse. Here in the ac­tual phys­i­cal uni­verse where times are fol­lowed by suc­ces­sor times, I strongly sus­pect that we should only ex­pect to ex­pe­rience stan­dard times, and not ex­pe­rience any non­stan­dard times. I think time is con­nected, and global con­nect­ed­ness is a prop­erty I can only talk about us­ing sec­ond-or­der logic. I think that ev­ery par­tic­u­lar time is finite, and yet time has no up­per bound—that there are all finite times, but only finite times—and that’s a prop­erty I can only char­ac­ter­ize us­ing sec­ond-or­der logic.

“But if you can’t ever tell the differ­ence be­tween stan­dard and non­stan­dard times? I mean, lo­cal prop­er­ties of time can be de­scribed us­ing first-or­der logic, and you can’t di­rectly see global prop­er­ties like ‘con­nect­ed­ness’ -”

But I can tell the differ­ence. There are only non­stan­dard times where a proof-check­ing ma­chine, run­ning for­ever, out­puts a proof of in­con­sis­tency from the Peano ax­ioms. So I don’t ex­pect to ex­pe­rience see­ing a ma­chine do that, since I ex­pect to ex­pe­rience only stan­dard times.

“Set the­ory can also prove PA con­sis­tent. If you use set the­ory to define time, you similarly won’t ex­pect to see a time where PA is proven in­con­sis­tent—those non­stan­dard in­te­gers don’t ex­ist in any model of ZF.”

Why should I an­ti­ci­pate that my phys­i­cal uni­verse is re­stricted to hav­ing only the non­stan­dard times al­lowed by a more pow­er­ful set the­ory, in­stead of non­stan­dard times al­lowed by first-or­der ar­ith­metic? If I then talk about a non­stan­dard time where a proof-enu­mer­at­ing ma­chine proves ZF in­con­sis­tent, will you say that only non­stan­dard times al­lowed by some still more pow­er­ful the­ory can ex­ist? I think it’s clear that the way you’re de­cid­ing which ex­per­i­men­tal out­comes you’ll have to ex­cuse, is by se­cretly as­sum­ing that only stan­dard times ex­ist re­gard­less of which the­ory is re­quired to nar­row it down.

“Ah… hm. Doesn’t physics say this uni­verse is go­ing to run out of ne­gen­tropy be­fore you can do an in­finite amount of com­pu­ta­tion? Maybe there’s only a bounded amount of time, like it stops be­fore googol­plex or some­thing. That can be char­ac­ter­ized by first-or­der the­o­ries.”

We don’t know that for cer­tain, and I wouldn’t want to build an AI that just as­sumed lifes­pans had to be finite, in case it was wrong. Be­sides, should I use a differ­ent logic than if I’d found my­self in Con­way’s Game of Life, or some­thing else re­ally in­finite? Wouldn’t the same sort of crea­tures evolve in that uni­verse, hav­ing the same sort of math de­bates?

“Per­haps no uni­verse like that can ex­ist; per­haps only finite uni­verses can ex­ist, be­cause only finite uni­verses can be uniquely char­ac­ter­ized by first-or­der logic.”

You just used the word ‘finite’! Fur­ther­more, taken at face value, our own uni­verse doesn’t look like it has a finite col­lec­tion of en­tities re­lated by first-or­der log­i­cal rules. Space and time both look like in­finite col­lec­tions of points—con­tin­u­ous col­lec­tions, which is a sec­ond-or­der con­cept—and then to char­ac­ter­ize the size of that in­finity we’d need sec­ond-or­der logic. I mean, by the Lowen­heim-Skolem the­o­rem, there aren’t just de­nu­mer­able mod­els of first-or­der ax­iom­a­ti­za­tions of the re­als, there’s also uni­mag­in­ably large car­di­nal in­fini­ties which obey the same premises, and that’s a pos­si­bil­ity straight out of H. P. Love­craft. Espe­cially if there are any things hid­ing in the in­visi­ble cracks of space.”

“How could you tell if there were in­ac­cessible car­di­nal quan­tities of points hid­den in­side a straight line? And any­thing that lo­cally looks con­tin­u­ous each time you try to split it at a de­scrib­able point, can be ax­io­m­a­tized by a first-or­der schema for con­ti­nu­ity.”

That brings up an­other point: Who’d re­ally be­lieve that the rea­son Peano ar­ith­metic works on phys­i­cal times, is be­cause that whole in­finite ax­iom schema of in­duc­tion, con­tain­ing for ev­ery Φ a sep­a­rate rule say­ing...

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

...was used to spec­ify our uni­verse? How im­prob­a­ble would it be for an in­finitely long list of rules to be true, if there wasn’t a unified rea­son for all of them? It seems much more likely that the real rea­son first-or­der PA works to de­scribe time, is that all prop­er­ties which are true at a start­ing time and true of the suc­ces­sor of any time where they’re true, are true of all later times; and this gen­er­al­iza­tion over prop­er­ties makes in­duc­tion hold for first-or­der for­mu­las as a spe­cial case. If my na­tive thought pro­cess is first-or­der logic, I wouldn’t see the con­nec­tion be­tween each in­di­vi­d­ual for­mula in the ax­iom schema—it would take sep­a­rate ev­i­dence to con­vince me of each one—they would feel like in­de­pen­dent math­e­mat­i­cal facts. But af­ter do­ing sci­en­tific in­duc­tion over the fact that many prop­er­ties true at zero, with suc­ces­sion pre­serv­ing truth, seem to be true ev­ery­where—af­ter gen­er­al­iz­ing the sim­ple, com­pact sec­ond-or­der the­ory of num­bers and times—then you could in­vent an in­finite first-or­der the­ory to ap­prox­i­mate it.

“Maybe that just says you need to ad­just what­ever the­ory of sci­en­tific in­duc­tion you’re us­ing, so that it can more eas­ily in­duct in­finite ax­iom schemas.”

But why the heck would you need to in­duct in­finite ax­iom schemas in the first place, if Real­ity na­tively ran on first-or­der logic? Isn’t it far more likely that the way we ended up with these in­finite lists of ax­ioms was that Real­ity was man­u­fac­tured—for­give the an­thro­po­mor­phism—that Real­ity was man­u­fac­tured us­ing an un­der­ly­ing schema in which time is a con­nected se­ries of events, and space is a con­tin­u­ous field, and these are prop­er­ties which hap­pen to re­quire sec­ond-or­der logic for hu­mans to de­scribe? I mean, if you picked out first-or­der the­o­ries at ran­dom, what’s the chance we’d end up in­side an in­finitely long ax­iom schema that just hap­pened to look like the pro­jec­tion of a com­pact sec­ond-or­der the­ory? Aren’t we ig­nor­ing a sort of hint?

“A hint to what?”

Well, I’m not that sure my­self, at this depth of philos­o­phy. But I would cur­rently say that find­ing our­selves in a phys­i­cal uni­verse where times have suc­ces­sor times, and space looks con­tin­u­ous, seems like a pos­si­ble hint that the Teg­mark Level IV mul­ti­verse—or the way Real­ity was man­u­fac­tured, or what­ever—might look more like causal uni­verses char­ac­ter­i­z­able by com­pact sec­ond-or­der the­o­ries than causal uni­verses char­ac­ter­i­z­able by first-or­der the­o­ries.

“But since any sec­ond-or­der the­ory can just as eas­ily be in­ter­preted as a many-sorted first-or­der the­ory with quan­tifiers that can range over ei­ther el­e­ments or sets of el­e­ments, how could us­ing sec­ond-or­der syn­tax ac­tu­ally im­prove an Ar­tifi­cial In­tel­li­gence’s abil­ity to han­dle a re­al­ity like that?”

Good ques­tion. One ob­vi­ous an­swer is that the AI would be able to in­duct what you would call an in­finite ax­iom schema, as a sin­gle ax­iom—a sim­ple, finite hy­poth­e­sis.

“There’s all sorts of ob­vi­ous hacks to sci­en­tific in­duc­tion of first-or­der ax­ioms which would let you as­sign nonzero prob­a­bil­ity to com­putable in­finite se­quences of ax­ioms—”

Sure. So be­yond that… I would cur­rently guess that the ba­sic as­sump­tion be­hind ‘be­hav­ing as if’ sec­ond-or­der logic is true, says that the AI should act as if only the ‘ac­tu­ally small­est’ num­bers will ever ap­pear in physics, rel­a­tive to some ‘true’ math­e­mat­i­cal uni­verse that it thinks it lives in, but knows it can’t fully char­ac­ter­ize. Which is roughly what I’d say hu­man math­e­mat­i­ci­ans do when they take sec­ond-or­der logic at face value; they as­sume that there’s some true math­e­mat­i­cal uni­verse in the back­ground, and that sec­ond-or­der logic lets them talk about it.

“And what be­hav­iorally, ex­per­i­men­tally dis­t­in­guishes the hy­poth­e­sis, ‘I live in the true ul­ti­mate math with fully pop­u­lated pow­er­sets’ from the hy­poth­e­sis, ‘There’s some ran­dom model of first-or­der set-the­ory ax­ioms I hap­pen to be liv­ing in’?”

Well… one be­hav­ioral con­se­quence is sus­pect­ing that your time obeys an in­finitely long list of first-or­der ax­ioms with in­duc­tion schemas for ev­ery for­mula. And then more­over be­liev­ing that you’ll never ex­pe­rience a time when a proof-check­ing ma­chine out­puts a proof that Zer­melo-Fraenkel set the­ory is in­con­sis­tent—even though there’s prov­ably some mod­els with times like that, which fit the ax­iom schema you just in­ducted. That sounds like se­cretly be­liev­ing that there’s a back­ground ‘true’ set of num­bers that you think char­ac­ter­izes phys­i­cal time, and that it’s the small­est such set. Another sus­pi­cious be­hav­ior is that as soon as you sus­pect Zer­melo-Fraenkel set the­ory is con­sis­tent, you sud­denly ex­pect not to ex­pe­rience any phys­i­cal time which ZF proves isn’t a stan­dard num­ber. You don’t think you’re in the non­stan­dard time of some weaker the­ory like Peano ar­ith­metic. You think you’re in the min­i­mal time ex­press­ible by any and all the­o­ries, so as soon as ZF can prove some num­ber doesn’t ex­ist in the min­i­mal set, you think that ‘real time’ lacks such a num­ber. All of these sound like be­hav­iors you’d carry out if you thought there was a sin­gle ‘true’ math­e­mat­i­cal uni­verse that pro­vided the best model for de­scribing all phys­i­cal phe­nom­ena, like time and space, which you en­counter—and be­liev­ing that this ‘true’ back­drop used the largest pow­er­sets and small­est num­bers.

“How ex­actly do you for­mal­ize all that rea­son­ing, there? I mean, how would you ac­tu­ally make an AI rea­son that way?”

Er… I’m still work­ing on that part.

“That makes your the­ory a bit hard to crit­i­cize, don’t you think? Per­son­ally, I wouldn’t be sur­prised if any such for­mal­ized rea­son­ing looked just like be­liev­ing that you live in­side a first-or­der set the­ory.”

I sup­pose I wouldn’t be too sur­prised ei­ther—it’s hard to ar­gue with the re­sults on many-sorted log­ics. But if com­pre­hend­ing the phys­i­cal uni­verse is best done by as­sum­ing that real phe­nom­ena are char­ac­ter­ized by a ‘true’ math­e­mat­ics con­tain­ing the pow­er­sets and the nat­u­ral num­bers—and thus ex­pect­ing that no math­e­mat­i­cal model we can for­mu­late will ever con­tain any larger pow­er­sets or smaller num­bers than those of the ‘true’ back­drop to physics—then I’d call that a moral vic­tory for sec­ond-or­der logic. In first-or­der logic we aren’t even sup­posed to be able to talk about such things.

“Really? To me that sounds like be­liev­ing you live in­side a model of first-or­der set the­ory, and be­liev­ing that all mod­els of any the­o­ries you can in­vent must also be sets in the larger model. You can prove the Com­plete­ness The­o­rem in­side ZF plus the Ax­iom of Choice, so ZFC already proves that all con­sis­tent the­o­ries have mod­els which are sets, al­though of course it can’t prove that ZFC it­self is such a the­ory. So—an­thro­po­mor­phi­cally speak­ing—no model of ZFC ex­pects to en­counter a the­ory that has fewer num­bers or larger pow­er­sets than it­self. No model of ZFC ex­pects to en­counter any quoted-model, any set that a quoted the­ory en­tails, which con­tains larger pow­er­sets than the ones in its own Pow­er­set Ax­iom. A first-or­der set the­ory can even make the leap from the finite state­ment, ‘P is true of all my sub­sets of X’, to be­liev­ing, ‘P is true of all my sub­sets of X that can be de­scribed by this de­nu­mer­able col­lec­tion of for­mu­las’ - it can en­com­pass the jump from a sin­gle ax­iom over ‘all my sub­sets’, to a quoted ax­iom schema over for­mu­las. I’d sum all that up by say­ing, ‘sec­ond-or­der logic is how first-or­der set the­ory feels from the in­side’.”

Maybe. Even in the event that nei­ther hu­man nor su­per­in­tel­li­gent cog­ni­tion will ever be able to ‘prop­erly talk about’ un­bounded finite times, global con­nect­ed­ness, par­tic­u­lar in­finite car­di­nal­ities, or true spa­tial con­ti­nu­ity, it doesn’t fol­low that Real­ity is similarly limited in which physics it can priv­ilege.

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

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