# Godel’s Completeness and Incompleteness Theorems

Fol­lowup to: Stan­dard and Non­stan­dard Numbers

So… last time you claimed that us­ing first-or­der ax­ioms to rule out the ex­is­tence of non­stan­dard num­bers—other chains of num­bers be­sides the ‘stan­dard’ num­bers start­ing at 0 - was for­ever and truly im­pos­si­ble, even unto a su­per­in­tel­li­gence, no mat­ter how clever the first-or­der logic used, even if you came up with an en­tirely differ­ent way of ax­io­m­a­tiz­ing the num­bers.

“Right.”

How could you, in your finite­ness, pos­si­bly know that?

“Have you heard of Godel’s In­com­plete­ness The­o­rem?”

Of course! Godel’s The­o­rem says that for ev­ery con­sis­tent math­e­mat­i­cal sys­tem, there are state­ments which are true within that sys­tem, which can’t be proven within the sys­tem it­self. Godel came up with a way to en­code the­o­rems and proofs as num­bers, and wrote a purely nu­mer­i­cal for­mula to de­tect whether a proof obeyed proper log­i­cal syn­tax. The ba­sic trick was to use prime fac­tor­iza­tion to en­code lists; for ex­am­ple, the or­dered list <3, 7, 1, 4> could be uniquely en­coded as:

23 * 37 * 51 * 74

And since prime fac­tor­iza­tions are unique, and prime pow­ers don’t mix, you could in­spect this sin­gle num­ber, 210,039,480, and get the unique or­dered list <3, 7, 1, 4> back out. From there, go­ing to an en­cod­ing for log­i­cal for­mu­las was easy; for ex­am­ple, you could use the 2 pre­fix for NOT and the 3 pre­fix for AND and get, for any for­mu­las Φ and Ψ en­coded by the num­bers #Φ and #Ψ:

¬Φ = 22 * 3

Φ ∧ Ψ = 23 * 3 * 5

It was then pos­si­ble, by dint of crazy amounts of work, for Godel to come up with a gi­gan­tic for­mula of Peano Arith­metic [](p, c) mean­ing, ‘P en­codes a valid log­i­cal proof us­ing first-or­der Peano ax­ioms of C’, from which di­rectly fol­lowed the for­mula []c, mean­ing, ‘There ex­ists a num­ber P such that P en­codes a proof of C’ or just ‘C is prov­able in Peano ar­ith­metic.’

Godel then put in some fur­ther clever work to in­vent state­ments which referred to them­selves, by hav­ing them con­tain sub-recipes that would re­pro­duce the en­tire state­ment when ma­nipu­lated by an­other for­mula.

And then Godel’s State­ment en­codes the state­ment, ‘There does not ex­ist any num­ber P such that P en­codes a proof of (this state­ment) in Peano ar­ith­metic’ or in sim­pler terms ‘I am not prov­able in Peano ar­ith­metic’. If we as­sume first-or­der ar­ith­metic is con­sis­tent and sound, then no proof of this state­ment within first-or­der ar­ith­metic ex­ists, which means the state­ment is true but can’t be proven within the sys­tem. That’s Godel’s The­o­rem.

“Er… no.”

No?

“No. I’ve heard ru­mors that Godel’s In­com­plete­ness The­o­rem is hor­ribly mi­s­un­der­stood in your Everett branch. Have you heard of Godel’s Com­plete­ness The­o­rem?”

Is that a thing?

Yes! Godel’s Com­plete­ness The­o­rem says that, for any col­lec­tion of first-or­der state­ments, ev­ery se­man­tic im­pli­ca­tion of those state­ments is syn­tac­ti­cally prov­able within first-or­der logic. If some­thing is a gen­uine im­pli­ca­tion of a col­lec­tion of first-or­der state­ments—if it ac­tu­ally does fol­low, in the mod­els pinned down by those state­ments—then you can prove it, within first-or­der logic, us­ing only the syn­tac­ti­cal rules of proof, from those ax­ioms.”

I don’t see how that could pos­si­bly be true at the same time as Godel’s In­com­plete­ness The­o­rem. The Com­plete­ness The­o­rem and In­com­plete­ness The­o­rem seem to say di­a­met­ri­cally op­po­site things. Godel’s State­ment is im­plied by the ax­ioms of first-or­der ar­ith­metic—that is, we can see it’s true us­ing our own math­e­mat­i­cal rea­son­ing -

“Wrong.”

What? I mean, I un­der­stand we can’t prove it within Peano ar­ith­metic, but from out­side the sys­tem we can see that -

All right, ex­plain.

“Ba­si­cally, you just com­mit­ted the equiv­a­lent of say­ing, ‘If all kit­tens are lit­tle, and some lit­tle things are in­no­cent, then some kit­tens are in­no­cent.’ There are uni­verses—log­i­cal mod­els—where it so hap­pens that the premises are true and the con­clu­sion also hap­pens to be true:”

“But there are also valid mod­els of the premises where the con­clu­sion is false:”

“If you, your­self, hap­pened to live in a uni­verse like the first one—if, in your mind, you were only think­ing about a uni­verse like that—then you might mis­tak­enly think that you’d proven the con­clu­sion. But your state­ment is not log­i­cally valid, the con­clu­sion is not true in ev­ery uni­verse where the premises are true. It’s like say­ing, ‘All ap­ples are plants. All fruits are plants. There­fore all ap­ples are fruits.’ Both the premises and the con­clu­sions hap­pen to be true in this uni­verse, but it’s not valid logic.”

Okay, so how does this in­val­i­date my pre­vi­ous ex­pla­na­tion of Godel’s The­o­rem?

“Be­cause of the non-stan­dard mod­els of first-or­der ar­ith­metic. First-or­der ar­ith­metic nar­rows things down a lot—it rules out 3-loops of non­stan­dard num­bers, for ex­am­ple, and man­dates that ev­ery model con­tain the num­ber 17 - but it doesn’t pin down a sin­gle model. There’s still the pos­si­bil­ity of in­finite-in-both-di­rec­tions chains com­ing af­ter the ‘stan­dard’ chain that starts with 0. Maybe you have just the stan­dard num­bers in mind, but that’s not the only pos­si­ble model of first-or­der ar­ith­metic.”

So?

“So in some of those other mod­els, there are non­stan­dard num­bers which—ac­cord­ing to Godel’s ar­ith­meti­cal for­mula for en­codes-a-proof—are ‘non­stan­dard proofs’ of Godel’s State­ment. I mean, they’re not what we would call ac­tual proofs. An ac­tual proof would have a stan­dard num­ber cor­re­spond­ing to it. A non­stan­dard proof might look like… well, it’s hard to en­vi­sion, but it might be some­thing like, ‘Godel’s state­ment is true, be­cause not-not-Godel’s state­ment, be­cause not-not-not-not-Godel’s state­ment’, and so on go­ing back­ward for­ever, ev­ery step of the proof be­ing valid, be­cause non­stan­dard num­bers have an in­finite num­ber of pre­de­ces­sors.”

And there’s no way to say, ‘You can’t have an in­finite num­ber of deriva­tions in a proof’?

“Not in first-or­der logic. If you could say that, you could rule out num­bers with in­finite num­bers of pre­de­ces­sors, mean­ing that you could rule out all in­finite-in-both-di­rec­tions chains, and hence rule out all non­stan­dard num­bers. And then the only re­main­ing model would be the stan­dard num­bers. And then Godel’s State­ment would be a se­man­tic im­pli­ca­tion of those ax­ioms; there would ex­ist no num­ber en­cod­ing a proof of Godel’s State­ment in any model which obeyed the ax­ioms of first-or­der ar­ith­metic. And then, by Godel’s Com­plete­ness The­o­rem, we could prove Godel’s State­ment from those ax­ioms us­ing first-or­der syn­tax. Be­cause ev­ery gen­uinely valid im­pli­ca­tion of any col­lec­tion of first-or­der ax­ioms—ev­ery first-or­der state­ment that ac­tu­ally does fol­low, in ev­ery pos­si­ble model where the premises are true—can always be proven, from those ax­ioms, in first-or­der logic. Thus, by the com­bi­na­tion of Godel’s In­com­plete­ness The­o­rem and Godel’s Com­plete­ness The­o­rem, we see that there’s no way to uniquely pin down the nat­u­ral num­bers us­ing first-or­der logic. QED.”

Whoa. So ev­ery­one in the hu­man-su­pe­ri­or­ity crowd gloat­ing about how they’re su­pe­rior to mere ma­chines and for­mal sys­tems, be­cause they can see that Godel’s State­ment is true just by their sa­cred and mys­te­ri­ous math­e­mat­i­cal in­tu­ition...

″...Is ac­tu­ally com­mit­ting a hor­ren­dous log­i­cal fal­lacy of the sort that no cleanly de­signed AI could ever be tricked into, yes. Godel’s State­ment doesn’t ac­tu­ally fol­low from the first-or­der ax­iom­a­ti­za­tion of Peano ar­ith­metic! There are mod­els where all the first-or­der ax­ioms are true, and yet Godel’s State­ment is false! The stan­dard mi­s­un­der­stand­ing of Godel’s State­ment is some­thing like the situ­a­tion as it ob­tains in sec­ond-or­der logic, where there’s no equiv­a­lent of Godel’s Com­plete­ness The­o­rem. But peo­ple in the hu­man-su­pe­ri­or­ity crowd usu­ally don’t at­tach that dis­claimer—they usu­ally pre­sent ar­ith­metic us­ing the first-or­der ver­sion, when they’re ex­plain­ing what it is that they can see that a for­mal sys­tem can’t. It’s safe to say that most of them are in­ad­ver­tently illus­trat­ing the ir­ra­tional over­con­fi­dence of hu­mans jump­ing to con­clu­sions, even though there’s a less stupid ver­sion of the same ar­gu­ment which in­vokes sec­ond-or­der logic.”

Nice. But still… that proof you’ve shown me seems like a rather cir­cuitous way of show­ing that you can’t ever rule out in­finite chains, es­pe­cially since I don’t see why Godel’s Com­plete­ness The­o­rem should be true.

“Well… an equiv­a­lent way of stat­ing Godel’s Com­plete­ness The­o­rem is that ev­ery syn­tac­ti­cally con­sis­tent set of first-or­der ax­ioms—that is, ev­ery set of first-or­der ax­ioms such that you can­not syn­tac­ti­cally prove a con­tra­dic­tion from them us­ing first-or­der logic—has at least one se­man­tic model. The proof pro­ceeds by try­ing to ad­join state­ments say­ing P or ~P for ev­ery first-or­der for­mula P, at least one of which must be pos­si­ble to ad­join while leav­ing the ex­panded the­ory syn­tac­ti­cally con­sis­tent—”

Hold on. Is there some more con­struc­tive way of see­ing why a non-stan­dard model has to ex­ist?

“Mm… you could in­voke the Com­pact­ness The­o­rem for first-or­der logic. The Com­pact­ness The­o­rem says that if a col­lec­tion of first-or­der state­ments has no model, some finite sub­set of those state­ments is also se­man­ti­cally un­re­al­iz­able. In other words, if a col­lec­tion of first-or­der state­ments—even an in­finite col­lec­tion—is un­re­al­iz­able in the sense that no pos­si­ble math­e­mat­i­cal model fits all of those premises, then there must be some finite sub­set of premises which are also un­re­al­iz­able. Or modus po­nens to modus tol­lens, if all finite sub­sets of a col­lec­tion of ax­ioms have at least one model, then the whole in­finite col­lec­tion of ax­ioms has at least one model.”

Ah, and can you ex­plain why the Com­pact­ness The­o­rem should be true?

No.

I see.

“But at least it’s sim­pler than the Com­plete­ness The­o­rem, and from the Com­pact­ness The­o­rem, the in­abil­ity of first-or­der ar­ith­metic to pin down a stan­dard model of num­bers fol­lows im­me­di­ately. Sup­pose we take first-or­der ar­ith­metic, and ad­join an ax­iom which says, ‘There ex­ists a num­ber greater than 0.’ Since there does in fact ex­ist a num­ber, 1, which is greater than 0, first-or­der ar­ith­metic plus this new ax­iom should be se­man­ti­cally okay—it should have a model if any model of first-or­der ar­ith­metic ever ex­isted in the first place. Now let’s ad­join a new con­stant sym­bol c to the lan­guage, i.e., c is a con­stant sym­bol refer­ring to a sin­gle ob­ject across all state­ments where it ap­pears, the way 0 is a con­stant sym­bol and an ax­iom then iden­ti­fies 0 as the ob­ject which is not the suc­ces­sor of any ob­ject. Then we start ad­join­ing ax­ioms say­ing ‘c is greater than X’, where X is some con­cretely speci­fied num­ber like 0, 1, 17, 2256, and so on. In fact, sup­pose we ad­join an in­finite se­ries of such state­ments, one for ev­ery num­ber:”

