No one knows what Peano arithmetic doesn’t know

WARNING: this post re­quires some knowl­edge of math­e­mat­i­cal logic and com­putabil­ity the­ory.

I was just talk­ing with Wei Dai and some­thing came up that seems at once ob­vi­ous and coun­ter­in­tu­itive. Though if the ar­gu­ment is cor­rect, I guess it will be old news to about 50% of the peo­ple who read my posts :-)

Imag­ine you have an or­a­cle that can de­ter­mine if an ar­bi­trary state­ment is prov­able in Peano ar­ith­metic. Then you can try us­ing it as a halt­ing or­a­cle: for an ar­bi­trary Tur­ing ma­chine T, ask “can PA prove that there’s an in­te­ger N such that T makes N steps and then halts?”. If the or­a­cle says yes, you know that the state­ment is true for stan­dard in­te­gers be­cause they’re one of the mod­els of PA, there­fore N is a stan­dard in­te­ger, there­fore T halts. And if the or­a­cle says no, you know that there’s no such stan­dard in­te­ger N be­cause oth­er­wise the or­a­cle would’ve found a long and bor­ing proof in­volv­ing the en­cod­ing of N as SSS...S0, there­fore T doesn’t halt. So your or­a­cle can in­deed serve as a halt­ing or­a­cle.

On the other hand, if you had a halt­ing or­a­cle to be­gin with, you could use it as a prov­abil­ity or­a­cle for PA: “if a pro­gram suc­ces­sively enu­mer­ates all proofs in PA, will it ever find a proof for such-and-such state­ment?”

So hav­ing a prov­abil­ity or­a­cle for PA or any other con­sis­tent for­mal sys­tem that proves some valid ar­ith­metic truths (like ZFC) is equiv­a­lent to hav­ing a halt­ing or­a­cle, and thus leads to a prov­abil­ity or­a­cle for any other for­mal sys­tem. In other words, if you knew all about the log­i­cal im­pli­ca­tions of PA, then you would also know all about the log­i­cal im­pli­ca­tions of ZFC and all other for­mal sys­tems. Hee hee.

ETA: this line leads to a non­triv­ial ques­tion. Is there a for­mal sys­tem (not talk­ing about the stan­dard in­te­gers, I guess) whose prov­abil­ity or­a­cle is strictly weaker than the halt­ing or­a­cle, but still un­com­putable?

ETA 2: the ques­tion seems to be re­solved, see Zetetic’s com­ment and my re­ply.

• Is there a for­mal sys­tem (not talk­ing about the stan­dard in­te­gers, I guess) whose prov­abil­ity or­a­cle is strictly weaker than the halt­ing or­a­cle, but still un­com­putable?

I did some read­ing and it looks like while there are some proofs of the ex­is­tence of a dense set of in­ter­me­di­ate Tur­ing de­grees, it’s a bit difficult to pin down definite prob­lems of in­ter­me­di­ate de­gree. I found one pa­per that pos­tu­lates a cou­ple of pos­si­bly in­ter­me­di­ate de­gree prob­lems.

This ar­ti­cle (same au­thor) talks about some of the sur­round­ing is­sues and some the difficul­ties with prov­ing the ex­is­tence of an in­ter­me­di­ate com­pu­ta­tional pro­cess.

Given those difficul­ties, it isn’t clear to me that in­ter­me­di­ate proof or­a­cles for for­mal sys­tems ex­ist and if they do it seems like that might be non-triv­ial, but I’m definitely not the best per­son to ask.

In a similar vein, it was shown by Fefer­man that deriv­abil­ity in a for­mal the­ory fully reﬂects the struc­ture of the r.e. de­grees: for ev­ery r.e. de­gree d there is an ax­iom­a­ti­z­able the­ory whose col­lec­tion of the­o­rems has de­gree ex­actly d, see [10].

And [10] re­solves to:

[10] S. Fefer­man. De­grees of un­solv­abil­ity as­so­ci­ated with classes of for­mal­ized the­o­ries. J. Sym­bolic Logic, 22:161–175, 1957.

I guess that’s enough in­for­ma­tion to an­swer my ques­tion. Thanks a lot!

• Some­thing is go­ing on with my com­ment, the mid­dle sec­tion keeps dis­ap­pear­ing.

• I found an­other pa­per with an in­ter­est­ing re­sult (un­for­tu­nately be­hind a pay wall). It asks what range of de­grees oc­cur for sub­the­o­ries of ar­ith­metic and con­cludes that a de­gree a is as­so­ci­ated with these the­o­ries iff it’s a com­plete de­gree. What does that mean?

Defi­ni­tion 10 A de­gree of re­cur­sive un­solv­abil­ity a is said to be com­plete if there ex­ists a de­gree b such that b’ = a (Ac­cord­ing to Freiberg’s the­o­rem [6, p.265] a de­gree a is com­plete iff 0′<= a).

That makes sense be­cause b’ is ba­si­cally a Tur­ing jump from b, but it’s bad be­cause 0′ is the de­gree of the halt­ing prob­lem. The first Tur­ing jump from de­cia­ble the­o­ries is of de­gree equal to the halt­ing prob­lem. So it looks like any un­de­cid­able (in dis­tinc­tion from Pres­berger and other de­cid­able the­o­ries) first or­der sub­sys­tems of ar­ith­metic, which to me would be the most in­tu­itive the­o­ries, are go­ing to be at least as strong as the halt­ing prob­lem. That is, if I’m read­ing this right—proof the­ory is sort of a hobby and I’m mostly self-taught.

