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.