Wait, so this new the­ory is say­ing that there ex­ists a num­ber c which is larger than ev­ery num­ber?

“No, the in­finite schema says that there ex­ists a num­ber c which is larger than any stan­dard num­ber.”

I see, so this new the­ory forces a non­stan­dard model of ar­ith­metic.

“Right. It rules out only the stan­dard model. And the Com­pact­ness The­o­rem says this new the­ory is still se­man­ti­cally re­al­iz­able—it has some model, just not the stan­dard one.”

Why?

“Be­cause any finite sub­col­lec­tion of the new the­ory’s ax­ioms, can only use a finite num­ber of the ex­tra ax­ioms. Sup­pose the largest ex­tra ax­iom you used was ‘c is larger than 2256’. In the stan­dard model, there cer­tainly ex­ists a num­ber 2256+1 with which c could be con­sis­tently iden­ti­fied. So the stan­dard num­bers must be a model of that col­lec­tion of ax­ioms, and thus that finite sub­set of ax­ioms must be se­man­ti­cally re­al­iz­able. Thus by the Com­pact­ness The­o­rem, the full, in­finite ax­iom sys­tem must also be se­man­ti­cally re­al­iz­able; it must have at least one model. Now, adding ax­ioms never in­creases the num­ber of com­pat­i­ble mod­els of an ax­iom sys­tem—each ad­di­tional ax­iom can only filter out mod­els, not add mod­els which are in­com­pat­i­ble with the other ax­ioms. So this new model of the larger ax­iom sys­tem—con­tain­ing a num­ber which is greater than 0, greater than 1, and greater than ev­ery other ‘stan­dard’ num­ber—must also be a model of first-or­der Peano ar­ith­metic. That’s a rel­a­tively sim­pler proof that first-or­der ar­ith­metic—in fact, any first-or­der ax­iom­a­ti­za­tion of ar­ith­metic—has non­stan­dard mod­els.”

Huh… I can’t quite say that seems ob­vi­ous, be­cause the Com­pact­ness The­o­rem doesn’t feel ob­vi­ous; but at least it seems more spe­cific than try­ing to prove it us­ing Godel’s The­o­rem.

“A similar con­struc­tion to the one we used above—adding an in­finite se­ries of ax­ioms say­ing that a thingy is even larger—shows that if a first-or­der the­ory has mod­els of un­bound­edly large finite size, then it has at least one in­finite model. To put it even more alarm­ingly, there’s no way to char­ac­ter­ize the prop­erty of finite­ness in first-or­der logic! You can have a first-or­der the­ory which char­ac­ter­izes mod­els of car­di­nal­ity 3 - just say that there ex­ist x, y, and z which are not equal to each other, but with all ob­jects be­ing equal to x or y or z. But there’s no first-or­der the­ory which char­ac­ter­izes the prop­erty of finite­ness in the sense that all finite mod­els fit the the­ory, and no in­finite model fits the the­ory. A first-or­der the­ory ei­ther limits the size of mod­els to some par­tic­u­lar up­per bound, or it has in­finitely large mod­els.”

So you can’t even say, ‘x is finite’, with­out us­ing sec­ond-or­der logic? Just form­ing the con­cept of in­finity and dis­t­in­guish­ing it from finite­ness re­quires sec­ond-or­der logic?

“Cor­rect, for pretty much ex­actly the same rea­son you can’t say ‘x is only a finite num­ber of suc­ces­sors away from 0’. You can say, ‘x is less than a googol­plex’ in first-or­der logic, but not, in full gen­er­al­ity, ‘x is finite’. In fact there’s an even worse the­o­rem, the Lowen­heim-Skolem the­o­rem, which roughly says that if a first-or­der the­ory has any in­finite model, it has mod­els of all pos­si­ble in­finite car­di­nal­ities. There are un­countable mod­els of first-or­der Peano ar­ith­metic. There are countable mod­els of first-or­der real ar­ith­metic—countable mod­els of any at­tempt to ax­io­m­a­tize the real num­bers in first-or­der logic. There are countable mod­els of Zer­melo-Frankel set the­ory.”

How could you pos­si­bly have a countable model of the real num­bers? Didn’t Can­tor prove that the real num­bers were un­countable? Wait, let me guess, Can­tor im­plic­itly used sec­ond-or­der logic some­how.

“It fol­lows from the Lowen­heim-Skolem the­o­rem that he must’ve. Let’s take Can­tor’s proof as show­ing that you can’t map ev­ery set of in­te­gers onto a dis­tinct in­te­ger—that is, the pow­er­set of in­te­gers is larger than the set of in­te­gers. The Di­ag­o­nal Ar­gu­ment is that if you show me a map­ping like that, I can take the set which con­tains 0 if and only if 0 is not in the set mapped to the in­te­ger 0, con­tains 1 if and only if 1 is not in the set mapped to the in­te­ger 1, and so on. That gives you a set of in­te­gers that no in­te­ger maps to.”

You know, when I was very young in­deed, I thought I’d found a coun­terex­am­ple to Can­tor’s ar­gu­ment. Just take the base-2 in­te­gers − 1=‘1’, 2=’10′, 3=‘11’, 4=‘100’, 5=‘101’, and so on, and let each in­te­ger cor­re­spond to a set in the ob­vi­ous way, keep­ing in mind that I was also young enough to think the in­te­gers started at 1:

 1 10 11 100 101 110 111 1000 1001 {1} {2} {2, 1} {3} {3, 1} {3, 2} {3, 2, 1} {4} {4, 1}

Clearly, ev­ery set of in­te­gers would map onto a unique in­te­ger this way.

“Heh.”

Yeah, I thought I was go­ing to be fa­mous.

“How’d you re­al­ize you were wrong?”

After an em­bar­rass­ingly long in­ter­val, it oc­curred to me to ac­tu­ally try ap­ply­ing Can­tor’s Di­ag­o­nal Ar­gu­ment to my own con­struc­tion. Since 1 is in {1} and 2 is in {2}, they wouldn’t be in the re­sult­ing set, but 3, 4, 5 and ev­ery­thing else would be. And of course my con­struct didn’t have the set {3, 4, 5, …} any­where in it. I’d mapped all the finite sets of in­te­gers onto in­te­gers, but none of the in­finite sets.

“In­deed.”

I was then tempted to go on ar­gu­ing that Can­tor’s Di­ag­o­nal Ar­gu­ment was wrong any­how be­cause it was wrong to have in­finite sets of in­te­gers. Thank­fully, de­spite my young age, I was self-aware enough to re­al­ize I was be­ing tempted to be­come a math­e­mat­i­cal crank—I had also read a book on math­e­mat­i­cal cranks by this point—and so I just quietly gave up, which was a valuable life les­son.

“In­deed.”

But how ex­actly does Can­tor’s Di­ag­o­nal Ar­gu­ment de­pend on sec­ond-or­der logic? Is it some­thing to do with non­stan­dard in­te­gers?

“Not ex­actly. What hap­pens is that there’s no way to make a first-or­der the­ory con­tain all sub­sets of an in­finite set; there’s no way to talk about the pow­er­set of the in­te­gers. Let’s illus­trate us­ing a finite metaphor. Sup­pose you have the ax­iom “All kit­tens are in­no­cent.” One model of that ax­iom might con­tain five kit­tens, an­other model might con­tain six kit­tens.”

“In a sec­ond-or­der logic, you can talk about all pos­si­ble col­lec­tions of kit­tens—in fact, it’s built into the syn­tax of the lan­guage when you quan­tify over all prop­er­ties.”

“In a first-or­der set the­ory, there are some sub­sets of kit­tens whose ex­is­tence is prov­able, but oth­ers might be miss­ing.”

“Though that image is only metaphor­i­cal, since you can prove the ex­is­tence of all the finite sub­sets. Just imag­ine that’s an in­finite num­ber of kit­tens we’re talk­ing about up there.”

And there’s no way to say that all pos­si­ble sub­sets ex­ist?

“Not in first-or­der logic, just like there’s no way to say that you want as few nat­u­ral num­bers as pos­si­ble. Let’s look at it from the stand­point of first-or­der set the­ory. The Ax­iom of Pow­er­set says:”

Okay, so that says, for ev­ery set A, there ex­ists a set P which is the power set of all sub­sets of A, so that for ev­ery set B, B is in­side the pow­er­set P if and only if ev­ery el­e­ment of B is an el­e­ment of A. Any set which con­tains only el­e­ments from A, will be in­side the pow­er­set of A. Right?

“Al­most. There’s just one thing wrong in that ex­pla­na­tion—the word ‘all’ when you say ‘all sub­sets’. The Pow­er­set Ax­iom says that for any col­lec­tion of el­e­ments from A, if a set B hap­pens to ex­ist which em­bod­ies that col­lec­tion, that set B is in­side the pow­er­set P of A. There’s no way of say­ing, within a first-or­der log­i­cal the­ory, that a set ex­ists for ev­ery pos­si­ble col­lec­tion of A’s el­e­ments. There may be some sub-col­lec­tions of A whose ex­is­tence you can prove. But other sub-col­lec­tions of A will hap­pen to ex­ist as sets in­side some mod­els, but not ex­ist in oth­ers.”

So in the same way that first-or­der Peano ar­ith­metic suffers from mys­te­ri­ous ex­tra num­bers, first-or­der set the­ory suffers from mys­te­ri­ous miss­ing sub­sets.

“Pre­cisely. A first-or­der set the­ory might hap­pen to be miss­ing the par­tic­u­lar in­finite set cor­re­spond­ing to, oh, say, {3, 8, 17, 22, 28, …} where the ‘...’ is an in­finite list of ran­dom num­bers with no com­pact way of spec­i­fy­ing them. If there’s a com­pact way of spec­i­fy­ing a set—if there’s a finite for­mula that de­scribes it—you can of­ten prove it ex­ists. But most in­finite sets won’t have any finite speci­fi­ca­tion. It’s pre­cisely the claim to gen­er­al­ize over all pos­si­ble col­lec­tions that char­ac­ter­izes sec­ond-or­der logic. So it’s triv­ial to say in a sec­ond-or­der set the­ory that all sub­sets ex­ist. You would just say that for any set A, for any pos­si­ble pred­i­cate P, there ex­ists a set B which con­tains x iff x in A and Px.”

I guess that tor­pe­does my clever idea about us­ing first-or­der set the­ory to uniquely char­ac­ter­ize the stan­dard num­bers by first as­sert­ing that there ex­ists a set con­tain­ing at least the stan­dard num­bers, and then talk­ing about the small­est sub­set which obeys the Peano ax­ioms.

“Right. When you talk about the num­bers us­ing first-or­der set the­ory, if there are ex­tra num­bers in­side your set of num­bers, the sub­set con­tain­ing just the stan­dard num­bers must be miss­ing from the pow­er­set of that set. Other­wise you could find the small­est sub­set in­side the pow­er­set such that it con­tained 0 and con­tained the suc­ces­sor of ev­ery num­ber it con­tained.”

Hm. So then what ex­actly goes wrong with Can­tor’s Di­ag­o­nal Ar­gu­ment?

“Can­tor’s Di­ag­o­nal Ar­gu­ment uses the idea of a map­ping be­tween in­te­gers and sets of in­te­gers. In set the­ory, each map­ping would it­self be a set—in fact there would be a set of all map­ping sets:”

“There’s no way to first-or­der as­sert the ex­is­tence of ev­ery pos­si­ble map­ping that we can imag­ine from out­side. So a first-or­der ver­sion of the Di­ag­o­nal Ar­gu­ment would show that in any par­tic­u­lar model, for any map­ping that ex­isted in the model from in­te­gers to sets of in­te­gers, the model would also con­tain a di­ag­o­nal­ized set of in­te­gers that wasn’t in that map­ping. This doesn’t mean that we couldn’t count all the sets of in­te­gers which ex­isted in the model. The model could have so many ‘miss­ing’ sets of in­te­gers that the re­main­ing sets were de­nu­mer­able. But then some map­pings from in­te­gers to sets would also be miss­ing, and in par­tic­u­lar, the ‘com­plete’ map­ping we can imag­ine from out­side would be miss­ing. And for ev­ery map­ping that was in the model, the Di­ag­o­nal Ar­gu­ment would con­struct a set of in­te­gers that wasn’t in the map­ping. On the out­side, we would see a pos­si­ble map­ping from in­te­gers to sets—but that map­ping wouldn’t ex­ist in­side the model as a set. It takes a logic-of-col­lec­tions to say that all pos­si­ble in­te­ger-col­lec­tions ex­ist as sets, or that no pos­si­ble map­ping ex­ists from the in­te­gers onto those sets.”

