# [LINK] Steven Landsburg “Accounting for Numbers”—response to EY’s “Logical Pinpointing”

“I started to post a com­ment, but it got long enough that I’ve turned my com­ment into a blog post.”

So the study of sec­ond-or­der con­se­quences is not logic at all; to tease out all the sec­ond-or­der con­se­quences of your sec­ond-or­der ax­ioms, you need to con­front not just the forms of sen­tences but their mean­ings. In other words, you have to un­der­stand mean­ings be­fore you can carry out the op­er­a­tion of in­fer­ence. But Yud­kowsky is try­ing to de­rive mean­ing from the op­er­a­tion of in­fer­ence, which won’t work be­cause in sec­ond-or­der logic, mean­ing comes first.

… it’s im­por­tant to rec­og­nize that Yud­kowsky has “solved” the prob­lem of ac­count­ing for num­bers only by re­duc­ing it to the prob­lem of ac­count­ing for sets — ex­cept that he hasn’t even done that, be­cause his re­duc­tion re­lies on pre­tend­ing that sec­ond or­der logic is logic.

• It seems to me that a) Lands­burg’s cri­tique is right, b) the prob­lem is still mys­te­ri­ous, c) mak­ing it less mys­te­ri­ous would re­quire a new math­e­mat­i­cal re­sult, d) that fu­ture re­sult is more likely to be nega­tive, like the in­com­plete­ness the­o­rem or un­defin­abil­ity of truth.

• By far the largest crit­i­cism here is the re­quire­ments of set the­ory:

Yud­kowsky is rely­ing on a the­o­rem when he says that sec­ond-or­der Peano ar­ith­metic has a unique model. That the­o­rem re­quires a sub­stan­tial dose of set the­ory. So in or­der to avoid tak­ing num­bers as prim­i­tive ob­jects, he’s effec­tively re­sorted to tak­ing sets as prim­i­tive ob­jects. But why is it any more satis­fy­ing to take set the­ory as “given” than to take num­bers as “given”? In­deed, the for­mal study of num­bers pre­cedes the for­mal study of sets by mil­len­nia, which sug­gests that num­bers are a more nat­u­ral start­ing point than sets are. Whether or not you buy that ar­gu­ment, it’s im­por­tant to rec­og­nize that Yud­kowsky has “solved” the prob­lem of ac­count­ing for num­bers only by re­duc­ing it to the prob­lem of ac­count­ing for sets — ex­cept that he hasn’t even done that, be­cause his re­duc­tion re­lies on pre­tend­ing that sec­ond or­der logic is logic.

This seems most damn­ing in that it makes most of the philo­soph­i­cal is­sues about the na­ture of logic ir­rele­vant.

• I think this cri­tique un­der­val­ues the in­sight sec­ond or­der ar­ith­metic gives for un­der­stand­ing the nat­u­ral num­bers.

If what you wanted from logic was a com­plete, self-con­tained ac­count of math­e­mat­i­cal rea­son­ing then sec­ond or­der ar­ith­metic is a punt: it pur­ports to de­scribe a set of rules for de­scribing the nat­u­ral num­bers, and then in the mid­dle says “Just fill in what­ever you want here, and then go on”. Lands­burg wor­ries that, as a con­se­quence, we haven’t got­ten any­where (or, worse, have started be­hind where we started, since no we need an ac­count of “prop­er­ties” in or­der to have an ac­count of nat­u­ral num­bers).

But, thanks to Gödel, we know that a self-con­tained ac­count of rea­son­ing is im­pos­si­ble. Lands­burg’s an­swer is to give up on rea­son­ing: the nat­u­ral num­bers are just there, and we have an in­tu­itive grasp of them. This is, ob­vi­ously, even more of a punt, and the sec­ond or­der ar­ith­metic ap­proach ac­tu­ally tells us some­thing use­ful about the con­cept of the nat­u­ral num­bers.

Sup­pose some­one pro­duces a proof of a the­o­rem about the nat­u­ral num­bers—let’s say, for speci­fic­ity, they prove the twin primes con­jec­ture (that there are in­finitely many twin primes). This proof pro­ceeds in the fol­low­ing fash­ion: by ex­ten­sive use of the most elab­o­rate ab­stract math you can think of—large car­di­nals and sheafs and an­abelian ge­om­e­try and what­not—the per­son proves the ex­is­tence of a set of nat­u­ral num­bers P such that 1) 0 is in P, 2) if x is in P then x+1 is in P, and 3) if x is in P then there are twin primes greater than x.

