A Loophole for Self-Applicative Soundness

See com­ments. This is a re­dis­cov­ery of a re­sult from the 1980′s that al­low con­clud­ing from via a -length proof, and even the state­ment that the the­ory has no dis­proof of length or less has a sin­gle -length proof. This is not vuln­er­a­ble to Critch’s Bounded Para­met­ric Lob proof, and was cre­ated by look­ing for ways to make it fail.


This re­sult is just an idea de­vel­oped very re­cently, and I’d put ~2:1 odds on it hav­ing a fatal flaw, but it looks ex­tremely promis­ing if it works out. EDIT: It works. None of the proof the­ory checks have been done yet, but it does causes both Lob’s the­o­rem, and Critch’s Bounded Para­met­ric Lob re­sult to fail.

So, to be­gin with, if a the­ory thinks it is sound, then it is in­con­sis­tent. Proof by Lob’s the­o­rem.

Well that didn’t work.

What if we give the the­ory a sound­ness schema over any proof which is of bounded length? Maybe the “there ex­ists a proof” in the stan­dard prov­abil­ity pred­i­cate is caus­ing prob­lems.

Well then Critch’s Bounded Para­met­ric Lob comes in to ruin our day. The en­tire proof will be re­pro­duced be­low.

Let , , and be such that , , and , asymp­tot­i­cally.

As a spe­cific ex­am­ple, this can be done by , , and .

If it takes a con­stant num­ber of steps to de­rive a spe­cific proof re­gard­less of , the num­ber on it will be sup­pressed for read­abil­ity. Also, tech­ni­cally, the origi­nal proof has in­stead of , but this change doesn’t al­ter much.

(Para­met­ric Di­ag­o­nal Lemma) (Bounded Ne­ces­si­ta­tion) (Quan­tifier Distri­bu­tion) (Im­pli­ca­tion Distri­bu­tion) (Im­pli­ca­tion Distri­bu­tion) Now spe­cial­ize to a=g(k), b=h(k). Also, for suffi­ciently large k above . (Bounded In­ner Ne­ces­si­ta­tion) Now, Spe­cial­iz­ing to a=g(k), we get Now, since af­ter some time , Pick a spe­cific value of k, , which is suffi­ciently large. By the sound­ness schema, . The length of this proof isn’t con­stant, be­cause might be re­ally big, so then it’d take about char­ac­ters to write down the sin­gle ap­pli­ca­tion of the sound­ness schema. (By the defi­ni­tion of ) even­tu­ally. Since was pre­vi­ously se­lected to be suffi­ciently big, Now we no longer care about ’s size, be­cause has been fixed, so

How­ever, not all is lost. If you look care­fully at this, you see that the in­tro­duc­tion of the sound­ness scheme lead to a minor proof blowup. Sure, it’s not enough of a blowup to sur­pass , so the proof of still goes through, but this seems like it might be ex­ploitable....

So then the next step is to make sure that can only ever be proved by a proof of steps or more. The agent can con­clude its own sound­ness for bounded proofs, but it may take a while. I’m pretty sure this is doable by hav­ing an ax­iom schema of the form for each in­di­vi­d­ual and seper­ately, but I’m not en­tirely sure of that. EDIT: Doesn’t work, see com­ments.

Re­gard­less, as­sume that any proof of via iter­ated sound­ness ax­ioms will always take or more steps. EDIT: You don’t need to as­sume this, there’s an ex­plicit proof of that state­ment.

Then, if we go through the proof again, some­thing in­ter­est­ing hap­pens. In­stead of mak­ing its way to the length of the proof, we get (or more). in or­der to get an ear­lier step of the proof to go through, but then the re­sult­ing proof of takes at least steps to work, so that proof can­not be used with the defi­ni­tion of to con­clude .

I’d sus­pect there’s some more sub­tle ar­gu­ment that can con­clude in­con­sis­tency, but break­ing the proof of Lob’s the­o­rem is promis­ing.

What’s the use of this, though, if it doesn’t shorten proofs?

Well, there’s a lot of -length proofs, but the “royal road” of ab­stractly es­tab­lish­ing sound­ness or con­sis­tency would al­low con­clud­ing the sen­tence di­rectly with­out hav­ing to em­bark on an ex­haus­tive search for the origi­nal proof.

If you spent a while prov­ing some­thing, and then wrote down the re­sult in your note­book, and for­got about it, then, upon ob­serv­ing the note­book page, you can con­clude and, since you can bound how good you are at math, you can es­tab­lish an up­per bound on the length of the proof, . This pro­vides a way to es­tab­lish with­out hav­ing to re­prove the thing from scratch, by just think­ing for a while about “Do I trust my own bounded proofs? Yes I do.”

This solves the Note­book Prob­lem in Vingean Reflec­tion.