So if first-or­der logic can’t even talk about finite­ness vs. in­finite­ness—let alone prove that there are re­ally more sets of in­te­gers than in­te­gers—then why is any­one in­ter­ested in first-or­der logic in the first place? Isn’t that like try­ing to eat din­ner us­ing only a fork, when there are lots of in­ter­est­ing foods which prov­ably can’t be eaten with a fork, and you have a spoon?

“Ah, well… some peo­ple be­lieve there is no spoon. But let’s take that up next time.”

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

Next post: “Se­cond-Order Logic: The Con­tro­versy

Pre­vi­ous post: “Stan­dard and Non­stan­dard Num­bers

• Math­e­mat­i­cal com­ment that might amuse LWers: the com­pact­ness the­o­rem is equiv­a­lent to the ul­tra­filter lemma, which in turn is es­sen­tially equiv­a­lent to the state­ment that Ar­row’s im­pos­si­bil­ity the­o­rem is false if the num­ber of vot­ers is al­lowed to be in­finite. More pre­cisely, non-prin­ci­pal ul­tra­filters are the same as meth­ods for de­ter­min­ing elec­tions based on votes from in­finitely many vot­ers in a way that satis­fies all of the con­di­tions in Ar­row’s the­o­rem.

Math­e­mat­i­cal com­ment that some LWers might find rele­vant: the com­pact­ness the­o­rem is in­de­pen­dent of ZF, which roughly speak­ing one should take as mean­ing that it is not pos­si­ble to write down a non-prin­ci­pal ul­tra­filter ex­plic­itly. If you’re suffi­ciently ul­tra­fini­tist, you might not trust a line of rea­son­ing that in­volved the com­pact­ness the­o­rem but pur­ported to be re­lated to a prac­ti­cal real-world prob­lem (e.g. FAI).

• The rea­son why com­pact­ness is not prov­able from ZF is that you need choice for some kinds of in­finite sets. You don’t need choice for countable sets (if you have a way of map­ping them into the in­te­gers that is). You can get a proof of com­pact­ness for any countable set of ax­ioms by prov­ing com­plete­ness for any countable set of ax­ioms, which can be done by con­struc­tion of a model as in John­stone’s Notes on Logic and Set The­ory p. 25.

• the com­pact­ness the­o­rem is equiv­a­lent to the ul­tra­filter lemma, which in turn is es­sen­tially equiv­a­lent to the state­ment that Ar­row’s im­pos­si­bil­ity the­o­rem is false if the num­ber of vot­ers is al­lowed to be in­finite.

Well, I can con­firm that I think that that’s su­per cool!

the com­pact­ness the­o­rem is in­de­pen­dent of ZF

As wun­ci­dunci says, that’s only true if you al­low un­countable lan­guages. I can’t think of many cases off the top of my head where you would re­ally want that… countable is usu­ally enough.

Also: more ev­i­dence that the higher model the­ory of first-or­der logic is highly de­pen­dent on set the­ory!

• I’m fas­ci­nated by but com­pletely failing to grasp your first com­ment. Speci­fi­cally:

Sup­pose we:

• Take a finite set FS of N voters

• Define an in­finite set IS of hy­po­thet­i­cal vot­ers, fully in­dexed by the pos­i­tive in­te­gers, such that hy­po­thet­i­cal vote n+1 is the same as real vote (n mod N)+1

• Use a “non-prin­ci­pal ul­tra­filter” to re­solve the result

Which of Ar­row’s crite­ria is vi­o­lated when con­sid­er­ing this to be a re­sult of the votes in FS but not vi­o­lated when con­sid­er­ing this to be a re­sult of the votes in IS?

• Good ques­tion! It’s dic­ta­tor­ship. In such a situ­a­tion, any non-prin­ci­pal ul­tra­filter picks out one of the con­gru­ence classes and only listens to that one.

More gen­er­ally, given any par­ti­tion of an in­finite set of vot­ers into a finite dis­joint union of sets, a non-prin­ci­pal ul­tra­filter picks out one mem­ber of the par­ti­tion and only listens to that one. In other words, a non-prin­ci­pal ul­tra­filter dis­en­fran­chises ar­bi­trar­ily large por­tions of the pop­u­la­tion. This is an­other rea­son it’s not very use­ful for ac­tu­ally con­duct­ing elec­tions!

• which in turn is es­sen­tially equiv­a­lent to the state­ment that Ar­row’s im­pos­si­bil­ity the­o­rem is false if the num­ber of vot­ers is al­lowed to be in­finite.

And you can achieve that, in effect, by per­mit­ting (finite) vot­ers to ex­press prefer­ences us­ing the full spec­trum of real num­bers, right? Since that’s equiv­a­lent to hav­ing in­finite vot­ers?

Thus, why sys­tems like range vot­ing avoid its con­se­quences. (Though range vot­ing typ­i­cally limits the pre­ci­sion in prac­tice.)

• No, the de­tails are very differ­ent from range vot­ing. You still only al­low each voter to pick one can­di­date, and the ul­tra­filter pro­vides a (highly non­con­struc­tive) way of dis­till­ing all of these votes into a win­ner of the elec­tion. You can get a feel for how this works by read­ing about what Ter­ence Tao calls an adap­tive or­a­cle. Roughly speak­ing, you can ar­bi­trar­ily choose win­ners sub­ject to con­sis­tency with your pre­vi­ous choices and with the con­di­tions in Ar­row’s the­o­rem, and the free­dom of hav­ing in­finitely many vot­ers en­sures that this pro­cess won’t lead to a con­tra­dic­tion.

In a cer­tain sense, “ul­tra­filter vot­ing” is still con­trol­led by a sort of “vir­tual dic­ta­tor,” so even con­cep­tu­ally this isn’t a strong blow to Ar­row’s the­o­rem, and in prac­tice “ul­tra­filter vot­ing” is use­less be­cause you can’t write down (non-prin­ci­pal) ul­tra­filters ex­plic­itly.

• I ad­mit I don’t know a lot about these in­ter­sect­ing top­ics, but I also don’t see the rele­vant differ­ence that you’re as­sert­ing be­tween in­finite vot­ers and in­finite pre­ci­sion of (finite) range-vot­ers, es­pe­cially given that range vot­ing does not, as you say, “only al­low each voter to pick one can­di­date”

• Okay, then I don’t un­der­stand what you’re say­ing. What do you mean by “per­mit­ting (finite) vot­ers to ex­press prefer­ences us­ing the full spec­trum of real num­bers” when, as I’ve said, in “ul­tra­filter vot­ing” each voter is still only al­lowed to pick one can­di­date in­stead of ex­press­ing a de­gree of prefer­ence be­tween can­di­dates?

• Well, then I don’t un­der­stand why you’re re­fut­ing claims about range vot­ing by mak­ing claims about ul­tra­filter vot­ing.

Edit: It turns out that this was the re­sult of mis­read­ing the first two sen­tences of this com­ment.

• I’m… not?

• The vot­ing on this thread is bizarre, but I think I know where some of my con­fu­sion comes from. I mis­read this com­ment:

No, the de­tails are very differ­ent from range vot­ing. You still only al­low each voter to pick one can­di­date, and the ul­tra­filter pro­vides a (highly non­con­struc­tive) way of dis­till­ing all of these votes into a win­ner of the elec­tion.

I thought the bit about “you still only al­low … one can­di­date” was about range vot­ing, and the ul­tra­filter clause was refer­ring to the­o­rem.

Nev­er­the­less, while you make a lot of points that are in­ter­est­ing in iso­la­tion, I don’t see how any of it is re­spon­sive to the ques­tion I asked, which was whether the range vot­ing (and other sys­tems like it) avoids the Ar­row The­o­rem prob­lems by al­low­ing in­finite (effec­tive, vir­tual) vot­ers.

To any­one still read­ing: I un­der­stand that I’ve made some log­i­cal er­rors in this thread, but why the se­vere down­vot­ing for some hon­est ques­tions? Is there a nicer way to tell some­one it looks like they’re chang­ing the topic?

• I don’t see how any of it is re­spon­sive to the ques­tion I asked, which was whether the range vot­ing (and other sys­tems like it) avoids the Ar­row The­o­rem prob­lems by al­low­ing in­finite (effec­tive, vir­tual) vot­ers.

The an­swer is still no. Again, the de­tails are very differ­ent. If you stud­ied them, it would be clear to you that the de­tails are very differ­ent. I don’t know what else there is to say. If you asked me “is an ap­ple tasty be­cause it be­haves like an or­ange?” my an­swer would be “no, ap­ples be­have very differ­ently from or­anges” and I don’t un­der­stand what would con­sti­tute a bet­ter an­swer than that.

• Ac­tu­ally, what hap­pened here would be more like this ex­change:

You: Red pro­duce is ex­empt from the pro­duce tar­iffs.
Me: Oh! Is that why they don’t make you pay a tax on red car­rots?
You: The de­tails are differ­ent there. Ap­ples have long been used in mak­ing cider, and cider has to be taxed, but it can’t be dou­ble-taxed, and you can read about why [here]. Ap­ples have a sig­nifi­cantly differ­ent shape from car­rots, and the ne­ces­sity of cer­tain in­fras­truc­ture has led to shape in­fluenc­ing tax­a­tion.
Me: Well, I don’t know about all those is­sues, but on the mat­ter of whether red car­rots be­ing red gets them out of the pro­duce tar­iffs, is my sug­ges­tion cor­rect?
You: I don’t even know what you’re say­ing now. What do you mean by “red car­rots be­ing red” when, as I’ve said, ap­ples can be used for cider? Look, just study tax law, I can’t con­ceive of how I can provide any other kind of re­ply.

That’s a sim­ple sub­sti­tu­tion of what hap­pened here:

You: In­finite-voter sys­tems avoid the con­se­quences of Ar­row’s The­o­rem.
Me: Oh, is that why range vot­ing avoids it?
You: The de­tails are differ­ent there. Ul­trafilter vot­ing pro­vides a way to se­lect a win­ner, similar to how an adap­tive or­a­cle works. It al­lows you to choose win­ners in a way that satis­fies the Ar­row con­straints.
Me: Well, I don’t know about all those is­sues, but on the mat­ter of whether range vot­ing be­ing effec­tively in­finite-voter (via in­finite pre­ci­sion), and in­finite-voter sys­tems avoid­ing the con­se­quences of Ar­row’s The­o­rem, am I right?
You: What do you mean “be­ing effec­tively in­finite voter … in­finite pre­ci­sion”, when ul­tra­filter vot­ing has you just vote for one can­di­date? Look, just study the topic, I can’t con­ceive of how I could re­ply differ­ently.

• No, it re­ally isn’t. A closer anal­ogy is that pro­duce that is ei­ther red or or­ange is ex­empt from the pro­duce tar­iffs, ul­tra­filter vot­ing is red, and range vot­ing is or­ange. If you aren’t will­ing to study the de­tails then I am not go­ing to re­spond any fur­ther. I’ve paid 10 karma to re­spond now en­tirely be­cause I think ul­tra­filters are great and peo­ple should learn about them, but they have noth­ing to do with range vot­ing.

• So were you wrong to say that all “in­finite voter sys­tems avoid the con­se­quences of Ar­row’s The­o­rem” (“both red and or­ange are ex­empt”), or were you wrong to re­ject my point about range vot­ing’s in­finite effec­tive vot­ers be­ing proof that it avoids the con­se­quences of Ar­row’s The­o­rem?

On the one hand, you want to say that the broad prin­ci­ple is true (“ap­ples and or­anges are ex­empt”/​”all in­finite voter sys­tems are ex­empt”), but on the other hand, you don’t want to agree that the broad prin­ci­ple has the im­pli­ca­tions I sug­gested (“Navals are or­anges and thus ex­empt”/​”Range vot­ing has in­finite vot­ers as is thus ex­empt”).

And a re­s­olu­tion of that in­con­sis­tency re­ally does not re­quire a thor­ough re­view of the cited sources.