• A more spe­cific state­ment of the re­sult from the pa­per is:

Lemma 1 Sup­pose that the the­ory T is omega con­sis­tent with rep­sect to some for­mula P(y) and that T has a finitely ax­iom­a­ti­z­able sub­the­ory S satis­fy­ing

(i) Each re­cur­sive re­la­tion is defin­able in S

(ii) For ev­ery m = 0, 1, …., $\\vdash\_s P\(\\bigtriangleup\_m\$)

Then each sub­the­ory of T is of com­plete degree

Also:

Co­ral­lary 6 Let T be the the­ory ZF or any ex­ten­sion of ZF. If T is omega con­sis­tent with re­spect to the for­mula $y \\in \\omega$ then the de­grees of sub­the­o­ries of T are ex­actly the com­plete de­grees.

ETA: Is this what you were refer­ring to in:

Is there a for­mal sys­tem (not talk­ing about the stan­dard in­te­gers, I guess)

I’m not sure, I don’t see a re­lated re­ply/​com­ment. Either way, I’m not 100% sure I’m fol­low­ing all of the ar­gu­ments in the pa­pers, but it ap­pears that the the­o­ries that are of in­ter­me­di­ate de­gree are nec­es­sar­ily very un­usual and com­pli­cated, and I’m not sure how fea­si­ble it would be to con­struct one ex­plic­itly.

ETA2: I found yet an­other in­ter­est­ing pa­per that seems to state that find­ing a nat­u­ral ex­am­ple of a prob­lem of in­ter­me­di­ate de­gree is a long stand­ing open prob­lem.

• Thanks again for tak­ing the time to parse all that!

ETA: Is this what you were refer­ring to in:

Yeah, kind of. I didn’t know the re­sults but for some rea­son felt that sub­the­o­ries of ar­ith­metic shouldn’t lead to in­ter­me­di­ate de­grees.

• No prob­lem! It’s an in­ter­est­ing topic with lots of sur­round­ing re­sults that are some­what sur­pris­ing (at least to me).

• More pow­er­ful for­mal sys­tems are not more pow­er­ful be­cause they know more stuff. They’re more pow­er­ful be­cause they have more con­fi­dence. PA proves that PA+Con(PA) proves Con(PA) (the proof, pre­sum­ably, is not very long), but PA does not trust PA+Con(PA) to be ac­cu­rate. ZFC is even more con­fi­dent—has even fewer mod­els—and so is even stronger. (Maybe it even has no mod­els!)

• More pow­er­ful for­mal sys­tems are not more pow­er­ful be­cause they know more stuff. They’re more pow­er­ful be­cause they have more con­fi­dence.

That’s an awe­some way of putting it, thanks!

PA proves that PA+Con(PA) proves Con(PA)

Duh, PA proves that PA+X proves X for any X, be­cause X is one of the ax­ioms of PA+X. Did you mean some less triv­ial ex­am­ple?

• No. I meant to in­clude a triv­ial ex­am­ple. I be­lieved that it would help clar­ify the point.

• Well, that ar­gu­ment only goes through if the other the­ory is re­cur­sively enu­mer­able, so PA isnt as awe­some as you make it sound.

• Agreed. For ex­am­ple, we can’t learn “all truths about the in­te­gers” by boot­strap­ping from PA in this way. But we can get all of for­mal­ist math­e­mat­ics.

• Zetetic gave a good re­sponse. I’d just like to note that the ti­tle is slightly in­ac­cu­rate. Con­sider for ex­am­ple Good­stein’s the­o­rem. PA can’t know whether Good­stein’s the­o­rem is true or not, but based on its truth in very weak, rea­son­ably in­tu­itive ex­ten­sions of PA we should prob­a­bly be­lieve its truth. So we can know some­thing that PA doesn’t know albeit in a weak sense.

• The ti­tle is a refer­ence to No One Knows What Science Doesn’t Know, from which I in­fer that it’s sup­posed to be read as “There is some set {what PA knows}. No one can know ex­actly where the bound­aries of this set are.”, not “There is some set {what PA knows}. No one can know the truth value of any propo­si­tion not in this set.”.

• Right.

• I be­lieve the an­swer to your ques­tion is yes. I’m go­ing to just in­ter­pret “for­mal sys­tem” as “first or­der the­ory”, and then try to do the most straight­for­ward thing.

Take a lan­guage L of in­ter­me­di­ate de­gree, as con­structed via the pri­or­ity method. I’d like to just take the strings (or num­bers) in this lan­guage to be the the­ory’s ax­ioms. So let the the­ory have some 1-ary re­la­tion, call it R, as well as +, and con­stants 0 and 1. Assert that ev­ery­thing has a suc­ces­sor, just to get the “nat­u­ral num­bers” (with­out hav­ing mul­ti­pli­ca­tion though). Then just in­clude the ax­iom that says R(x) for all x in L, and not R(x) for all x not in L.