Se­cond or­der ar­ith­metic says that this prop­erty P must ex­tend all the way through the nat­u­ral num­bers, and there­fore must it­self be the nat­u­ral num­bers, and so we could con­clude the twin primes con­jec­ture.

The rest of this proof is re­ally com­pli­cated, and uses things you might not think are valid, so you might not buy it. But sec­ond or­der ar­ith­metic de­mands that if you be­lieve the rest of the proof, you should also agree that the twin primes con­jec­ture holds. This is ac­tu­ally worth some­thing: it says that if you and I agree about all the fancy ab­stract stuff, we also have to agree about the nat­u­ral num­bers. And that’s the most we can ask for.

To phrase this differ­ently, sec­ond or­der ar­ith­metic gives us a uni­ver­sal way of pick­ing the nat­u­ral num­bers out in any situ­a­tion. Differ­ent mod­els of set the­ory may end up dis­agree­ing about what’s true in the nat­u­ral num­bers, but sec­ond or­der ar­ith­metic is a con­sis­tent way of iden­ti­fy­ing the no­tion in that model of set the­ory which lines up with our in­tu­itions for the what the nat­u­ral num­bers are. That’s a very differ­ent ac­count than the one offered by first or­der logic, but it’s a valuable one in its own right.

One more phras­ing, just for thor­ough­ness. Lands­burg passes off an ac­count of the nat­u­ral num­bers to Pla­ton­ism: we just in­tuit the nat­u­ral num­bers. But sup­pose you and I both pur­port to have good in­tu­itions of the nat­u­ral num­bers, but we seem to dis­agree about some prop­erty. So we sit down to hash this out; it might turn out that we have some dis­agree­ment about what con­sti­tutes valid math­e­mat­i­cal rea­son­ing, in which case we may be stuck. But if not—if we agree on the rea­son­ing—then even­tu­ally the dis­agree­ment will boil down to some­thing like this:

You: “And since 0 is turquoise and, when­ever x is turquoise, x+1 is also turquoise, all the nat­u­ral num­bers are turquoise.”

Me: “Wait, those aren’t all the nat­u­ral num­bers. Those are just the small nat­u­ral num­bers.”

You: “What? What are the small nat­u­ral num­bers?”

Me: “You know, the ini­tial seg­ment of the nat­u­ral num­bers closed un­der the prop­erty of be­ing turquoise.”

You: “There’s an ini­tial seg­ment of the nat­u­ral num­bers which in­cludes 0, is closed un­der adding 1, but isn’t ev­ery nat­u­ral num­ber?”

Me: “Sure. The small nat­u­ral num­bers. Haven’t you heard of them?”

You: “Wait, are there any ini­tial seg­ments of the small nat­u­ral num­bers which in­clude 0 and are closed un­der adding 1?”

Me: “Sure. The tiny nat­u­ral num­bers, for starters.”

You: “Look, you’re us­ing the word ‘nat­u­ral num­bers’ wrong. It means...” and then you ex­plain the sec­ond or­der in­duc­tion ax­iom. So ap­par­ently what­ever I thought was the nat­u­ral num­bers was some other biz­zarre ob­ject; what the sec­ond or­der in­duc­tion ax­iom does for a Pla­ton­ist is pin down which Pla­tonic ob­ject we’re ac­tu­ally talk­ing about.

• I dis­agree with your ex­am­ple:

The rest of this proof is re­ally com­pli­cated, and uses things you might not think are valid, so you might not buy it. But sec­ond or­der ar­ith­metic de­mands that if you be­lieve the rest of the proof, you should also agree that the twin primes con­jec­ture holds.

But set the­ory says the same thing. And set the­ory, un­like sec­ond-or­der ar­ith­metic, is prob­a­bly strong enough to for­mal­ize the large and com­pli­cated proof in the first place. Even if there are el­e­ments in the proof that go be­yond ZFC (large car­di­nals etc.), math­e­mat­i­ci­ans are likely to view them as ad­di­tional as­sump­tions on top of what they see as set the­ory.

Con­sider a non-lo­gi­cian math­e­mat­i­cian to whom the in­duc­tion prin­ci­ple is not pri­mar­ily a for­mal state­ment to be an­a­lyzed, but just, well, in­duc­tion, a ba­sic work­ing tool. Given a large proof as you de­scribe, end­ing in an ap­pli­ca­tion of in­duc­tion. What would be the benefit, to the math­e­mat­i­cian, of view­ing that ap­pli­ca­tion as hap­pen­ing in sec­ond-or­der logic, as op­posed to first-or­der set the­ory? Why would they want to use sec­ond-or­der any­thing?