• There’s a su­perfi­cial similar­ity, in that both situ­a­tions (in­finite vot­ers, and real-num­ber range vot­ing) have an un­countable bal­lot space. Where by bal­lot space I mean the set of all pos­si­ble com­bi­na­tions of votes for all vot­ers. But oth­er­wise, it’s not re­ally equiv­a­lent at all. For one thing, range vot­ing doesn’t ac­tu­ally re­quire in­finite pre­ci­sion. Even if the only val­ues al­lowed are {0, 1, 2, …, 10} it still gets around Ar­row’s the­o­rem, right? Even though you ac­tu­ally have a finite bal­lot space in this case.

• Right—my point was just that the in­finite (effec­tive) vot­ers would be suffi­cient but not nec­es­sary.

• If you could say that, you could rule out num­bers with in­finite num­bers of pre­de­ces­sors, mean­ing that you could rule out all in­finite-in-both-di­rec­tions chains, and hence rule out all non­stan­dard num­bers. And then the only re­main­ing model would be the stan­dard num­bers. And then Godel’s State­ment would be a se­man­tic im­pli­ca­tion of those ax­ioms; there would ex­ist no num­ber en­cod­ing a proof of Godel’s State­ment in any model which obeyed the ax­ioms of first-or­der ar­ith­metic. And then, by Godel’s Com­plete­ness The­o­rem, we could prove Godel’s State­ment from those ax­ioms us­ing first-or­der syn­tax. Be­cause ev­ery gen­uinely valid im­pli­ca­tion of any col­lec­tion of first-or­der ax­ioms—ev­ery first-or­der state­ment that ac­tu­ally does fol­low, in ev­ery pos­si­ble model where the premises are true—can always be proven, from those ax­ioms, in first-or­der logic. Thus, by the com­bi­na­tion of Godel’s In­com­plete­ness The­o­rem and Godel’s Com­plete­ness The­o­rem, we see that there’s no way to uniquely pin down the nat­u­ral num­bers us­ing first-or­der logic. QED.”

This is a tor­tured and un­for­tu­nate phras­ing of the fol­low­ing di­rect and clearer ar­gu­ment:

Godel’s In­com­plete­ness The­o­rem says that there’s a sen­tence G that our first-or­der the­ory PA nei­ther proves nor dis­proves. And Godel’s Com­plete­ness the­o­rem says that ev­ery con­sis­tent the­ory has a model.

(this is also a bet­ter, more in­tu­itive way of pre­sent­ing the Com­plete­ness the­o­rem than “ev­ery state­ment valid in ev­ery model has a proof”, be­cause it hints at why it’s true. It’s not in­tu­itively clear why ev­ery valid state­ment must have a proof, but if a the­ory is con­sis­tent, if you can­not puz­zle out a con­tra­dic­tion within it, then it makes sense that some­thing out there looks like what it says. If it could hap­pen (by virtue of be­ing con­sis­tent), it does hap­pen. And the usual proof of the Com­plete­ness the­o­rem in fact shows how it hap­pens).

“PA doesn’t prove G” means “PA+not-G is con­sis­tent” and “PA doesn’t dis­prove G” means “PA+G is con­sis­tent”. Thus by the Com­plete­ness the­o­rem both PA+G and PA+not-G have a model. And only one of them could pos­si­bly be the stan­dard model, so the other is cer­tainly non­stan­dard.

The Com­pact­ness The­o­rem says that if a col­lec­tion of first-or­der state­ments has no model, there is a finite syn­tac­ti­cal proof of an in­con­sis­tency.

No. No. No.

You keep con­flat­ing syn­tax and se­man­tics, and the re­sult is a mud­dled de­scrip­tion in which differ­ent kinds of non­stan­dard mod­els ex­ist­ing for differ­ent rea­sons merge and run to­gether in a con­fused whole.

Prop­erly phrased, the Com­pact­ness the­o­rem is wholly se­man­tic, not syn­tac­tic. It says that if a col­lec­tion of state­ments has no model, than already some finite sub­set of it has no model. There is no refer­ence to proof any­where. This is im­por­tant!

First-or­der logic pre­sents us with two kinds of limi­ta­tions on the power of our rea­son­ing. There are se­man­tic limi­ta­tions on what we can cap­ture in a state­ment or a set of state­ments. In other words, how ex­pres­sive our for­mal lan­guage is, how well it’s able to de­scribe the math­e­mat­i­cal re­al­ity. And then there are syn­tac­tic limi­ta­tions on what we can hope to prove, given an ap­pro­pri­ate ax­io­matic sys­tem and a set of ax­ioms.

It’s vi­tal to keep syn­tax and se­man­tics sharply apart in your mind and keep track of what is what. But both syman­tic and syn­tac­tic limi­ta­tions may man­i­fest as ex­is­tence of un­wanted “non­stan­dard mod­els”, and your ac­count mud­dles them to­gether. And more gen­er­ally your ac­count of “try­ing to pin­point the stan­dard num­bers” again and again fails to dis­t­in­guish be­tween the limits on what we can ex­press and the limits on what we can prove, and the re­sult is con­fu­sion.

(Here’s a thought ex­per­i­ment. Imag­ine we deleted rules of in­fer­ence from our first-or­der logic. Now we have a logic with an in­cred­ibly weak proof sys­tem: noth­ing can be proved ex­cept what is taken as an ax­iom. Proofs are one state­ment long. There is no Com­plete­ness the­o­rem: the Com­plete­ness the­o­rem says that first-or­der logic’s abil­ity to prove things is as strong as it ought to be, and our logic is weak. But there is still the Com­pact­ness the­o­rem, it didn’t go any­where. And there are still non­stan­dard mod­els due to it, noth­ing hap­pened to them. The Com­pact­ness the­o­rem may be proved via the Com­plete­ness the­o­rem, but that’s just a pos­si­ble proof. It can also be proved via a com­pletely se­man­tic ar­gu­ment. It’s about what can be ex­pressed in a state­ment, not what can be proved, and mak­ing our logic ridicu­lously weak doesn’t af­fect it in the least.)

So, among se­man­tic limi­ta­tions on what we can ex­press we can count the Com­pact­ness the­o­rem, that shows us, among other things, we can­not hope to cap­ture with first-or­der state­ments the be­hav­ior of any par­tic­u­lar in­finite model, like the nat­u­ral num­bers. There will always be non­stan­dard mod­els, and in many cases of in­ter­est they will even be of the same size as the stan­dard model.

(an­other ex­am­ple of a se­man­tic limi­ta­tion is Tarski’s un­defin­abil­ity of truth, which re­ally de­serves much of the rep­u­ta­tion thoughtlessly be­stowed upon Godel’s In­com­plete­ness The­o­rem).

And in mat­ters syn­tac­tic we have, as a great boon, the Com­plete­ness The­o­rem tel­ling us we can prove uni­ver­sally true things, but on the other hand the In­com­plete­ness The­o­rem is a check on our abil­ity to cap­ture all ar­ith­meti­cal truths in a man­age­able set of ax­ioms. We can com­bine this in­abil­ity with the Com­plete­ness The­o­rem (act­ing in a semi-evil ca­pac­ity here) to demon­strate non­stan­dard mod­els that show off our failure in the flesh, so to speak. But that is merely an echo of the real thing, the real failure that is our in­abil­ity to form a man­age­able com­plete the­ory of ar­ith­metics. Imag­ine for a sec­ond that our logic were a lit­tle weaker so that we didn’t have the Com­plete­ness the­o­rem in full gen­er­al­ity, but would still have a rel­a­tively pow­er­ful proof sys­tem to for­mal­ize the usual math­e­mat­i­cal proofs and in par­tic­u­lar to have the In­com­plete­ness the­o­rem. Then per­haps we wouldn’t be able to prove that there ex­ists a non­stan­dard model of PA+not-G. But that wouldn’t re­ally mat­ter, the real failure would re­main the fact that PA nei­ther proves nor dis­proves G. That would re­main an es­sen­tial limi­ta­tion on the pow­ers of our for­mal rea­son­ing.

The non­stan­dard mod­els due to the syn­tac­tic limi­ta­tions of the In­com­plet­ess The­o­rem are thus more of a shiny ex­hi­bi­tion than the real failure. And at any rate, they are so differ­ent in na­ture from the non­stan­dard mod­els due to the se­man­tic limi­ta­tions that it’s con­fus­ing to run them to­gether. The former kind, the In­com­plete­ness-based non­stan­dard mod­els, nec­es­sar­ily dis­agree on some state­ments of the stan­dard lan­guage of ar­ith­metic. They are in­stan­ti­a­tions of differ­ent first-or­der claims about nat­u­ral num­bers. There are perfectly or­di­nary state­ments about nat­u­ral num­bers, like G, that are true in one of them and false in the other.

But in the other kind of non­stan­dard mod­els, the ones re­sult­ing from the Com­pact­ness the­o­rem, that doesn’t have to be the case. Even T(N), the full the­ory of true ar­ith­metic, which takes for ax­ioms all true state­ments about nat­u­ral num­bers, has non­stan­dard mod­els due to the Com­pact­ness the­o­rem. Th­ese non­stan­dard mod­els do not dis­agree with the stan­dard one about any first-or­der claim in the stan­dard lan­guage. They are man­i­fes­ta­tions of limi­ta­tions in­her­ent in the lan­guage it­self, not in what truths we are able to cap­ture. Even if we could cap­ture all first-or­der truths about nat­u­ral num­bers—even if there was no In­com­plete­ness The­o­rem, and PA were a com­plete the­ory of ar­ith­metic—they would still be there, ex­press­ing the same truths in a differ­ent-look­ing model, as a sign that our lan­guage is not an all-pow­er­ful means of ex­press­ing the math­e­mat­i­cal re­al­ity.

• I re­al­ized af­ter read­ing this that I’d stated the Com­pact­ness The­o­rem much more strongly than I needed, and that I only needed the fact that in­finite se­man­tic in­con­sis­tency im­plies finite se­man­tic in­con­sis­tency, never mind syn­tac­tic proofs of in­con­sis­tency, so I did a quick rewrite ac­cord­ingly. Hope­fully this ad­dresses your wor­ries about “mud­dled de­scrip­tion”, al­though ini­tially I was con­fused about what you meant by “mud­dled” since I’d always care­fully dis­t­in­guished se­man­tics from syn­tax at each point in the post.

I was also con­fused by what you meant by “non­stan­dard mod­els re­sult­ing from the Com­pact­ness The­o­rem” ver­sus “non­stan­dard mod­els re­sult­ing from the In­com­plete­ness The­o­rem”—the non­stan­dard mod­els are just there, af­ter all, they don’t poof into ex­is­tence as a re­sult of one The­o­rem or the other be­ing proved. But yes, the Com­pact­ness The­o­rem shows that even ad­join­ing all first-or­der state­able truths about the nat­u­ral num­bers to PA (re­sult­ing in a the­ory not de­scrib­able within PA) would still give a the­ory with non­stan­dard mod­els.

• I think “se­man­tic con­sis­tency” is not a very good phrase, and you should con­sider re­plac­ing it with “satis­fi­a­bil­ity” or, if that seems too tech­ni­cal, “re­al­iz­abil­ity”. The word “in­con­sis­tent” tells us that there’s some sort of con­tra­dic­tion hid­den within. But there could be state­ments with­out con­tra­dic­tion that are yet not re­al­iz­able—not in our logic, thanks to the Com­plete­ness the­o­rem, but in some other, per­haps less use­ful one. Imag­ine for ex­am­ple that you tried to de­velop math­e­mat­i­cal logic from scratch, and defined “mod­els” in such a way that only finite sets can serve as their do­mains (per­haps be­cause you’re a hard­core fini­tist or some­thing). Then your class of mod­els is too poor and doesn’t sus­tain the Com­plete­ness the­o­rem. There are con­sis­tent finite sets of state­ments, from which no con­tra­dic­tion may be syn­tac­ti­cally de­rived, that are only re­al­iz­able in in­finite mod­els and so are not re­al­iz­able at all in this hy­po­thet­i­cal logic. It feels wrong to call them “se­man­ti­cally in­con­sis­tent” even though you can tech­ni­cally do that of course, it’s just a defi­ni­tion. “Real­iz­able” seems bet­ter.