It seems pretty clear that the only things this the­ory proves are things that FOL proves, silly things about the suc­ces­sor func­tion, and silly things about R, like “forall x, R(x) → R(x)” and “(R(14) and R(12)) → R(17)” where R(14) is false. So an or­a­cle for the log­i­cal im­pli­ca­tions of this the­ory has the same de­gree as an or­a­cle for L.

Don’t feel like think­ing about how to say/​prove this part for­mally, but maybe some­one can help (or cor­rect) me. Also, for refer­ence, Pres­burger ar­ith­metic is ba­si­cally ar­ith­metic with­out mul­ti­pli­ca­tion, and is de­cid­able.

• I’m a lit­tle out of my depth here, so sorry if my com­ments don’t make sense.

Then just in­clude the ax­iom that says R(x) for all x in L, and not R(x) for all x not in L.

That’s sup­posed to be a r.e. set of ax­ioms, not a sin­gle ax­iom, right? I can eas­ily imag­ine the pro­gram that suc­ces­sively prints the ax­ioms R(x) for all x in L, but how do you enu­mer­ate the ax­ioms not R(x) for all x not in L, given that L is only r.e. and not re­cur­sive? Or am I miss­ing some easy way to have the whole thing as a sin­gle ax­iom with­out pul­ling in the ma­chin­ery for run­ning ar­bi­trary pro­grams and such?

On sec­ond thought, maybe we don’t need the sec­ond part. Just hav­ing R(x) for all x in L could be enough.

It seems pretty clear that the only things this the­ory proves are things that FOL proves, silly things about the suc­ces­sor func­tion, and silly things about R, like “forall x, R(x) → R(x)” and “(R(14) and R(12)) → R(17)” where R(14) is false. So an or­a­cle for the log­i­cal im­pli­ca­tions of this the­ory is ba­si­cally the same as an or­a­cle for L.

I don’t com­pletely un­der­stand why there won’t be an ac­ci­den­tal smart thing among all the silly things...

• I’m a lit­tle out of my depth here, so sorry if my com­ments don’t make sense.

I’m not an ex­pert ei­ther, so I’m prob­a­bly just be­ing unclear

That’s sup­posed to be a r.e. set of ax­ioms, not a sin­gle ax­iom, right? I can eas­ily imag­ine the pro­gram that suc­ces­sively prints the ax­ioms R(x) for all x in L, but how do you enu­mer­ate the ax­ioms not R(x) for all x not in L, given that L is only r.e. and not re­cur­sive? Or am I miss­ing some easy way to have the whole thing as a sin­gle ax­iom with­out pul­ling in the ma­chin­ery for run­ning ar­bi­trary pro­grams and such?

The ax­ioms don’t need to be r.e. If they were, the or­a­cle would never be more helpful than a halt­ing or­a­cle, no?

I don’t com­pletely un­der­stand why there won’t be an ac­ci­den­tal smart thing among all the silly things...

I don’t ei­ther. It’s just a strong in­tu­ition which I’m not sure I can jus­tify, and which might be wrong.

ETA: By silly, I don’t nec­es­sar­ily mean as sim­ple as the ex­am­ples I gave. Ba­si­cally if you have a for­mula phi(S(x), T, F), which holds for ar­bi­trary sen­tences S(x), prov­ably true T, and prov­ably false S, then you can re­place S(x) with R(x), T with R(x in L), and S with R(x not in L). Not sure if that was well ex­plained, but yeah.

At least it looks like my an­swer is cor­rect :). Also my proof should gen­er­al­ize, if it does work. So I would have guessed that Fefer­man’s (stronger) re­sult was true, and I wouldn’t be sur­prised if the ar­gu­ment was along these lines, though maybe the de­tails are harder.

• If they were, the or­a­cle would never be more helpful than a halt­ing or­a­cle, no?

But we want the or­a­cle to be less helpful than the halt­ing or­a­cle...

Any­way, the ques­tion is set­tled now, thanks a lot :-)

• Oops sorry! Ig­nore what I said there. Any­ways, the ax­ioms aren’t nec­es­sar­ily r.e., but as far as I can tell, they don’t need to be.

• My knowl­edge of com­putabil­ity is far from ex­ten­sive so please for­give me if this is a stupid ques­tion.

Does an or­a­cle be­ing able to de­ter­mine if a state­ment is prov­able in Peano ar­ith­metic nec­es­sar­ily be ca­pa­ble of prov­ing that all of the Tur­ing ma­chines that halt for stan­dard in­te­gers do in fact halt? Or to put it an­other way, is there a Tur­ing ma­chine that op­er­ates on some stan­dard in­te­ger that can­not be proved in Peano ar­ith­metic?

Thanks.

• The post wasn’t talk­ing about Tur­ing ma­chines that ac­cept stan­dard in­te­gers as in­put, it was talk­ing about Tur­ing ma­chines with no ar­gu­ments. If such a ma­chine halts, then PA has a proof that just enu­mer­ates all the steps the ma­chine takes be­fore halt­ing.

• Ah thanks, it seems I mis­read the whole “is there an in­te­ger N such that T takes N steps” as “is there an in­te­ger N such that T takes some num­ber of steps then halts”, sorry about that—brain malfunc­tion I guess. Though now that I see what you mean rather than what I thought you meant, good post! Not old news to me, but them I’m rel­a­tively new to com­putabil­ity the­ory.

• So is PA the weak­est sys­tem ca­pa­ble of en­cap­su­lat­ing Tur­ing logic?