To phrase this differ­ently, sec­ond or­der ar­ith­metic gives us a uni­ver­sal way of pick­ing the nat­u­ral num­bers out in any situ­a­tion. Differ­ent mod­els of set the­ory may end up dis­agree­ing about what’s true in the nat­u­ral num­bers, but sec­ond or­der ar­ith­metic is a con­sis­tent way of iden­ti­fy­ing the no­tion in that model of set the­ory which lines up with our in­tu­itions for the what the nat­u­ral num­bers are.

I don’t see how that works, ei­ther.

Let G be the ar­ith­meti­cal state­ment ex­press­ing the con­sis­tency of ZFC. There are mod­els of set the­ory in which G is true, and mod­els in which G is false. Are you say­ing that sec­ond-or­der ar­ith­metic gives us a bet­ter way, a less am­bigu­ous way, to study the truth of G? How would that work in prac­tice?

The way I see it, differ­ent mod­els of set the­ory agree on what nat­u­ral num­bers are, but dis­agree on what sub­sets of nat­u­ral num­bers ex­ist. This am­bi­guity is not re­solved by sec­ond-or­der ar­ith­metic; rather, it’s swept un­der the car­pet. The “unique” model “pin­pointed” by it is ut­terly at the mercy of the same am­bi­guity of what the set of sub­sets of N is, and the am­bi­guity re­asserts it­self the mo­ment you start study­ing the se­man­tics of sec­ond-or­der ar­ith­metic which you will do through model the­ory, ex­pressed within set the­ory. So what is it that you have gained?

So ap­par­ently what­ever I thought was the nat­u­ral num­bers was some other biz­zarre ob­ject; what the sec­ond or­der in­duc­tion ax­iom does for a Pla­ton­ist is pin down which Pla­tonic ob­ject we’re ac­tu­ally talk­ing about.

To a Pla­ton­ist, what you used was not the sec­ond or­der in­duc­tion ax­iom; it was just the fa­mil­iar prin­ci­ple of in­duc­tion.

• I think you’re read­ing too much into what I’m say­ing. I’m not sug­gest­ing that sec­ond or­der ar­ith­metic is use­ful as a math­e­mat­i­cal frame­work to talk about rea­son­ing, in the way that first-or­der logic can. I’m say­ing that sec­ond or­der ar­ith­metic is a use­ful way to talk about what makes the nat­u­ral num­bers spe­cial.

I’m also not sug­gest­ing that sec­ond or­der ar­ith­metic has any­thing deep to add rel­a­tive to a naïve (but suffi­ciently ab­stract) un­der­stand­ing of in­duc­tion, but given that many peo­ple don’t have a suffi­ciently ab­stract un­der­stand­ing of in­duc­tion, I think it use­fully illus­trates just how broadly in­duc­tion has to be un­der­stood. (To be clear, I’m also not sug­gest­ing that sec­ond or­der ar­ith­metic is the one true way to think about the nat­u­ral num­bers, only that it’s a use­ful per­spec­tive.)

Con­sider a non-lo­gi­cian math­e­mat­i­cian to whom the in­duc­tion prin­ci­ple is not pri­mar­ily a for­mal state­ment to be an­a­lyzed, but just, well, in­duc­tion, a ba­sic work­ing tool. Given a large proof as you de­scribe, end­ing in an ap­pli­ca­tion of in­duc­tion. What would be the benefit, to the math­e­mat­i­cian, of view­ing that ap­pli­ca­tion as hap­pen­ing in sec­ond-or­der logic, as op­posed to first-or­der set the­ory? Why would they want to use sec­ond-or­der any­thing?

I’m not claiming there is any such benefit. This is the wrong ques­tion to ask; nei­ther Eliezer’s origi­nal post nor my com­ment were writ­ten for an au­di­ence of math­e­mat­i­ci­ans con­cerned with the op­ti­mal way to do math­e­mat­ics in prac­tice.

Let G be the ar­ith­meti­cal state­ment ex­press­ing the con­sis­tency of ZFC. There are mod­els of set the­ory in which G is true, and mod­els in which G is false. Are you say­ing that sec­ond-or­der ar­ith­metic gives us a bet­ter way, a less am­bigu­ous way, to study the truth of G?