I feel that this ex­am­ple is part of a larger trend. Think of first-or­der logic as a perfect fit be­tween syn­tac­tic no­tions (how for­mu­las are built up, what is a proof) and se­man­tic no­tions (how to as­sign a truth value to a state­ment in a model, what mod­els ex­ist and how they’re defined). Apri­ori it’s not clear or pre­or­dained that these two fit to­gether like a hand in a glove, but thanks to Sound­ness and Com­plete­ness the­o­rems they ac­tu­ally do. You keep us­ing that fit to jump seam­lessly be­tween se­man­tic no­tions and syn­tac­tic no­tions, and al­though you’re not com­mit­ting any er­ror, I think the re­sult is con­fus­ing; in “al­ter­na­tive uni­verses”—other log­ics—the fit doesn’t ex­ist or it’s very differ­ent, and to gain un­der­stand­ing and ap­pre­ci­a­tion of how logic works the two must be kept sharply sep­a­rate in one’s mind. I’m not say­ing that you don’t ap­pre­ci­ate the differ­ence—I’m say­ing that ped­a­gog­i­cally your posts in this se­quence fail in mak­ing the reader un­der­stand it.

I was con­fused about what you meant by “mud­dled” since I’d always care­fully dis­t­in­guished se­man­tics from syn­tax at each point in the post.

Here’s an ex­am­ple from an ear­lier post:

...Gosh. I think I see the idea now. It’s not that ‘ax­ioms’ are math­e­mat­i­ci­ans ask­ing for you to just as­sume some things about num­bers that seem ob­vi­ous but can’t be proven. Rather, ax­ioms pin down that we’re talk­ing about num­bers as op­posed to some­thing else.

“Ex­actly. That’s why the math­e­mat­i­cal study of num­bers is equiv­a­lent to the log­i­cal study of which con­clu­sions fol­low in­evitably from the num­ber-ax­ioms. The way that the­o­rems like 2 + 2 = 4 are syn­tac­ti­cally prov­able from those ax­ioms re­flects the way that 2 + 2 = 4 is se­man­ti­cally im­plied within this unique math­e­mat­i­cal uni­verse that the ax­ioms pin down.

I’m con­vinced that a reader of this se­quence who is not ed­u­cated in logic sim­ply won’t no­tice the leaps be­tween syn­tax and se­man­tics that you ha­bit­u­ally make in an undis­ci­plined fash­ion, and will not get a clear pic­ture of why and which non­stan­dard mod­els ex­ist and how proof sys­tems, Com­plete­ness and In­com­plete­ness in­ter­act with their ex­is­tence.

I was also con­fused by what you meant by “non­stan­dard mod­els re­sult­ing from the Com­pact­ness The­o­rem” ver­sus “non­stan­dard mod­els re­sult­ing from the In­com­plete­ness The­o­rem”—the non­stan­dard mod­els are just there, af­ter all, they don’t poof into ex­is­tence as a re­sult of one The­o­rem or the other be­ing proved.

Well, I thought I made that clear in my com­ment. Yes, they are there, but you can imag­ine other log­ics where one of the the­o­rems holds but not the other, and see that one kind of the non­stan­dard mod­els re­mains and the other dis­ap­pears. The differ­ence be­tween them to work­ing math­e­mat­i­ci­ans and lo­gi­ci­ans is vast. Lowen­helm-Skolem was proved, I think in 1917 or there­abouts, but un­til Godel’s In­com­plete­ness The­o­rem ap­peared no­body thought that it demon­strated that first-or­der logic is not suit­able to for­mal­ize math­e­mat­ics be­cause it doesn’t “pin down stan­dard num­bers”.

That’s why I think that your em­pha­sis on “pins down a unique model” is wrong­headed and doesn’t re­flect the real con­cerns math­e­mat­i­ci­ans and lo­gi­ci­ans had and con­tinue to have about how well ax­io­matic sys­tems for­mal­ize math­e­mat­ics. It’s be­cause this prop­erty is too coarse to dis­t­in­guish e.g. be­tween in­com­plete and com­plete the­o­ries—even com­plete the­o­ries have non­stan­dard mod­els in first-or­der logic. In an al­ter­nate uni­verse where Godel’s In­com­plete­ness doesn’t ex­ist and PA is a com­plete first-or­der the­ory that proves or dis­proves any state­ment about nat­u­ral num­bers, ap­prox­i­mately no­body cares that it has non­stan­dard mod­els due to Com­pact­ness, and ev­ery­body’s very happy that they have a set of ax­ioms that are able in prin­ci­ple to an­swer all ques­tions you can ask about nat­u­ral num­bers. (if you protest that PA is in­com­plete in any al­ter­nate uni­verse, con­sider that there are com­plete first-or­der the­o­ries, e.g. of real closed fields). You’re free to dis­agree with that and to in­sist that cat­e­goric­ity—hav­ing only one model up to iso­mor­phism—must be the all-im­por­tant prop­erty of the logic we want to use, but your read­ers are ill-equipped to agree or dis­agree in an in­formed way be­cause your de­scrip­tion mud­dles the hugely im­por­tant differ­ence be­tween those two kinds of non­stan­dard mod­els. To math­e­mat­i­ci­ans in­ter­ested in foun­da­tions, the fact that PA is in­com­plete is a blow to Hilbert’s pro­gram and more gen­er­ally to the pro­ject of for­mal­iz­ing math­e­mat­i­cal mean­ing, while non­stan­dard mod­els ex­ist­ing due to com­pact­ness are at worst an an­noy­ing tech­ni­cal dis­trac­tion, and at best a source of in­ter­est­ing con­struc­tions like non­stan­dard anal­y­sis.

• I’ll try a cou­ple more ed­its, but keep in mind that this isn’t aimed at lo­gi­ci­ans con­cerned about Hilbert’s pro­gram, it’s aimed at im­prov­ing gib­ber­ish-de­tec­tion skills (sen­tences that can’t mean things) and avoid­ing logic abuse (try­ing to get em­piri­cal facts from first prin­ci­ples) and im­prov­ing peo­ple’s metaethics and so on.

• Just as an aside, I re­ally en­joyed Scott Aaron­son’s ex­pla­na­tion of non­stan­dard mod­els in this writeup:

...The Com­plete­ness The­o­rem is con­fus­ing for two rea­sons: on the one hand, it sounds like a tau­tol­ogy (“that which is con­sis­tent, is con­sis­tent”) — what could it pos­si­bly mean to prove such a thing? And on the other hand, it seems to con­tra­dict the In­com­plete­ness The­o­rem.

We’re go­ing to clear up this mess, and as a bonus, an­swer our ques­tion about whether all mod­els of ZF are un­countable. The best way to un­der­stand the Com­plete­ness The­o­rem is to make up a con­sis­tent ax­iom set that you’d guess doesn’t have a model. Given a the­ory T, let Con(T) be the as­ser­tion that T is con­sis­tent. We know from Gödel’s In­com­plete­ness The­o­rem that Con(ZF) can be ex­pressed in ZF, and also that Con(ZF) can’t be proved in ZF, as­sum­ing ZF is con­sis­tent. It fol­lows that as­sum­ing ZF is con­sis­tent, the “self-hat­ing the­ory” ZF+¬Con(ZF), or ZF plus the as­ser­tion of its own in­con­sis­tency, must also be con­sis­tent. So by the Com­plete­ness The­o­rem, ZF+¬Con(ZF) has a model. What on earth could it be? We’ll an­swer this ques­tion via a ﬁc­tional di­alogue be­tween you and the ax­ioms of ZF+¬Con(ZF).

You: Look, you say ZF is in­con­sis­tent, from which it fol­lows that there’s a proof in ZF that 1+1=3. May I see that proof?

Ax­ioms of ZF+¬Con(ZF): I pre­fer to talk about in­te­gers that en­code proofs. (Ac­tu­ally sets that en­code in­te­gers that en­code proofs. But I’ll cut you a break — you’re only hu­man, af­ter all.)

You: Then show me the in­te­ger.

Ax­ioms: OK, here it is: X.

You: What the hell is X?

Ax­ioms: It’s just X, the in­te­ger en­coded by a set in the uni­verse that I de­scribe.

You: But what is X, as an or­di­nary in­te­ger?

Ax­ioms: No, no, no! Talk to the ax­ioms.

You: Alright, let me ask you about X. Is greater or smaller than a billion?

Ax­ioms: Greater.

You: The 10^10^1,000,000,000th Ack­er­mann num­ber?

Ax­ioms: Greater than that too.

You: What’s X^2+100?

Ax­ioms: Hmm, let me see… Y.

You: Why can’t I just add an ax­iom to rule out these weird ‘non­stan­dard in­te­gers?’ Let me try: for all in­te­gers X, X be­longs to the set ob­tained by start­ing from 0 and...

Ax­ioms: Ha ha! This is ﬁrst-or­der logic. You’re not al­lowed to talk about sets of ob­jects — even if the ob­jects are them­selves sets.

Ax­ioms: That right! What Gödel showed is that we can keep play­ing this game for­ever. What’s more, the in­ﬁnite se­quence of bizarre en­tities you’d force me to make up — X, Y, and so on — would then con­sti­tute a model for the pre­pos­ter­ous the­ory ZF+¬Con(ZF).

You: But how do you know I’ll never trap you in an in­con­sis­tency?

Ax­ioms: Be­cause if you did, the Com­plete­ness The­o­rem says that we could con­vert that into an in­con­sis­tency in the origi­nal ax­ioms, which con­tra­dicts the ob­vi­ous fact that ZF is con­sis—no, wait! I’m not sup­posed to know that! Aaahh! [The ax­ioms melt in a pud­dle of in­con­sis­tency.]

• I’m con­cerned that you’re push­ing sec­ond or­der logic too hard, us­ing a false fork—such and so can­not be done in first or­der logic there­fore sec­ond-or­der logic. “Se­cond or­der” logic is a par­tic­u­lar thing—for ex­am­ple it is a logic based on model the­ory. http://​​en.wikipe­dia.org/​​wiki/​​Se­cond-or­der_logic#His­tory_and_dis­puted_value

There are lots of al­ter­na­tive di­rec­tions to go when you go be­yond the gen­eral con­sen­sus of first-or­der logic. Freek Wiedijk’s pa­per “Is ZF a hack?” is a great tour of al­ter­na­tive foun­da­tions of math­e­mat­ics—first or­der logic and the Zer­melo-Frankel ax­ioms for set the­ory turns out to be the small­est by many mea­sures, but the oth­ers are gen­er­ally higher or­der in one way or an­other. http://​​www.cs.ru.nl/​​~freek/​​zfc-etc/​​zfc-etc.pdf

“First or­der logic can’t talk about finite­ness vs. in­finite­ness.” is sortof true in that first-or­der logic in a fixed lan­guage is nec­es­sar­ily lo­cal—it can step from ob­ject to ob­ject (along re­la­tion links) but the num­ber of steps bounded by the size of the first-or­der for­mula. How­ever, a stan­dard move is to change the lan­guage, in­tro­duc­ing a new sort of ob­ject “sets” and some ax­ioms re­gard­ing re­la­tions be­tween the old ob­jects and the new ob­jects such as in­clu­sion, and then you can talk about prop­er­ties of these new ob­jects such as finite­ness and in­finite­ness. Ad­mit­tedly this stan­dard move is in­for­mal or metathe­o­retic; we’re say­ing “this the­ory is the same as that the­ory ex­cept for these new ob­jects and ax­ioms”.

This is what the Zer­melo-Frankel ax­ioms do, and the vast ma­jor­ity of math­e­mat­ics can be done within ZF or ZFC. Al­most any time you en­counter “finite­ness” and “in­finite­ness” in a branch of math­e­mat­ics other than logic, they are for­mal­iz­able as first-or­der prop­er­ties of first-or­der en­tities called sets.

• you could use the 2 pre­fix for NOT and the 3 pre­fix for AND

Im­me­di­ately af­ter this, you use 1 for NOT and 2 for AND.

• Fixed.

• 27 Dec 2012 17:48 UTC
4 points

Some­thing I’ve been won­der­ing for a while now: if con­cepts like “nat­u­ral num­ber” and “set” can’t be ad­e­quately pinned down us­ing first-or­der logic, how the heck do we know what those words mean? Take “nat­u­ral num­ber” as a given. The phrase “set of nat­u­ral num­bers” seems perfectly mean­ingful, and I feel like I can clearly imag­ine its mean­ing, but I can’t see how to define it.

The best ap­proach that comes to my mind: for all n, it’s easy enough to define the con­cept “set of nat­u­ral num­bers less than n”, so you sim­ply need to take the limit of this con­cept as n ap­proaches in­finity. But the “limit of a con­cept” is not ob­vi­ously a well-defined no­tion.