• No. You don’t need in­duc­tion to do so. You can just use ar­ith­metic to slowly, slowly eval­u­ate the TM un­til you find some­thing that halts or don’t. The or­a­cle holds all the power.

• Imag­ine you have an or­a­cle that can de­ter­mine if an ar­bi­trary state­ment is prov­able in Peano ar­ith­metic. Then you can try us­ing it as a halt­ing or­a­cle: for an ar­bi­trary Tur­ing ma­chine T, ask “can PA prove that there’s an in­te­ger N such that T makes N steps and then halts?”. If the or­a­cle says yes, you know that the state­ment is true for stan­dard in­te­gers be­cause they’re one of the mod­els of PA, there­fore N is a stan­dard in­te­ger, there­fore T halts. And if the or­a­cle says no, you know that there’s no such stan­dard in­te­ger N be­cause oth­er­wise the or­a­cle would’ve found a long and bor­ing proof in­volv­ing the en­cod­ing of N as SSS...S0, there­fore T doesn’t halt. So your or­a­cle can in­deed serve as a halt­ing or­a­cle.

I don’t think this works. We can’t ex­pect PA to de­cide whether or not any given Tur­ing ma­chine halts. For ex­am­ple, there is a ma­chine which enu­mer­ates the the­o­rems proven by PA and halts if it ever en­coun­ters a proof of 0=1. By in­com­plete­ness, PA will not prove that that this ma­chine halts. (I’m as­sum­ing PA is con­sis­tent.) This ar­gu­ment works for any stronger con­sis­tent the­ory as well, such as ZFC or even much stronger ones. Note: I ba­si­cally stole this ar­gu­ment from Scott Aaron­son.

Note that this is differ­ent from the ques­tion of whether or not the halt­ing prob­lem is re­ducible to the set of the­o­rems of PA (i.e. whether or not the or­a­cle you’ve speci­fied is enough to com­pute whether or not a given TM halts). It’s just that this par­tic­u­lar ap­proach does not give such an al­gorithm.

ETA: I was in er­ror, see replies. In the OP, PA doesn’t need to prove that a non-halt­ing ma­chine doesn’t halt, it only needs to fail to prove that it halts (and it cer­tainly does, if we be­lieve PA is sound).

• The post ar­gues that ask­ing “does this ma­chine halt?” is always equiv­a­lent to ask­ing the or­a­cle “does PA prove that this ma­chine halts?” A coun­terex­am­ple should be a ma­chine for which the an­swers to these two ques­tions are differ­ent. Your ma­chine is a “no” on both ques­tions (it doesn’t halt and PA doesn’t prove that it halts), so it doesn’t seem to be a coun­terex­am­ple.

• Imag­ine you have an or­a­cle that can de­ter­mine if an ar­bi­trary state­ment is prov­able in Peano arithmetic

[...] We can’t ex­pect PA to de­cide whether or not any given Tur­ing ma­chine halts

The or­a­cle isn’t work­ing in PA, it’s just de­cid­ing state­ments that are in PA.

• I was just talk­ing with Wei Dai and some­thing came up that seems at once ob­vi­ous and coun­ter­in­tu­itive.

Agree on the ob­vi­ous part!

In other words, if you knew all about the log­i­cal im­pli­ca­tions of PA, then you would also know all about the log­i­cal im­pli­ca­tions of ZFC and all other for­mal sys­tems.

Ahh, now that is a lit­tle coun­ter­in­tu­itive! Like it.

• For you fi­nal ques­tion, I find it hard to imag­ine a no­tion of “for­mal sys­tem” that does not just mean “lan­guage.” Then an RE for­mal sys­tem is the same as an RE lan­guage. If you in­sist on the ter­minol­ogy of proofs, you can take the words of the lan­guage as ax­ioms and not have any rules of in­fer­ence.

• For your fi­nal ques­tion, I find it hard to imag­ine a no­tion of “for­mal sys­tem” that does not just mean “lan­guage.”

• So you agree that “prov­abil­ity or­a­cle for an RE for­mal sys­tem” is the same as “mem­ber­ship or­a­cle for an RE lan­guage” and your ques­tion is triv­ial?

ETA: No, first or­der lan­guages does re­strict the set of lan­guages. But I ob­ject to this us­age. “For­mal sys­tems” should in­clude more gen­eral sys­tems.

• So hav­ing a prov­abil­ity or­a­cle for PA, or any other for­mal sys­tem that has a model con­tain­ing the stan­dard in­te­gers (like ZFC), is equiv­a­lent to hav­ing a halt­ing oracle

No, you need guaran­tees on the for­mal sys­tem’s com­plex­ity, similar to the ones in Godel’s in­com­plete­ness the­o­rem(s). You also need the for­mal sys­tem to be sound for your ar­gu­ment to carry through. This is stronger than your “has a model con­tain­ing the stan­dard in­te­gers”, and is equiv­a­lent to “has the stan­dard in­te­gers as a model”.

In other words, if you knew all about the log­i­cal im­pli­ca­tions of PA, then you would also know all about the log­i­cal im­pli­ca­tions of ZFC

Note that you’re as­sum­ing here that PA is sound and in par­tic­u­lar con­sis­tent.