No, I am not say­ing that.

The way I see it, differ­ent mod­els of set the­ory agree on what nat­u­ral num­bers are, but dis­agree on what sub­sets of nat­u­ral num­bers ex­ist.

If there are mod­els where G is true and mod­els where G is false then differ­ent mod­els of set the­ory don’t agree on what nat­u­ral num­bers are.

This am­bi­guity is not re­solved by sec­ond-or­der ar­ith­metic; rather, it’s swept un­der the car­pet. The “unique” model “pin­pointed” by it is ut­terly at the mercy of the same am­bi­guity of what the set of sub­sets of N is, and the am­bi­guity re­asserts it­self the mo­ment you start study­ing the se­man­tics of sec­ond-or­der ar­ith­metic which you will do through model the­ory, ex­pressed within set the­ory. So what is it that you have gained?

No, the am­bi­guity is not re­solved by sec­ond-or­der ar­ith­metic. The am­bi­guity is not re­solved by any­thing, so that doesn’t seem like a very use­ful ob­jec­tion.

Also, note that I didn’t re­fer to ei­ther a unique model nor to pin­point­ing. (I’m aware that Eliezer did, but you’re re­ply­ing to me.) What I said was: “[S]econd or­der ar­ith­metic gives us a uni­ver­sal way of pick­ing the nat­u­ral num­bers out in any situ­a­tion. Differ­ent mod­els of set the­ory may end up dis­agree­ing about what’s true in the nat­u­ral num­bers, but sec­ond or­der ar­ith­metic is a con­sis­tent way of iden­ti­fy­ing the no­tion in that model of set the­ory which lines up with our in­tu­itions for the what the nat­u­ral num­bers are”

• ...some other biz­zarre ob­ject...

I ob­ject to the no­tion that the hy­per­nat­u­rals are bizarre. Down with ω-con­sis­tency!

/​geek

• Heh—I’m amazed at how many things in this post I al­ter­nately strongly agree or strongly dis­agree with.

It’s im­por­tant to dis­t­in­guish be­tween the nu­meral “2″, which is a for­mal sym­bol de­signed to be ma­nipu­lated ac­cord­ing to for­mal rules, and the noun “two”, which ap­pears to name something

OK… I hon­estly can’t com­pre­hend how some­one could si­mul­ta­neously be­lieve that “2” is just a sym­bol and that “two” is a blob of pure mean­ing. It sug­gests the in­fer­en­tial dis­tances are ac­tu­ally pretty great here de­spite a lot of sur­face similar­i­ties be­tween what Lands­burg is say­ing and what I would say.

In­stead, the point of the Peano ax­ioms was to model what math­e­mat­i­ci­ans do when they’re talk­ing about numbers

I’m happy with this (al­though the next sen­tence sug­gests I may have been mis­in­ter­pret­ing it slightly). Another way I would put it is that the Peano ax­ioms are about mak­ing things pre­cise and get­ting ev­ery­one to agree to the same rules so that they ar­gue fairly.

Like all good mod­els, the Peano ax­ioms are a sim­plifi­ca­tion that cap­tures im­por­tant as­pects of re­al­ity with­out at­tempt­ing to re­pro­duce re­al­ity in de­tail.

I’d like an ex­am­ple here.

I’d prob­a­bly start with some­thing like Ber­trand Rus­sell’s ac­count of num­bers: We say that two sets of ob­jects are “equinu­mer­ous” if they can be placed in one-one cor­re­spon­dence with each other

This is defin­ing num­bers in terms of sets, which he ex­plic­itly crit­i­cizes Yud­kowsky for later. I’ll take the char­i­ta­ble in­ter­pre­ta­tion though, which would be “Y thinks he can some­how avoid defin­ing num­bers in terms of sets… which it turns out he can’t… so if you’re go­ing to do that any­way you may as well take the more straight­for­ward Rus­sell ap­proach”

the whole point of logic is that it is a me­chan­i­cal sys­tem for de­riv­ing in­fer­ences from as­sump­tions, based on the forms of sen­tences with­out any refer­ence to their meanings

I re­ally like this defi­ni­tion of logic! It doesn’t seem to be com­pletely stan­dard though, and Yud­kowksy is us­ing it in the more gen­eral sense of valid rea­son­ing. So this point is ba­si­cally about the se­man­tics of the word “logic”.

But Yud­kowsky is try­ing to de­rive mean­ing from the op­er­a­tion of in­fer­ence, which won’t work be­cause in sec­ond-or­der logic, mean­ing comes first.