• I don’t think “set” has a fixed mean­ing in mod­ern math­e­mat­ics. At least one promi­nent set the­o­rist talks about the set-the­o­retic mul­ti­verse, which roughly speak­ing means that in­stead of choos­ing par­tic­u­lar truth val­ues of var­i­ous state­ments about sets such as the con­tinuum hy­poth­e­sis, set the­o­rists study all pos­si­ble set the­o­ries given by all pos­si­ble (con­sis­tent) as­sign­ments of truth val­ues to var­i­ous state­ments about sets, and look at re­la­tion­ships be­tween these set the­o­ries.

In prac­tice, it’s not ac­tu­ally a big deal that “set” doesn’t have a fixed mean­ing. Most of what we need out of the no­tion of “set” is the abil­ity to perform cer­tain op­er­a­tions, e.g. take power sets, that have cer­tain prop­er­ties. In other words, we need a cer­tain set of ax­ioms, e.g. the ZF ax­ioms, to hold. Whether or not those ax­ioms have a unique model is less im­por­tant than whether or not they’re con­sis­tent (that is, have at least one model).

There are also some math­e­mat­i­ci­ans (strict fini­tists) who re­ject the ex­is­tence of the “set of nat­u­ral num­bers”…

• The stan­dard ap­proach in foun­da­tions of math­e­mat­ics is to con­sider a spe­cial first or­der the­ory called ZFC, it de­scribes sets, whose el­e­ments are them­selves sets. In­side this the­ory you can en­code all other math­e­mat­ics us­ing sets for ex­am­ple by the Von Neu­mann con­struc­tion of or­di­nals. Then you can re­strict your­self to the finite or­di­nals and ver­ify the Peano ax­ioms, in­clud­ing the prin­ci­ple of in­duc­tion which you can now for­mu­late us­ing sets. So ev­ery­thing turns out to be unique and pinned down in­side your set the­ory.

What about pin­ning down your set the­ory? Well most math­e­mat­i­ci­ans don’t worry about set the­ory. The set the­o­rists seem to be quite fine with it not be­ing pinned down, but are some­times need to be care­ful about in­side which model they are work­ing. A very use­ful con­se­quence of set the­ory not be­ing pinned down is a con­struc­tion called forc­ing, which al­lows you to prove the in­de­pen­dence of ZFC from the con­tinuum hy­poth­e­sis (there not be­ing a set of re­als which can’t be bi­jected into nei­ther the nat­u­rals nor the re­als). What you do in this con­struc­tion is that you work in­side a model of set the­ory which is countable, which al­lows you to define a spe­cial kind of sub­set that does not ex­ist in the origi­nal model but can be used to cre­ate a new model where cer­tain prop­er­ties fail to hold.

Some peo­ple want to use sec­ond or­der logic, talk­ing about prop­er­ties as prim­i­tive ob­jects, to get this kind of pin­point­ing in­stead. The stan­dard crit­i­cism to this is that you need to for­mal­ise what you mean by prop­er­ties through ax­ioms and rules of in­fer­ence, giv­ing you some­thing quite similar to set the­ory. I’m not very fa­mil­iar with sec­ond or­der logic so can’t elab­o­rate on the differ­ences or similar­i­ties, but it does look like the next post in this se­quence will be about it.

• The thing about ZFC is that it doesn’t feel like “the defi­ni­tion” of a set. It seems like the no­tion of a “set” or a “prop­erty” came first, and then we came up with ZFC as a way of ap­prox­i­mat­ing that no­tion. There are state­ments about sets that are in­de­pen­dent of ZFC, and this seems more like a short­com­ing of ZFC than a short­com­ing of the very con­cept of a set; per­haps we could come up with a philo­soph­i­cal defi­ni­tion of the word “set” that pins the con­cept down pre­cisely, even if it means re­sort­ing to sub­jec­tive con­cepts like sim­plic­ity or use­ful­ness.

On the other hand, the word “set” doesn’t seem to be as well-defined as we would like it to be. I doubt that there is one unique con­cept that you could call “the set of all real num­bers”, since this con­cept be­haves differ­ent ways in differ­ent set the­o­ries, and I see no ba­sis on which to say one set the­ory or an­other is “in­cor­rect”.

• Math­e­mat­ics and logic are part of a strat­egy that I’ll call “for­mal­iza­tion”. In­for­mal speech leans on (hu­man) biolog­i­cal ca­pa­bil­ities. We com­mu­ni­cate ideas, in­clud­ing ideas like “nat­u­ral num­ber” and “set” us­ing in­for­mal speech, which does not de­pend on defi­ni­tions. In­for­mal speech is not quite point­ing and grunt­ing, but point­ing and grunt­ing is per­haps a use­ful car­toon of it. If I point and grunt to a dead leaf, that does not nec­es­sar­ily pin down any par­tic­u­lar con­cept such as “dead leaves”. It could just as well in­di­cate the con­cept “things which are dry on top and wet on bot­tom”—in­clud­ing armpits. There’s a Tal­mu­dic story about a de­bate that might be rele­vant here. Nev­er­the­less (by shared biol­ogy) in­for­mal com­mu­ni­ca­tion is pos­si­ble.

In ex­e­cut­ing the strat­egy of for­mal­iza­tion, we do some in­for­mal ar­gu­men­ta­tion to jus­tify and/​or at­tach mean­ing to cer­tain sym­bols and/​or premises and/​or rules. Then we do a chain of for­mal ma­nipu­la­tions. Then we do some in­for­mal ar­gu­men­ta­tion to in­ter­pret the re­sult.

Model the­ory is a par­tic­u­lar strat­egy of jus­tify­ing and/​or at­tach­ing mean­ing to things. It con­sists of dis­cussing things called “mod­els”, pos­si­bly us­ing coun­ter­fac­tu­als or pos­si­ble wor­lds as in­tu­ition boost­ers. Then it defines the mean­ing of some strings of sym­bols first by refer­ence to par­tic­u­lar mod­els, and then “val­idity” by refer­ence to all pos­si­ble mod­els, and ar­gues that cer­tain rules for ma­nipu­lat­ing (e.g. sim­plify­ing) strings of sym­bols are “val­idity-pre­serv­ing”.

Model the­ory is com­pel­ling, per­haps be­cause it seems to offer “thicker” foun­da­tions. But you do not have to go through model the­ory in or­der to do the strat­egy of for­mal­iza­tion. You can jus­tify and/​or at­tach mean­ing to your for­mal sym­bols and/​or rules di­rectly. A sim­ple ex­am­ple is if you write down se­quences of sym­bols, ex­plain how to “pro­nounce” them, and then say “I take these ax­ioms to be self-ev­i­dent.”.

One prob­lem with model the­ory from my per­spec­tive is that it puts too much in the metathe­ory (the in­for­mal ar­gu­men­ta­tion around the for­mal sym­bol-ma­nipu­la­tion). Set the­ory seems to me like some­thing that should be in the for­mal (even, ma­chine-check­able?) part, not in the metathe­ory. It’s cer­tainly pos­si­ble to have two lay­ers of for­mal­ity, which in prin­ci­ple I have no ob­jec­tion to, but model the­o­ret­i­cal ar­gu­ments of­ten seem to ne­glect the (in­for­mal) work to jus­tify and at­tach mean­ing to the outer layer. Fur­ther­more, mak­ing the for­mal part more com­pli­cated has costs.

I think this pa­per by Simp­son: Par­tial Real­iza­tions of Hilbert’s Pro­gram might be illu­mi­nat­ing.

To me, it’s all about re­flec­tive equil­ibrium. In our minds, we have this idea about what a “nat­u­ral num­ber” is. We care about this idea, and want to do some­thing us­ing it. How­ever, when we re­al­ize that we can’t de­scribe it, per­haps we worry that we are just com­pletely con­fused, and think­ing of some­thing that has no con­nec­tion to re­al­ity, or maybe doesn’t even make sense in the­ory.

How­ever, it turns out that we do have a good idea of what the nat­u­ral num­bers are, in the­ory...a sys­tem de­scribed by the Peano ax­ioms. Th­ese are given in sec­ond-or­der logic, but, like first-or­der logic, the se­man­tics are built in to how we think about col­lec­tions of things. If you can’t pin down what you’re talk­ing about with ax­ioms, it’s a pretty clear sign that you’re con­fused.

How­ever, find­ing ac­tual (syn­tac­tic) in­fer­ence rules to deal with col­lec­tions of things proved tricky. Many peo­ple’s in­nate idea of how col­lec­tions of things work come out to some­thing like naive set the­ory. In 1901, Ber­trand Rus­sell found a flaw in the lens...Rus­sell’s para­dox. So, to keep re­flec­tive equil­ibrium, math­e­mat­i­ci­ans had to think of new ways of deal­ing with col­lec­tions. And this pro­ject yielded the ZFC ax­ioms. Th­ese can be trans­lated into in­fer­ence rules /​ ax­ioms for sec­ond-or­der logic, and per­son­ally that’s what I’d pre­fer to do (but I haven’t had the time yet to for­mal­ize all of my own math­e­mat­i­cal in­tu­itions).

Now, as a con­se­quence of Gödel’s first in­com­plete­ness the­o­rem (there are ac­tu­ally two, only the first is dis­cussed in the origi­nal post), no sys­tem of sec­ond-or­der logic can prove all truths about ar­ith­metic. Since we are able to pin down ex­actly one model of the nat­u­ral num­bers us­ing sec­ond-or­der logic, that means that no com­putable set of valid in­fer­ence rules for sec­ond-or­der logic is com­plete. So we pick out as many in­fer­ence rules as we need for a cer­tain prob­lem, check with our in­tu­ition that they are valid, and press on.

If some­one found an in­con­sis­tency in ZFC, we’d know that our in­tu­ition wasn’t good enough, and we’d up­date to differ­ent ax­ioms. And this is why, some­times, we should definitely use first-or­der Peano ar­ith­metic...be­cause it’s prov­ably weaker than ZFC, so we see it as more likely to be con­sis­tent, since our in­tu­itions about num­bers are stronger than our in­tu­itions about groups of things, es­pe­cially in­finite groups of things.

All of this talk can be bet­ter for­mal­ized with or­di­nal anal­y­sis, but I’m still just be­gin­ning to learn about that my­self, and, as I hinted at be­fore, I don’t think I could for­mally de­scribe a sys­tem of sec­ond-or­der logic yet. I’m busy with a lot of things right now, and, as much as I en­joy study­ing math, I don’t have the time.

• Se­cond-or­der logic.

• So ev­ery­one in the hu­man-su­pe­ri­or­ity crowd gloat­ing about how they’re su­pe­rior to mere ma­chines and for­mal sys­tems, be­cause they can see that Godel’s State­ment is true just by their sa­cred and mys­te­ri­ous math­e­mat­i­cal in­tu­ition… ”...Is ac­tu­ally com­mit­ting a hor­ren­dous log­i­cal fal­lacy [...] though there’s a less stupid ver­sion of the same ar­gu­ment which in­vokes sec­ond-or­der logic.”

So… not ev­ery­one. In Godel, Escher, Bach, Hofs­tadter pre­sents the sec­ond-or­der ex­pla­na­tion of Godel’s In­com­plete­ness The­o­rem, and then goes on to dis­cuss the “hu­man-su­pe­ri­or­ity” crowd. Granted, he doesn’t give it much weight—but for rea­sons that have noth­ing to do with first- ver­sus sec­ond-or­der logic.

Don’t bash a camp just be­cause some of their ar­gu­ments are bad. Bash them be­cause their strongest ar­gu­ment is bad, or shut up.

(To avoid mi­s­un­der­stand­ing: I think said camp is in fact wrong.)

• The rea­son it’s not ran­dom-straw­man is that the hu­man-su­pe­ri­or­ity crowd claims we have a mys­ti­cal abil­ity to see im­pli­ca­tions that ma­chines can’t. If some of them, while mak­ing this claim, ac­tu­ally fail at ba­sic logic, the irony is not ir­rele­vant—it illus­trates the point, “No, hu­mans re­ally aren’t bet­ter at Godelian rea­son­ing than ma­chines would be.”

• Why is the mys­ti­cal abil­ity to see im­pli­ca­tions that ma­chines can’t mu­tu­ally ex­clu­sive with the abil­ity to fail at ba­sic logic?

• It’s not log­i­cally ex­clu­sive. It’s just that the only ev­i­dence for the ex­is­tence of this abil­ity comes from log­i­cal rea­son­ing done by peo­ple. Which con­tains failures at ba­sic logic.

• I didn’t eval­u­ate the strongest ar­gu­ments for the hu­man-su­pe­rior crowd, be­cause I find the ques­tion ir­rele­vant. If some ev­i­dence comes from ar­gu­ments which have not been shown to be flawed, then there is rea­son to be­lieve that some hu­mans are bet­ter at Godelian rea­son­ing than ma­chines can be.