Is there a for­mal sys­tem (not talk­ing about the stan­dard in­te­gers, I guess) whose prov­abil­ity or­a­cle is strictly weaker than the halt­ing or­a­cle, but still un­com­putable?

The halt­ing or­a­cle’s un­com­putabil­ity de­gree is the small­est pos­si­ble un­com­putable de­gree, so no.

• The halt­ing or­a­cle’s un­com­putabil­ity de­gree is the small­est pos­si­ble un­com­putable de­gree, so no.

What? That’s false. See http://​​en.wikipe­dia.org/​​wiki/​​Tur­ing_de­gree#Post.27s_problem

ETA: Also, not sure what you are say­ing about sound­ness… =/​

• What? That’s false.

Yeah, re­tracted above. Don’t know what I was think­ing.

ETA: Also, not sure what you are say­ing about sound­ness… =/​

Sup­pose PA is in­con­sis­tent. Then a prov­abil­ity or­a­cle for PA always an­swers “yes”, and is com­pletely use­less as a halt­ing prob­lem or­a­cle. De­bug­ging cousin_it’s ar­gu­ment with this ex­am­ple helps to see where he re­lies on PA be­ing sound, that is, any­thing proved by PA be­ing a true state­ment about N.

• Right. Also there’s always the freaky pos­si­bil­ity that there’s no such thing as the “stan­dard in­te­gers”. After all, we don’t re­ally have any for­mal grounds to be­lieve that they ex­ist, only un­re­li­able evolved in­tu­itions about count­ing ap­ples, and these have already let us down many times (e.g. Rus­sell’s para­dox).

• Sure. You ac­tu­ally need some­thing a bit stronger than sound­ness, in that you want omega-con­sis­tency, right?

I still don’t agree/​un­der­stand with what you two are say­ing about hav­ing the stan­dard in­te­gers as a model, or in­terepret­ing PA with its own ax­ioms, though (or any­thing along the lines of need­ing to con­tain PA). I think this ar­gu­ment holds as long as the other for­mal sys­tem is re­cur­sively enu­mer­able, and if PA is omega-con­sis­tent.

• Some parts of my post were just wrong, they’re ed­ited now. But other parts use the un­spo­ken as­sump­tion that there’s such a thing as “stan­dard in­te­gers” (or, equiv­a­lently, there’s such a thing as “Tur­ing ma­chines”) and the ax­ioms of PA are true state­ments about that thing. That seems to im­ply omega-con­sis­tency, but the whole ar­gu­ment is so in­for­mal that I can’t tell for sure. It could be for­mal­ized some­how, I guess, but that was not the in­tent.

In the words of Liron Shapira, I’m talk­ing about Tur­ing ma­chines as “their own meta-level thing”, so state­ments about their halt­ing or non-halt­ing are to be in­ter­preted as “facts of the mat­ter” out­side any for­mal sys­tem. The “stan­dard in­te­gers” ex­ist in the same limbo. That’s where the hand­wavy rea­son­ing about SSS...S0 comes from.

Yeah I know that’s weird.

• Are you con­fus­ing sound­ness with con­sis­tency? omega-con­sis­tency is much weaker than sound­ness.

Con­sis­tency: a syn­tac­tic claim that it’s im­pos­si­ble to de­rive a con­tra­dic­tion. Doesn’t re­quire a no­tion of truth to be use­ful.

Omega-con­sis­tency: a syn­tac­tic claim that it’s im­pos­si­ble to prove cer­tain state­ments to­gether. Doesn’t need a no­tion of truth, but is mo­ti­vated by the stan­dard model of nat­u­ral num­bers.

Sound­ness: a se­man­tic claim that given a spe­cific no­tion of “true” as ap­plies to a state­ment, e.g. truth in the model N of nat­u­ral num­bers, all the ax­ioms of the the­ory are true. Au­to­mat­i­cally im­plies both con­sis­tency and omega-con­sis­tency. Re­quires a no­tion of the “in­tended model” or a “stan­dard model” for the the­ory in which we con­sider the truth of propo­si­tions. For ex­am­ple, sound­ness is mean­ingless to talk about in the case of ZFC, which doesn’t have an in­tended model.

I think this ar­gu­ment holds as long as the other for­mal sys­tem is re­cur­sively enu­mer­able, and if PA is omega-con­sis­tent.

Look at this sen­tence from the ar­gu­ment:

“If the or­a­cle says yes, you know that the state­ment is true for stan­dard in­te­gers be­cause they’re one of the mod­els of PA, there­fore N is a stan­dard in­te­ger, there­fore T halts.”