I think this is a slight straw­man­ning of Yud­kowsky. Here Yud­kowsky is try­ing to define the mean­ing of one par­tic­u­lar sys­tem—the nat­u­ral num­bers—not define the en­tire con­cept of mean­ing.

he’s effec­tively re­sorted to tak­ing sets as prim­i­tive objects

So when study­ing logic, model the­ory etc. we have to make a dis­tinc­tion be­tween the sys­tem of rea­son­ing that we are study­ing and “meta-rea­son­ing”. Meta-rea­son­ing can be done in nat­u­ral lan­guage or in for­mal math­e­mat­ics—gen­er­ally I pre­fer when it’s a bit more mathy be­cause of the thing of pre­ci­sion/​agree­ing to play by the rules that I men­tioned ear­lier. I don’t see math and nat­u­ral lan­guage as op­er­at­ing at differ­ent lev­els of ab­strac­tion though—clearly Lands­burg dis­agrees (with the whole 2/​two thing) but it’s hard for me to un­der­stand why.

Any­way, if you’re do­ing model the­ory then your meta-rea­son­ing in­volves sets. If you use nat­u­ral lan­guage in­stead though, you’re prob­a­bly still us­ing sets at least by im­pli­ca­tion.

full-fledged Pla­tonic acknowledgement

I think this is what us­ing nat­u­ral lan­guage as your meta-rea­son­ing feels like from the in­side. Lands­burg would say that the nat­u­ral num­bers ex­ist and that “two” refers to a par­tic­u­lar one; in model the­ory this would be “there ex­ists a model N with such-and-such prop­er­ties, and we have a map­ping from sym­bols “0”, “1“, “2” etc. to el­e­ments of N”.

It seems enor­mou­osly more plau­si­ble to me that numbes are “just out there” than that phys­i­cal ob­jects are “just out there”

So he’s say­ing that the ex­is­tence of num­bers im­plies the ex­is­tence of the phys­i­cal uni­verse, and there­fore that the ex­is­tence of num­bers is more likely?? Or is there some qual­ity of “just out there”ness that’s dis­tinct from ex­is­tence?

• This is defin­ing num­bers in terms of sets

But we don’t need to use the full strength of set the­ory (or any­thing like it), so it might still be an im­prove­ment. Though I think there are still other prob­lems.

• math­e­mat­i­ci­ans from Pythago­ras through Dedekind had ab­solutely no prob­lem talk­ing about num­bers in the ab­sence of the Peano ax­ioms.

So, they were lucky. It could have been that that-which-Pythago­ras-calls-num­ber was not that-which-Fibonacci-calls-num­bers.

Are there ab­solutely no ex­am­ples of cases where math­e­mat­i­ci­ans dis­agreed about some the­o­rem about some not-yet-ax­io­m­a­tized sub­ject, and then it turns out the dis­agree­ment was be­cause they were ac­tu­ally talk­ing about differ­ent things?

(I know of no such ex­am­ples, but I would be sur­prised it none ex­ist)

• Are there ab­solutely no ex­am­ples of cases where math­e­mat­i­ci­ans dis­agreed about some the­o­rem about some not-yet-ax­io­m­a­tized sub­ject, and then it turns out the dis­agree­ment was be­cause they were ac­tu­ally talk­ing about differ­ent things?

There is such an ex­am­ple—rather more com­pli­cated than you’re de­scribing, but the same sort of thing: Euler’s the­o­rem about poly­he­dra, be­fore ge­om­e­try was for­mal­ised. This is the the­o­rem that F-E+V = 2, where F, E, and V are the num­bers of faces, edges, and ver­tices of a poly­he­dron. What is a poly­he­dron?

Lakatos’s book “Proofs and Re­fu­ta­tions” con­sists of a his­tory of this prob­lem in which var­i­ous “odd” poly­he­dra were in­vented and the defi­ni­tion of a poly­he­dron cor­re­spond­ingly re­fined, un­til reach­ing the pre­sent un­der­stand­ing of the the­o­rem.

• Upvoted for “Proofs and Re­fu­ta­tions” reference

• I don’t know if this is true, but I once had a lec­turer tell me that there used to be con­sid­er­able de­bate over the ques­tion of whether a deriva­tive of a differ­en­tiable func­tion was nec­es­sar­ily con­tin­u­ous, which ul­ti­mately boiled down to the two sides hav­ing differ­ent defi­ni­tions of con­ti­nu­ity, but not re­al­is­ing it since nei­ther had ever fully set down their ax­ioms and defi­ni­tions.