The re­sponse wasn’t “All of the ev­i­dence is log­i­cally flawed”. The re­sponse was

If some of them, while mak­ing this claim, ac­tu­ally fail at ba­sic logic, the irony is not ir­rele­vant—it illus­trates the point, “No, hu­mans re­ally aren’t bet­ter at Godelian rea­son­ing than ma­chines would be.”

• I dis­agree with EY. I think all of them, while mak­ing this claim, fail at ba­sic logic, al­though their failures come in sev­eral kinds.

This is based on ar­gu­ments I have seen (all flawed) and my in­abil­ity to come up my­self with a non-flawed ar­gu­ment for that po­si­tion. So if you think I am wrong, please point to ev­i­dence for hu­man-only mys­ti­cal pow­ers, which is not log­i­cally flawed.

• Sup­pose that hu­mans had the abil­ity to cor­rectly in­tuit things in the pres­ence of in­ad­e­quate or mis­lead­ing ev­i­dence. That abil­ity would re­quire that hu­mans not fol­low first-or­der logic in draw­ing all of their con­clu­sions. There­fore, if did not fol­low perfect logic it would be (very weak) ev­i­dence that they have su­pe­rior abil­ity to draw cor­rect con­clu­sions from in­ad­e­quate or mis­lead­ing ev­i­dence.

Hu­mans do not always fol­low perfect logic.

I don’t have good ev­i­dence, but I haven’t searched the available space yet.

• This is neg­ligibly weak ev­i­dence, not even strong enough to raise the hy­poth­e­sis to the level of con­scious con­sid­er­a­tion. (Good ev­i­dence would be e.g. hu­mans be­ing ac­tu­ally ob­served to de­duce things bet­ter than the ev­i­dence available to them would seem to al­low.)

Con­sider that there are much much bet­ter rea­sons for hu­mans not to fol­low logic perfectly. The stronger these are, the less ev­i­dence your ap­proach gen­er­ates, be­cause the fact hu­mans are not log­i­cal does not re­quire ad­di­tional ex­pla­na­tion.

Logic is hard (and un­likely to be perfect when evolv­ing an ex­ist­ing com­plex brain). Logic is ex­pen­sive (in time taken to think, calories used, maybe brain size, etc.) Ex­ist­ing hu­man adap­ta­tions in­terfere with logic (e.g. use of opinions as sig­nal­ling; the difficulty of ly­ing with­out com­ing to be­lieve the lie; var­i­ous bi­ases). Ex­ist­ing hu­man adap­ta­tions which are less good than perfect logic would be, but are good enough to make the de­vel­op­ment of perfect logic a bad value propo­si­tion. There are oth­ers.

• Ever known some­one to jump to the cor­rect con­clu­sion? Ever tried to de­ter­mine how likely it is, given that some­one is jump­ing to a con­clu­sion with the available ev­i­dence, that the con­clu­sion that they reach is cor­rect?

Con­sider that sev­eral peo­ple have as­serted, ba­si­cally, that they have done the math, and more peo­ple than ex­pected do bet­ter than ex­pected at reach­ing cor­rect con­clu­sions with in­ad­e­quate in­for­ma­tion. I haven’t gath­ered em­piri­cal data, so I nei­ther sup­port nor re­fute their em­piri­cal claim about the world; do your em­piri­cal data agree, or dis­agree?

• In my per­sonal ex­pe­rience I can’t think off­hand of peo­ple who guessed a cor­rect an­swer when a ran­dom guess, given available ev­i­dence, would have been very un­likely to be cor­rect.

Some­times peo­ple do guess cor­rectly; far more of­ten they guess wrong, and I ex­pect the two to be bal­anced ap­pro­pri­ately, but I haven’t done stud­ies to check this.

Can you please point me to these peo­ple who have done the math?

• I played the Cal­ibra­tion Game for a while and I got right more than 60% of the ques­tions to which I had guessed with “50%”. It kind-of freaked me out. (I put that down to hav­ing heard about one of the things in the ques­tion but not con­sciously re­mem­ber­ing it, and sub­con­sciously pick­ing it, and since the big­ger some­thing is the more likely I am to have heard about it… or some­thing like that.)

• I have like 53% − 55% in the 50% cat­e­gory. 60% seems high. Since I have some knowl­edge of the ques­tions I would ex­pect to an­swer above above 50% cor­rectly.

• The hu­man-su­pe­ri­orists make the claim that they have done the math; I haven’t checked their work, be­cause I find the ques­tion of whether hu­mans can be bet­ter than a ma­chine can be are ir­rele­vant; the rele­vant fact is whether a given hu­man us bet­ter than a given ma­chine is, and the an­swer there is rel­a­tively easy to find and very hard to gen­er­al­ize.

• So, can you point me to some spe­cific claims made by these hu­man-su­pe­ri­orists? I know of sev­eral, but not any that claim to back up their claims with data or ev­i­dence.

• The best hu­man Go play­ers re­main bet­ter than the best com­puter Go play­ers. In a finite task which is ex­clu­sively solv­able logic, hu­mans are su­pe­rior. Un­til re­cently, that was true of Chess as well.

• There seems to be a mi­s­un­der­stand­ing here. We all know of lots of tasks where ma­chines cur­rently perform much worse than hu­mans do (and vice versa). What I thought we were dis­cussing was hu­mans who could ar­rive at cor­rect an­swers with­out ap­par­ently hav­ing suffi­cient in­for­ma­tion to do so, and re­search which failed to turned up ex­pla­na­tions based on data available to these peo­ple.

• What would the method­ol­ogy of such re­search look like? One could eas­ily claim that poker play­ers vary in skill and luck, or one could claim that poker play­ers vary in their abil­ity to make cor­rect guesses about the state of the table based on the finite in­for­ma­tion available to them. How well do you think a perfect ma­chine would do in a large poker tour­na­ment?

• What would the method­ol­ogy of such re­search look like?

I don’t know, you’re the one who said you’ve seen peo­ple claiming they’ve done this re­search.

How well do you think a perfect ma­chine would do in a large poker tour­na­ment?

Machines are not nearly good enough yet at rec­og­niz­ing fa­cial and ver­bal clues to do as well as hu­mans in poker. And poker re­quires rel­a­tively lit­tle mem­o­riza­tion and calcu­la­tions, and hu­mans do no worse than ma­chines. So a ma­chine (with a cam­era and micro­phone) would lose to the best hu­man play­ers right now.

OTOH, if a poker game is con­ducted over the net­work, and no in­for­ma­tion (like speech /​ video) is available of other play­ers, just the moves they make, then I would ex­pect a well writ­ten poker-play­ing ma­chine to be bet­ter than al­most all hu­man play­ers (who are vuln­er­a­ble to bi­ases) and no worse than the best hu­man play­ers.

• The best com­puter player on KGS is cur­rently ranked 6 dan, hav­ing risen from 1 dan since 2009. I’d ex­pect the best pro­grams to beat the best am­a­teur play­ers within the next five years, and pro­fes­sion­als in 10–15.

• That long? How long un­til you be­lieve Go is solved?

• I think it’s worth ad­dress­ing that kind of ar­gu­ment be­cause it is fairly well known. Pen­rose, for ex­am­ple, makes a huge deal over it. Although mostly I think of Pen­rose as a case study in how be­ing a great math­e­mat­i­cian doesn’t make you a great philoso­pher, he’s still fairly visi­ble.

• A few things.

a) I’m a lit­tle con­fused by the dis­cus­sion of Can­tor’s ar­gu­ment. As I un­der­stand it, the ar­gu­ment is valid in first-or­der logic, it’s just that the con­clu­sion may have differ­ent se­man­tics in differ­ent mod­els. That is, the state­ment “the set X is un­countable” is cashed out in terms of set the­ory, and so if you have a non-stan­dard model of set the­ory, then that state­ment may have non-stan­dard se­mat­ics.

This is all made hor­ren­dously con­fus­ing by the fact that when we do model the­ory we tend to model our do­mains us­ing sets. So even in a non-stan­dard model of set the­ory we’ll usu­ally be talk­ing about sets do­ing the mod­el­ling, and so we may ac­tu­ally be us­ing a set that is countable in the “outer” set the­ory in which we’re work­ing, but not in the “in­ner” the­ory which we’re mod­el­ling.

What the re­quire­ment to use set the­ory to talk about first-or­der logic says about the sta­tus of logic is a whole other hope­lessly cir­cu­lar ket­tle of fish.

Any­way, I think that’s ba­si­cally what you were say­ing, but I ac­tu­ally found your ex­pla­na­tion harder to fol­low than the usual one. Which is un­usual, since I nor­mally think your ex­pla­na­tions of mathsy stuff are very good!

b) I kind of feel like Godel’s the­o­rem could be dropped from this post. While it’s nice to re­it­er­ate the gen­eral point that “If you’re us­ing Godel’s the­o­rem in an ar­gu­ment and you’re not a pro­fes­sional lo­gi­cian, you should prob­a­bly stop”, I don’t think it ac­tu­ally helps the thrust of this post much. I’d just use Com­pact­ness.

c) The Com­pact­ness the­o­rem is the best rea­son not to use first-or­der logic. Se­ri­ously, it’s weird as hell. We’re all so used to it from do­ing model the­ory etc, but it’s pretty counter-in­tu­itive full stop; doesn’t cor­re­spond to how we nor­mally use logic; and leads to most of the “re­mark­able” prop­er­ties of first-or­der logic.

Your se­man­tics is im­pov­er­ished if you can prove ev­ery­thing with finite syn­tac­ti­cal proofs. Down with Com­pact­ness!

• a) I’m a lit­tle con­fused by the dis­cus­sion of Can­tor’s ar­gu­ment. As I un­der­stand it, the ar­gu­ment is valid in first-or­der logic, it’s just that the con­clu­sion may have differ­ent se­man­tics in differ­ent mod­els. That is, the state­ment “the set X is un­countable” is cashed out in terms of set the­ory, and so if you have a non-stan­dard model of set the­ory, then that state­ment may have non-stan­dard se­mat­ics.

More clearly—“X is un­countable” means “there is no bi­jec­tion be­tween X and a sub­set of N”, but “there” stilll means “within the given model”.

• Ex­actly (I’m as­sum­ing by sub­set you mean non-strict sub­set). Cru­cially, a non-stan­dard model may not have all the bi­jec­tions you’d ex­pect it to, which is where EY comes at it from.

• I’m as­sum­ing by sub­set you mean non-strict subset

I was, but that’s not nec­es­sary—a countably in­finite set can be bi­jec­tively mapped onto {2, 3, 4, …} which is a proper sub­set of N af­ter all! ;-)

• Oh yeah—brain fail ;)

• b) I kind of feel like Godel’s the­o­rem could be dropped from this post. While it’s nice to re­it­er­ate the gen­eral point that “If you’re us­ing Godel’s the­o­rem in an ar­gu­ment and you’re not a pro­fes­sional lo­gi­cian, you should prob­a­bly stop”, I don’t think it ac­tu­ally helps the thrust of this post much. I’d just use Com­pact­ness.

Disagree. I ac­tu­ally un­der­stand Godel’s in­com­plete­ness the­o­rem, and started out mi­s­un­der­stand­ing it un­til a dis­cus­sion similar to the one pre­sented in this post, so this may help clear up the in­com­plete­ness the­o­rem for some peo­ple. And un­like the Com­pact­ness the­o­rem, Godel’s com­plete­ness the­o­rem at least seems fairly in­tu­itive. Prov­ing the ex­is­tence of non­stan­dard mod­els from the Com­pact­ness the­o­rem seems kind of like pul­ling a rab­bit out of a hat if you can’t show me why the Com­pact­ness the­o­rem is true.

Your se­man­tics is im­pov­er­ished if you can prove ev­ery­thing with finite syn­tac­ti­cal proofs.

Do you have any ba­sis for this claim?

• I ab­solutely agree that this will help peo­ple stop be­ing con­fused about Godel’s the­o­rem, I just don’t know why EY does it in this par­tic­u­lar post.

Do you have any ba­sis for this claim?

Nope, it’s pure polemic ;) In­tu­itively I feel like it’s a re­al­ism/​in­stru­men­tal­ism is­sue: claiming that the only things which are true are prov­able feels like col­laps­ing the true and the know­able. In this case the de­ci­sion is about which tool to use, but us­ing a tool like first-or­der logic that has these weird prop­er­ties seems sus­pi­cious.