If the or­a­cle for a for­mal sys­tem S says “yes” on a given state­ment S that en­codes the propo­si­tion “a Tur­ing ma­chine T will halt on this in­put”, this means that S proves this propo­si­tion. It does not mean that the propo­si­tion is true and T will in fact halt! For that to be true, you need the for­mal sys­tem S to be sound. S could eas­ily be omega-con­sis­tent and not sound, in which case it’ll lie to you (ex­am­ple, as­sum­ing you be­lieve PA to be con­sis­tent: the for­mal sys­tem.

• Sound­ness: a se­man­tic claim that given a spe­cific no­tion of “true” as ap­plies to a state­ment, e.g. truth in the model N of nat­u­ral num­bers, all the ax­ioms of the the­ory are true. Au­to­mat­i­cally im­plies both con­sis­tency and omega-con­sis­tency. Re­quires a no­tion of the “in­tended model” or a “stan­dard model” for the the­ory in which we con­sider the truth of propo­si­tions. For ex­am­ple, sound­ness is mean­ingless to talk about in the case of ZFC, which doesn’t have an in­tended model.

I looked it up, and it seems like what you’re refer­ring to as sound­ness is called “ar­ith­metic sound­ness.” The sound­ness I know doesn’t re­quire a no­tion of stan­dard model. It sim­ply says that any­thing prov­able syn­tac­ti­cally is also true in ev­ery model/​in­ter­pre­ta­tion. This is au­to­mat­i­cally true for any the­ory in first or­der logic. (Note that my ver­sion of sound­ness is the cor­rect analogue of com­plete­ness, which is also true for any FOL the­ory, as Godel showed, less triv­ially.)

“If the or­a­cle says yes, you know that the state­ment is true for stan­dard in­te­gers be­cause they’re one of the mod­els of PA, there­fore N is a stan­dard in­te­ger, there­fore T halts.”

So here, the or­a­cle says some­thing of the form “ex­ists x such that T halts af­ter x steps”. Omega-con­sis­tency guaran­tees that there is some ac­tual stan­dard num­ber N so that “T halts af­ter N steps” is prov­able/​true. The ex­is­tence of a stan­dard model im­plies omega-con­sis­tency, so I might has well have gone with that, but I was just try­ing to be min­i­mal­ist.

Sorry for the mis­com­mu­ni­ca­tion. Are we on the same page now? I do think that say­ing “sound­ness” gen­er­ally refers to the no­tion I said, though.

• I looked it up, and it seems like what you’re refer­ring to as sound­ness is called “ar­ith­metic sound­ness.” The sound­ness I know doesn’t re­quire a no­tion of stan­dard model. It sim­ply says that any­thing prov­able syn­tac­ti­cally is also true in ev­ery model/​in­ter­pre­ta­tion. This is au­to­mat­i­cally true for any the­ory in first or­der logic. (Note that my ver­sion of sound­ness is the cor­rect analogue of com­plete­ness, which is also true for any FOL the­ory, as Godel showed, less triv­ially.)

It’s just a differ­ent mean­ing of the word “sound­ness”. The sound­ness you’re talk­ing about is re­ally a prop­erty of a de­duc­tive sys­tem in first-or­der logic, as you point out. The sound­ness I’m talk­ing about is a prop­erty of a the­ory w.r.t. a par­tic­u­lar no­tion of truth defined for first-or­der for­mu­las (and it’s usu­ally defined by fix­ing a struc­ture and an in­ter­pre­ta­tion, in that struc­ture, of the logic’s con­stant/​func­tion/​re­la­tion sym­bols; in other words, a model). You’re right that some­times, when talk­ing about the model N, it’s referred to as “ar­ith­metic sound­ness”, but the mod­ifier is not at all re­quired. E.g. search for “a the­ory T is sound” on Google as a phrase, with quo­ta­tion marks, to see us­age ex­am­ples. Or search for “sound” in this post: http://​​rjlip­ton.word­press.com/​​2011/​​03/​​30/​​ran­dom-ax­ioms-and-gdel-in­com­plete­ness/​​

Com­pare with the word “com­plete­ness”, which, I’m sure you’re aware, is also no­to­ri­ously am­bigu­ous: in “Godel’s com­plete­ness the­o­rem” and “Godel’s in­com­plete­ness the­o­rems” it refers to two to­tally differ­ent kinds of com­plete­ness. The differ­ence be­tween them is similar, though not iden­ti­cal, to the one be­tween sound­ness as a prop­erty of a first-or­der logic and sound­ness as a prop­erty of a the­ory.

So here, the or­a­cle says some­thing of the form “ex­ists x such that T halts af­ter x steps”. Omega-con­sis­tency guaran­tees that there is some ac­tual stan­dard num­ber N so that “T halts af­ter N steps” is prov­able/​true.

Well, not quite. Why do you think that omega-con­sis­tency guaran­tees that? What is it about omega-con­sis­tency that guaran­tees any­thing to be true? It only speaks of things that are prov­able/​non­prov­able.

Let me try to be a bit more de­tailed. You ac­tu­ally need your the­ory S (the one you have an or­a­cle for, be it PA or some­thing else) to up­hold two sep­a­rate re­quire­ments:

1. When S proves a sen­tence of the form “Ex­ists x such that T halts af­ter x steps”, you need that sen­tence to be true. This sen­tence is a Sigma1 sen­tence (let me know if I need to de­tail that fur­ther).

2. When there is a true sen­tence of the form “this is a run of T that ends af­ter N steps” (which is a Sigma0 sen­tence), you need S to be able to prove it. This is what the origi­nal post means when it says “the or­a­cle would have found a long and bor­ing proof...”—you need this proof to ac­tu­ally ex­ist! If S is too weak, it might not ex­ist.

If you have both con­di­tions, then the ar­gu­ment in the origi­nal post—the one that says an or­a­cle for S can ser­vice as an or­a­cle for the halt­ing prob­lem—goes through. In de­tail: if S proves T halts, by 1. T in fact halts. If S does not prove T halts, S can­not pos­si­bly prove “This is a run of T that ends af­ter N steps” for any par­tic­u­lar N, be­cause if it could, it would also prove “T halts” by straight­for­ward gen­er­al­iza­tion. There­fore by 2. this can­not be true for any par­tic­u­lar N, there­fore T doesn’t halt.

So far, omega-con­sis­tency is not even in the pic­ture. How does it come in? The eas­iest way to en­sure 1. and 2. is sim­ply to re­quire that

(i) S is Sigma1-sound, that is, ev­ery Sigma1 sen­tence it proves must be true. (ii) S is Sigma0-com­plete, that is, ev­ery true Sigma0 sen­tence is prov­able in S.

It turns out that (ii) is a fairly weak re­quire­ment, and ev­ery S that is strong enough to prove some ba­sic state­ments about +, * and < satis­fies it. The ex­act state­ment is that S must be stronger than Robin­son’s the­ory R. And, given (ii), (i) is in fact im­plied by omega-con­sis­tency. By it­self, omega-con­sis­tency of S doesn’t im­ply (i), but com­bined with Sigma0-com­plete­ness of S, it does. And here’s why:

Let P be a Sigma1 sen­tence of the form “There ex­ist x such that R(x)” prov­able in S, where R is Sigma0. Sup­pose P is ac­tu­ally false, and then R(N) is false for ev­ery spe­cific N, then not-R(N) is true for ev­ery spe­cific N, and it is prov­able in S for ev­ery spe­cific N, by Sigma0-com­plete­ness. This di­rectly con­tra­dicts the omega-con­sis­tency of S. There­fore P is true, and S is Sigma1-sound.

To sum up, it is enough to de­mand that S be omega-con­sis­tent if also it is strong enough to en­sure that it is Sigma0-com­plete, and that re­quire­ment works two du­ties: both to trans­late omega-con­sis­tency into Sigma1-sound­ness which is what the ar­gu­ment re­ally needs, and di­rectly for the sec­ond half of the ar­gu­ment it­self.

Phew. Hope I didn’t make any stupid mis­take there. Let me know if any­thing’s un­clear or dis­agree­able to you.

P.S. Note that the ar­gu­ment above de­pends cru­cially on the no­tion of what is “true”, which is defined in the model N of nat­u­ral num­bers. You can­not ap­ply it to some the­ory S which isn’t able to speak of nat­u­ral num­bers at all (in fact, omega-con­sis­tency can­not be defined for such an S) or doesn’t have the ba­sic ma­chin­ery of ar­ith­metic func­tions and re­la­tions (be­cause it’s used to trans­late as­ser­tions about Tur­ing ma­chines into ar­ith­meti­cal state­ments). Thus my origi­nal re­mark that the ar­gu­ment de­pends on sound­ness of S. It was too broad in the sense that if you an­a­lyze the mat­ter closely, you see that only Sigma1-sound­ness and not gen­eral sound­ness is re­quired, as ex­plained above, and that can be satis­fied with omega-con­sis­tency and some mod­est strength. But the se­man­tic re­quire­ments of hav­ing to talk about N and true state­ments doesn’t go away (be­cause you can’t define Sigma0-com­plete­ness with­out that, and you do cru­cially need that for the ar­gu­ment to go through).

• No, you need guaran­tees on the for­mal sys­tem’s com­plex­ity, similar to the ones in Godel’s in­com­plete­ness the­o­rem(s).

Agreed. It’s kind of ob­vi­ous but I should’ve spel­led that out, I guess.

This is stronger than your “has a model con­tain­ing the stan­dard in­te­gers”, and is equiv­a­lent to “has the stan­dard in­te­gers as a model”.

I agree that my ver­sion is wrong, but yours doesn’t sound com­pletely right ei­ther. ZFC doesn’t have the stan­dard in­te­gers as a model, or does it? I thought it also in­cluded other ob­jects...

Note that you’re as­sum­ing here that PA is sound and in par­tic­u­lar con­sis­tent.

Yes.

The halt­ing or­a­cle’s un­com­putabil­ity de­gree is the small­est pos­si­ble un­com­putable de­gree, so no.

Could you give a refer­ence? Wikipe­dia seems to dis­agree but maybe I fail read­ing com­pre­hen­sion:

Emil Post stud­ied the r.e. Tur­ing de­grees and asked whether there is any r.e. de­gree strictly be­tween 0 and 0′. The prob­lem of con­struct­ing such a de­gree (or show­ing that none ex­ist) be­came known as Post’s prob­lem. This prob­lem was solved in­de­pen­dently by Fried­berg and Much­nik in the 1950s, who showed that these in­ter­me­di­ate r.e. de­grees do ex­ist.

• I agree that my ver­sion is wrong, but yours doesn’t sound right ei­ther. ZFC doesn’t have the stan­dard in­te­gers as a model, or does it? I thought it also in­cluded other ob­jects...

My ver­sion is right, but per­haps too re­stricted. The rea­son your ar­gu­ment works for ZFC is be­cause it in­ter­prets PA by prov­ing its ax­ioms as ap­plied to par­tic­u­lar sets in ZFC. So the gen­eral re­quire­ment would be for a sys­tem to be strong enough to prove cer­tain true state­ments about the nat­u­ral num­bers and to dis­prove cer­tain false state­ments.

Could you give a refer­ence?

No, I wrote non­sense—I re­al­ized that and wanted to come back and edit it point­ing out this ex­act link you gave, but you did that be­fore me. I don’t know enough about Post’s prob­lem or the Fried­berg/​Much­nik solu­tions to say whether they can be suit­ably pre­sented as prov­abil­ity classes.

• The rea­son your ar­gu­ment works for ZFC is be­cause it in­ter­prets PA by prov­ing its ax­ioms as ap­plied to par­tic­u­lar sets in ZFC.

Nice! I didn’t re­al­ize that. I guess the eas­iest way is to ask for the same guaran­tees that Gödel’s the­o­rems use, do you agree? For now, changed the post ac­cord­ingly :-)