• I’ve heard that be­fore also but haven’t seen a source for it. But keep in mind that that’s a ques­tion about func­tions on the real num­bers, not about what is be­ing called “num­bers” here which seems to be a sub­sti­tute for the in­te­gers or the nat­u­ral num­bers.

• I thought he was ask­ing if it had ever hap­pened in any not-yet-ax­io­ma­tised sub­ject, pre­sum­ably look­ing for ex­am­ples other than ar­ith­metic.

• Yes. I think the math­e­mat­i­ci­ans were lucky that it didn’t hap­pen on the sort of in­te­gers they were dis­cussing (there was, af­ter all, great dis­cus­sion about ir­ra­tional num­bers, zero , later imag­i­nary num­bers, and even Archimedes’ at­tempt to de­scribe big in­te­gers was prob­a­bly not with­out con­tro­versy ).

• Hmm, in that case, it might be rele­vant to point out ex­am­ples that don’t quite fit Plas­mon’s situ­a­tion but are al­most the same: There are a va­ri­ety of ex­am­ples where due to a lack of rigor­ous ax­iom­a­ti­za­tion, state­ments were be­lieved to be true that just turned out to be false. One clas­si­cal ex­am­ple is the idea that of a func­tion con­tin­u­ous on an in­ter­val and nowhere differ­en­tiable. Every­one took for granted that for granted that a con­tin­u­ous func­tion could only fail differ­en­tia­bil­ity at iso­lated points un­til Weier­strass showed oth­er­wise.

• For an­other one, Rus­sell’s para­dox seems like it was a con­se­quence naively as­sum­ing our in­tu­itions about what counts as a ‘set’ would nec­es­sar­ily be cor­rect, or even in­ter­nally con­sis­tent.

• Plas­mon:

So, they were lucky. It could have been that that-which-Pythago­ras-calls-num­ber was not that-which-Fibonacci-calls-num­bers.

Why do you imag­ine that the in­tro­duc­tion of an ax­io­matic sys­tem would ad­dress this prob­lem?

• To quote, just put a greater-than sign `>` at the be­gin­ning of the first line.

• Why do you imag­ine that the in­tro­duc­tion of an ax­io­matic sys­tem would ad­dress this prob­lem?

Be­cause then the prob­lem is not “Does this non-ax­io­m­a­tized stuff obey that the­o­rem ?” but “Does that the­o­rem fol­low from these ax­ioms ?”. One is a pure logic prob­lem, and proofs may be checked by au­to­mated proof-check­ers. The other di­rectly or in­di­rectly re­lies on the math­e­mat­i­cian’s in­tu­ition of the non-ax­io­m­a­tized sub­ject in ques­tion, and can’t be checked by au­to­mated proof-check­ers.

• Be­cause then the prob­lem is not “Does this non-ax­io­m­a­tized stuff obey that the­o­rem ?” but “Does that the­o­rem fol­low from these ax­ioms ?”. One is a pure logic prob­lem, and proofs may be checked by au­to­mated proof-check­ers. The other di­rectly or in­di­rectly re­lies on the math­e­mat­i­cian’s in­tu­ition of the non-ax­io­m­a­tized sub­ject in ques­tion, and can’t be checked by au­to­mated proof-check­ers.

Ex­cept in­so­far as the math­e­mat­i­ci­ans, un­known to each other, have differ­ent ideas of what con­sti­tutes a valid rule of in­fer­ence.

A log­i­cal sys­tem is a math­e­mat­i­cal obect. If the prob­lem is that differ­ent math­e­mat­i­ci­ans might think they’re talk­ing about the same ob­ject when they’re re­ally talk­ing about differ­ent ones, then I don’t see why log­i­cal sys­tems, out of all math­e­mat­i­cal ob­jects, should be par­tic­u­larly ex­empt from this prob­lem.

Also, of course, to put this in the con­text of the origi­nal post, if we’re talk­ing about sec­ond or­der logic, then of course there can be no au­to­mated proof-check­ers.

• Also, of course, to put this in the con­text of the origi­nal post, if we’re talk­ing about sec­ond or­der logic, then of course there can be no au­to­mated proof-check­ers.

You ap­pear to be con­fused here. The rest of your post is good.