• Your se­man­tics is im­pov­er­ished if you can prove ev­ery­thing with finite syn­tac­ti­cal proofs.

Isn’t the know­able limited to what can be known with finite chains of rea­son­ing, what­ever your base logic?

• Sure. So you’re not go­ing to be able to prove (and hence know) some true state­ments. You might be able to do some meta-rea­son­ing about your logic to figure some of these out, al­though quite how that’s sup­posed to work with­out re­quiring the con­text of set the­ory again, I’m not re­ally sure.

• bryj­nar: I think the point is that the met­a­log­i­cal anal­y­sis that hap­pens in the con­text of set the­ory is still a finite syn­tac­ti­cal proof. In es­sense, all math­e­mat­ics can be re­duced to finite syn­tac­ti­cal proofs in­side of ZFC. Any­thing that re­ally, truly, re­quires in­finite proof in ac­tual math is un­know­able to ev­ery­one, su­per­s­mart AI in­cluded.

• Ab­solutely, but it’s one that hap­pens in a differ­ent sys­tem. That can be rele­vant. And I quite agree: that still leaves some things that are un­know­able even by su­per­s­mart AI. Is that sur­pris­ing? Were you ex­pect­ing an AI to be able to know ev­ery­thing (even in prin­ci­ple)?

• No, it is not sur­pris­ing… I’m just say­ing that say­ing that the se­man­tics is im­pov­er­ished if you only use finite syn­tac­ti­cal proof, but not to any de­gree that can be fixed by just be­ing re­ally re­ally re­ally smart.

• By se­man­tics I mean your no­tion of what’s true. All I’m say­ing is that if you think that you can prove ev­ery­thing that’s true, you prob­a­bly have a an overly weak no­tion of truth. This isn’t nec­es­sar­ily a prob­lem that needs to be “fixed” by be­ing re­ally smart.

Also, I’m not say­ing that our no­tion of proof is too weak! Look­ing back I can see how you might have got the im­pres­sion that I thought we ought to switch to a sys­tem that al­lows in­finite proofs, but I don’t. For one thing, it wouldn’t be much use, and sec­ondly I’m not even sure if there even is such a proof sys­tem for SOL that is com­plete.

• My im­pres­sion (which might be par­tially a re­sult of not un­der­stand­ing sec­ond or­der logic well enough) is that log­i­cal pin­point­ing is hope­less in at least two senses: (1) it’s not pos­si­ble to syn­tac­ti­cally rep­re­sent suffi­ciently com­pli­cated struc­tures (such as ar­ith­metic and par­tic­u­lar set the­o­retic uni­verses) in some ways, and (2) try­ing to cap­ture par­tic­u­lar struc­tures that are in­tu­itively or oth­er­wise iden­ti­fied by hu­mans is like con­cep­tual anal­y­sis of wrong ques­tions, the in­tu­itions typ­i­cally don’t iden­tify a unique idea, and work­ing on figur­ing out which class of ideas they vaguely iden­tify is less use­ful than study­ing par­tic­u­lar more spe­cific ideas cho­sen among the things par­tially mo­ti­vated by the in­tu­ition. For ex­am­ple, in set the­ory there are many ax­ioms that could go ei­ther way (like the con­tinuum hy­poth­e­sis) that as a re­sult iden­tify differ­ent set the­o­retic uni­verses.

What’s left is to rea­son with the­o­ries that are weaker than is nec­es­sary to pin­point par­tic­u­lar mod­els (and to in­tro­duce ad­di­tional data to stipu­late some prop­er­ties we need, in­stead of ex­pect­ing such prop­er­ties to fall out on their own). On the other hand, physics, if seen as a model, seems to make the se­man­tic view of math­e­mat­ics more rele­vant, but it’s prob­a­bly isn’t fully know­able in a similar sense. (Learn­ing more about phys­i­cal facts might mo­ti­vate study­ing differ­ent weak the­o­ries, which seems to be some­what analo­gous to this se­quence’s “mixed refer­ence”.)

• Nit­pick, the Lowen­heim-Skolem The­o­rems arre not quite that gen­eral. If we al­low lan­guages with un­countably many sym­bols and sets of un­countably many ax­ioms then we can lower bound the car­di­nal­ity (by bring­ing in un­countably many con­stants and for each pair adding the ax­iom that they are not equal). The tech­ni­cally cor­rect claim would be that any set of ax­ioms ei­ther have a finite up­per bound on their mod­els, or have mod­els of ev­ery in­finite car­di­nal­ity at least as large as the alpha­bet in which they are ex­pressed.

But at least it’s (the Com­pact­ness The­o­rem) sim­pler than the Com­plete­ness Theorem

It is!? Does any­one know a proof of Com­pact­ness that doesn’t use com­plete­ness as a lemma?

• It is!? Does any­one know a proof of Com­pact­ness that doesn’t use com­plete­ness as a lemma?

There’s ac­tu­ally a di­rect one on ProofWiki. It’s con­struc­tive, even, sort of. (Roughly: take the ul­tra­product of all the mod­els of the finite sub­sets with a suit­able choice of ul­tra­filter.) If you’ve worked with ul­tra­prod­ucts at all, and maybe if you haven’t, this proof is pretty in­tu­itive.

As Qiaochu_Yuan points out, this is equiv­a­lent to the ul­tra­filter lemma, which is in­de­pen­dent of ZF but strictly weaker than the Ax­iom of Choice. So, maybe it’s not that in­tu­itive.

• That’s re­ally beau­tiful, thanks.

• It is!? Does any­one know a proof of Com­pact­ness that doesn’t use com­plete­ness as a lemma?

Yes: in­stead of prov­ing “A the­ory that has no model has a finite proof of a con­tra­dic­tion” you prove the equiv­a­lent con­verse “If ev­ery finite sub­set of a the­ory has a model, then the the­ory has a model” (which is why the the­o­rem is named af­ter com­pact­ness at all) by con­struct­ing a chain of model and show­ing that the limit of the chain has a model. Also the origi­nal proof of Goedel used Com­pact­ness to prove Com­plete­ness.

• It is!? Does any­one know a proof of Com­pact­ness that doesn’t use com­plete­ness as a lemma?

Yes. Or, at least, I did once! That’s the way we proved it the logic course I did. The proof is a lot harder. But con­sid­er­ing that the im­pli­ca­tion from Com­plete­ness is pretty triv­ial, that’s not say­ing much.

• Given these re­cent logic-re­lated posts, I’m cu­ri­ous how oth­ers “vi­su­al­ize” this part of math, e.g. what do you “see” when you try to un­der­stand Goedel’s in­com­plete­ness the­o­rem?

(And don’t tell me it’s kit­tens all the way down.)

Things like deriva­tives or con­vex func­tions are re­ally easy in this re­gard, but when some­one starts talk­ing about mod­els, proofs and for­mal sys­tems, my men­tal paint­brush starts do­ing some pretty weird stuff. In ad­di­tion to or­di­nary imagery like bub­bles of half-imag­ined ob­jects, there is also some­thing ma­chine-like in the con­cept of a for­mal sys­tem, for ex­am­ple, like it was im­bued with a po­ten­tial to pro­duce a spe­cific uni­verse of var­i­ous thin­gies in a larger mul­ti­verse (an­other men­tal image)...

Any­way, this is be­com­ing quite hard to de­scribe—and it’s not all due to me be­ing a non-na­tive speaker, so… if any­one is pre­pared to share her mind’s round­abouts, that would be re­ally nice, but apart from that—is there a book, by a pro­fes­sional math­e­mat­i­cian if pos­si­ble, where one can find such rev­e­la­tions?

• You can think of the tech­ni­cal heart of the in­com­plete­ness the­o­rem as be­ing a fixed point the­o­rem. You want to write down a sen­tence G that as­serts “the­ory T does not prove G.” In other words, there is a func­tion which takes as in­put a sen­tence S and out­puts the sen­tence “the­ory T does not prove S,” and you want to find a fixed point of this func­tion. There is a gen­eral fixed point the­o­rem due to Law­vere which im­plies that this func­tion does in fact have a fixed point. It is a more gen­eral ver­sion of what Wikipe­dia calls the di­ag­o­nal lemma. In­ter­est­ingly, it im­plies Can­tor’s the­o­rem, and one way to prove it pro­ceeds es­sen­tially by con­struct­ing a more gen­eral ver­sion of the Y com­bi­na­tor. Yanofsky’s A Univer­sal Ap­proach to Self-Refer­en­tial Para­doxes, In­com­plete­ness and Fixed Points is a good refer­ence.

I men­tion this for two rea­sons. First, there is a lot of vi­sual ma­chin­ery you can bring to bear on the gen­eral sub­ject of fixed point the­o­rems. For ex­am­ple, to vi­su­al­ize the Banach fixed point the­o­rem you can think of a se­quence of copies of the same shape nested in each other and shrink­ing to­wards a sin­gle point (the fixed point), and to vi­su­al­ize the Brouwer fixed point the­o­rem you can draw a bunch of ar­rows in a disk.

Se­cond, there is a graph­i­cal lan­guage, roughly analo­gous to Pen­rose graph­i­cal no­ta­tion, for do­ing com­pu­ta­tions in Carte­sian closed cat­e­gories, and a ver­sion of Law­vere’s the­o­rem can be proven us­ing this graph­i­cal lan­guage. Un­for­tu­nately I don’t know a refer­ence for this; I found the proof while try­ing to un­der­stand the Y com­bi­na­tor and don’t ac­tu­ally know if it’s in the liter­a­ture (but it prob­a­bly is).

• Think­ing about alge­bra (e.g. group the­ory) makes a lot of this make more sense. The defi­ni­tion of a group is a “the­ory”; any par­tic­u­lar group is a “model”. This isn’t a huge rev­e­la­tion or any­thing, but it’s eas­ier to think about these ideas in the con­text of alge­bra (where differ­ent struc­tures that be­have similarly are com­mon­place) rather than ar­ith­metic (where we like think­ing about one “true” pic­ture).

• Vi­sual/​imag­i­na­tive mod­el­ling of math­e­mat­i­cal tasks is not a uni­ver­sal trait.

• How­ever, it’s a use­ful skill.

• Here’s how I vi­su­al­ize Goedel’s in­com­plete­ness the­o­rem (I’m not sure how “vi­sual” this is, but bear with me): I imag­ine the Goedel con­struc­tion over the ax­ioms of first-or­der Peano ar­ith­metic. Clearly, in the stan­dard model, the Goedel sen­tence is true, so we add G to the ax­ioms. Now we con­struct G’ a Goedel sen­tence in this new set, and add G″ as an ax­iom. We go on and on, G‴, etc. Luck­ily that con­struc­tion is com­putable, so we add G^w as a Goedel sen­tence in this new set. We con­tinue on and on, un­til we reach the first un­com­putable countable or­di­nal, at which point we stop, be­cause we have an un­com­putable ax­iom set. Note that Goedel is fine with that—you can have a com­plete first-or­der Peano ar­ith­metic (it would have non-stan­dard mod­els, but it would be com­plete!) -- as long as you are will­ing to live with the fact that you can­not know if some­thing is a proof or not with a mere ma­chine (and yes, Virginia, hu­mans are also mere ma­chines).

• Wait… this will seems stupid, but can’t I just say: “there does not ex­ist x where sx = 0”

nevermind

• +5 insightful

• Yeah, I glaze over here­abouts.

• “Ah, well… some peo­ple be­lieve there is no spoon. But let’s take that up next time.”

Con­grat­u­la­tions, you have just writ­ten a shaggy dog story. :P

• Naah … in a shaggy-dog story, the setup for the pun be­gins at the be­gin­ning of the story. This is just an es­say with a pun at the end.

• an un­stated as­sump­tion in Godels In­com­plete­ness Theorem

Ex­ceuse me I h ave come up with a pos­si­ble way around Godels the­o­rem.

A cru­cial fact in the the­o­rem is that the the­ory T (any ex­ten­sion of PA) can en­code re­cur­sively “x proves y”.

but we well know that there are many fast grow­ing func­tions that can’t be proved to­tal in PA.. thus...

if we define a the­ory of math­e­mat­ics which has a very com­pli­cated (al­gorithm com­plex­ity)defin­tiion of “x proves y” (in ZFC meta-the­ory for ex­am­ple), so fast grow­ing that it can’t be define in T.

then T may be a the­ory con­tain­ing ar­ith­metic for which godels the­o­rem does not ap­ply.. may even a con­sis­tent the­ory T ex­ists than can prove its own con­sis­tency!