• This post has noth­ing to do with ra­tio­nal­ity and is likely to scare away read­ers who haven’t the slight­est idea what “Peano ar­ith­metic” refers to. And call­ing your con­clu­sion “ob­vi­ous” sends a rather “ob­vi­ous” mes­sage to a large sub­set of po­ten­tial read­ers.

• (I didn’t down­vote your com­ment.)

I have writ­ten many tech­ni­cal posts, and the next one I’ve got planned will be more difficult than this one. Sev­eral of those posts got pro­moted and I also got some com­ments like this one say­ing my half-baked ideas were a big part of what at­tracted them to LW. That’s prob­a­bly a bit too much flat­tery, but still :-) To be fair, I also got some com­ments similar to yours. Eliezer has also writ­ten many tech­ni­cal posts like the car­toon guide to Löb’s the­o­rem which is more com­plex than most of my posts, in­clud­ing this one.

I’d re­ally like to con­tinue writ­ing about AI-re­lated tech­ni­cal stuff on LW. Would re­mov­ing the word “ob­vi­ous” satisfy your com­plaint?

• I’d re­ally like to con­tinue writ­ing about AI-re­lated tech­ni­cal stuff on LW.

Would re­mov­ing the word “ob­vi­ous” satisfy your com­plaint?

You could go all math­e­mat­i­cian and use ‘triv­ial’. ;)