• I should have said this more care­fully. If one al­lows enough rules of in­fer­ence so that all the log­i­cal con­se­quences of the ax­ioms can be proved, then there are no au­to­mated proof check­ers. So you can have proof check­ers, but only at the cost of re­strict­ing the sys­tem so that not all log­i­cal con­se­quences (i.e. im­pli­ca­tions that are true in ev­ery model) can be proved.

• I think there’s a defi­ni­tional is­sue here. Eug­ine is us­ing “proof checker” to mean an al­gorithm that given a se­quence of state­ments in an ax­io­matic sys­tem ver­ifies that the proof is for­mally valid. You seem to mean by proof checker some­thing like a pro­cess that goes through list­ing all valid state­ments in the sys­tem along with a proof of the state­ment.

• JoshuaZ: No, I mean the former. The prob­lem is that you have enough rules of in­fer­ence to al­low you to ex­tract all log­i­cal con­se­quences of your ax­ioms, then that set of rules of in­fer­ence is go­ing to be too com­pli­cated to ex­plain to any com­puter. (i.e. the rules of in­fer­ence are non-re­cur­sive.)

• Isn’t that more a con­se­quence of the stronger state­ment that you just can’t write down all valid in­fer­ences in the sec­ond-or­der sys­tem?

• Do you mean that there can be no au­to­mated proof-check­ers which are sound and com­plete (and ter­mi­nat­ing)? Surely there can be use­ful sound check­ers (which ter­mi­nate)? The ex­is­tence of Coq and other Depen­dently typed lan­guages sug­gests that’s true.

• LessWrong uses Mark­down for com­ment for­mat­ting. Click the but­ton la­bel­led “Show help” un­der the right-hand side of the com­ment box.

• Well, that would’ve worked fine in stan­dard Mark­down.

• What is “stan­dard Mark­down”?

• Speci­fied here—I think it is canon­i­cally pro­duced by `Mark­down.pl`, down­load­able there.

Notably, Mark­down al­lows in­line html. Most im­ple­men­ta­tions that work with client data, like that of Red­dit/​Lw, only al­low a limited sub­set of Mark­down func­tion­al­ity. (Most also add func­tion­al­ity).

• Oh, I see—a speci­fi­ca­tion in the style of “only perl can parse perl.”

But then these “most im­ple­men­ta­tions” are not im­ple­men­ta­tions of “stan­dard Mark­down,” hence my con­fu­sion.

• Oh, I see—a speci­fi­ca­tion in the style of “only perl can parse perl.”

All uni­ver­sal pro­gram­ming lan­guages (as­sem­bler, C, CLIP, Lisp, Cobol, Python, Java) can parse perl as well.

• All uni­ver­sal pro­gram­ming lan­guages (as­sem­bler, C, CLIP, Lisp, Cobol, Python, Java) can parse perl as well.

Only if they im­ple­ment Perl, perfectly mimick­ing the func­tion­al­ity of `perl` (the only spec for Perl). Amongst other difficul­ties, Perl has available the full power of Perl at the pre­pro­cess­ing stage.

• That doesn’t mat­ter, kind of like non-pa­per­clips.

• But then these “most im­ple­men­ta­tions” are not im­ple­men­ta­tions of “stan­dard Mark­down,”

Note the qual­ifier—“most im­ple­men­ta­tions that work with client data”. Mark­down is also used ex­ten­sively to gen­er­ate static con­tent that is not user-gen­er­ated.

• There are still mul­ti­ple im­ple­men­ta­tions used in gen­er­at­ing static con­tent, no two of which re­ally do the same thing, e.g., pan­doc, mul­ti­mark­down, and etc. Th­ese are all still ar­guably “mark­down” (at least, they call them­selves that) but don’t con­form to stan­dard mark­down as you un­der­stand it.

• Con­sider also the par­allel ‘pos­tu­late’, re­luc­tantly in­tro­duced as an ax­iom in Eu­clid. Peo­ple tried to prove it as a the­o­rem for two thou­sand years, un­til it was re­al­ized that its nega­tion defined en­tirely differ­ent kinds of ge­om­e­try.

• A not-quite-but-close fit: the dis­tinc­tion be­tween prime and ir­re­ducible el­e­ments of a num­ber field be­came nec­es­sary be­cause unique fac­tor­iza­tion into primes failed in sim­ple num­ber fields.