• I think it would also help if you spel­led out “Peano ar­ith­metic” in the ti­tle in­stead of “PA.” After read­ing the ti­tle, I had no idea what this post would be about.

• When read­ing a tech­ni­cal post, it would be nice to see some­thing like an “as­sumed reader’s back­ground” note be­fore all the gory de­tails. And maybe a non-tech­ni­cal sum­mary for the rest of us.

For ex­am­ple, in your case you could state that the tar­get au­di­ence is (say) a 3rd year math un­der­grad or higher, fa­mil­iar with the con­cepts of <...> and <...>

• Made some ed­its. Though writ­ing a non­tech­ni­cal sum­mary is a lit­tle be­yond my skills right now :-)

• Per­haps you could put some­thing in the ti­tle or first line of the post to sig­nal that it will be (a) only of in­ter­est to peo­ple who en­joy math­e­mat­i­cal philos­o­phy and (b) not in­dica­tive of the kind of writ­ing nor­mally seen here. The fact that similar posts of yours have at­tracted read­ers to LW is, I ac­knowl­edge, ev­i­dence against my pre­vi­ous com­ment.

Also please do omit the term ob­vi­ous from fu­ture ar­ti­cles. It’s in­furi­at­ing (for me at least) to read tech­ni­cal ar­ti­cles and not un­der­stand some­thing the au­thor has la­beled “ob­vi­ous”.

If pos­si­ble you might want to mo­ti­vate why what­ever you have writ­ten pro­vides in­sight into ra­tio­nal­ity. EY, I think, at least even­tu­ally always does this with his writ­ings.

• Per­haps you could put some­thing in the ti­tle or first line of the post to sig­nal that it will be (a) only of in­ter­est to peo­ple who en­joy math­e­mat­i­cal philos­o­phy and (b) not in­dica­tive of the kind of writ­ing nor­mally seen here.

Done, sort of.

Also please do omit the term ob­vi­ous from fu­ture ar­ti­cles.

Okay,

It’s in­furi­at­ing (for me at least) to read tech­ni­cal ar­ti­cles and not un­der­stand some­thing the au­thor has la­beled “ob­vi­ous”.

whuh? Your past com­ments in­di­cate that you’re a col­lege pro­fes­sor and have writ­ten a book on game the­ory! I’m sur­prised… Okay, point taken.

If pos­si­ble you might want to mo­ti­vate why what­ever you have writ­ten pro­vides in­sight into ra­tio­nal­ity.

Most of my tech­ni­cal posts are about the math­e­mat­ics of de­ci­sion the­ory and AI, not hu­man ra­tio­nal­ity. That is also a tra­di­tional LW topic that pre­dates me. In par­tic­u­lar, I’m very in­ter­ested in AIs that try to prove the­o­rems, and this post is the sort of the­o­ret­i­cal re­sult that could be rele­vant to those. Also it’s rele­vant to my next post which will be about de­ci­sion the­ory, if I don’t re­fute that re­sult first :-)

• If I see a bunch of stuff that I’m not fa­mil­iar with and don’t im­me­di­ately want to make the effort to be­come fa­mil­iar with, I just click out of the thread. I think that if things like this com­posed a larger frac­tion of the posts here, then there might be a prob­lem, but that there re­ally isn’t one at the mo­ment.

• (com­ment re­tracted be­cause it sounded dis­mis­sive)