• Var­i­ous the­o­rems, lem­mas, and other prin­ci­ples equiv­a­lent to the Ax­iom of Choice (e.g. Zorn’s lemma) were ar­gued over un­til it was es­tab­lished (by Kurt Gödel and Paul Co­hen) that the AoC is en­tirely in­de­pen­dent of the ZF ax­ioms, i.e. ZFC and ZF!C are both con­sis­tent sys­tems. I think this is the canon­i­cal ex­am­ple.

“The Ax­iom of Choice is ob­vi­ously true, the well-or­der­ing prin­ci­ple ob­vi­ously false, and who can tell about Zorn’s lemma?” — Jerry Bona

• 16 Nov 2012 15:58 UTC
1 point

From Lands­burg’s “Ac­count­ing for Num­bers,” point 9:

num­bers are in­deed just “out there” and that they are di­rectly ac­cessible to our in­tu­itions.

[Em­pha­sis mine.]

I’m con­flicted on whether to think the world is ac­tu­ally phys­i­cal in a spe­cial way, or sim­ply math­e­mat­i­cal in such a way that all math­e­mat­i­cal struc­tures ex­ist and are equally real. My great­est stick­ing point to ac­cept­ing the lat­ter po­si­tion is the em­pha­sized part of the quote.

Okay, if I grant that num­bers are “out there,” we do seem to in­ter­act with them via a cog­ni­tive al­gorithm we call “in­tu­ition.” But how the heck does that work!? Noth­ing I know about cog­ni­tive sci­ence sug­gests that in­tu­itions are some­how spe­cially equipped to in­ter­act with num­bers, or are fun­da­men­tally differ­ent than the brain’s other cog­ni­tive al­gorithms.

The crux of the ar­gu­ment for a math­e­mat­i­cal uni­verse—so far as I un­der­stand it—is par­si­mony. But in or­der for par­si­mony to be the rele­vant crite­ria, both hy­pothe­ses need have the same ex­per­i­men­tal pre­dic­tions. In other words, if the math­e­mat­i­cal uni­verse hy­poth­e­sis is cor­rect, we would ex­pect it to be con­sis­tent with our non-math­e­mat­i­cal uni­verse un­der­stand­ing of cog­ni­tive sci­ence. But with re­spect to in­tu­itions, this doesn’t seem to be the case.

Without hav­ing a satis­fy­ing ac­count of how in­tu­itions work in a math­e­mat­i­cal uni­verse, the MUH isn’t con­sis­tent with my cur­rent un­der­stand­ing of re­al­ity. Is there such an ex­pla­na­tion of in­tu­itions? If not, maybe a more fruit­ful ques­tion to ask might be:

What kind of cog­ni­tive al­gorithms gen­er­ate the feel­ing that num­bers are “out there”?

• What kind of cog­ni­tive al­gorithms gen­er­ate the feel­ing that num­bers are “out there”?

Per­haps the same sorts that gen­er­ate feel­ings like ‘lines and edges are out there’ or that ‘we say dis­tinct words’ (rather than con­tin­u­ously slurred to­gether sounds) or which leads to http://​​en.wikipe­dia.org/​​wiki/​​Subitizing

• Is there re­ally that much differ­ence be­tween Se­cond Order Logic, and First Order Logic quan­tify­ing over sets, or over classes?

Put it an­other way, Eliezer is us­ing SOL to pin­point the con­cept of a (nat­u­ral) “num­ber”. But to do that thor­oughly he also needs to pin­point the con­cept of a “prop­erty” or a “set” of num­bers with that prop­erty, so he needs some ax­ioms of set the­ory. And those set the­ory ax­ioms had bet­ter be in FOL, be­cause if they are also in SOL he will fur­ther need to pin­point prop­er­ties of sets (or proper classes of sets), so he needs some ax­ioms of class the­ory. Some­where it all bot­toms out in FOL, doesn’t it?

• Why isn’t it nec­es­sary to pin point FOL?

• Well, the topic is “log­i­cal pin­point­ing”, and the at­tempt to log­i­cally pin­point logic it­self sounds rather cir­cu­lar...

How­ever, if we re­ally want to, we can de­scribe a com­puter pro­gram which sys­tem­at­i­cally checks any given in­put string to de­cide whether it con­sti­tutes a valid string of de­duc­tions in FOL. Then “first or­der logic” is any­thing to which the pro­gram gives the an­swer “Valid”. That’s pos­si­ble for FOL, but not for SOL. If you want to fur­ther pin­point what a “pro­gram” is, the best way to do that is to find a com­puter and run the d**n thing!

• I agree with pretty much all of Lands­burg’s crit­i­cisms. We’ve raised similar points be­fore.