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.

• As you say, this isn’t a proof, but it wouldn’t be too sur­pris­ing if this were con­sis­tent. There is some such that has a proof of length by a re­sult of Pavel Pudlák (On the length of proofs of fini­tis­tic con­sis­tency state­ments in first or­der the­o­ries). Here I’m mak­ing the de­pen­dence on ex­plicit, but not the de­pen­dence on . I haven’t looked at it closely, but the proof strat­egy in The­o­rems 5.4 and 5.5 sug­gests that will not de­pend on , as long as we only ask for the weaker prop­erty that will only be prov­able in length for sen­tences of length at most .

• I found an im­proved ver­sion by Pavel, that gives a way to con­struct a proof of from that has a length of . The im­proved ver­sion is here.

There are re­stric­tions to this re­sult, though. One is that the C-rule must ap­ply to the logic. This is just the abil­ity to go from to in­stan­ti­at­ing a such that . Pretty much all rea­son­able the­o­rem provers have this.

The sec­ond re­stric­tion is that the the­ory must be finitely ax­iom­a­ti­z­able. No ax­iom schemas al­lowed. Again, this isn’t much of a re­stric­tion in prac­tice, be­cause NBG set the­ory, which proves the con­sis­tency of ZFC, is finitely ax­iom­a­ti­z­able.

The proof strat­egy is ba­si­cally as fol­lows. It’s shown that the short­est proof of a state­ment with quan­tifier depth n must have a length of , if the max­i­mum quan­tifier depth in the proof is or greater.

This can be flipped around to con­clude that if there’s a length-n proof of , the max­i­mum quan­tifier depth in the proof can be at most .

The sec­ond part of the proof in­volves con­struct­ing a bounded-quan­tifier ver­sion of a truth pred­i­cate. By Tarski’s un­defin­abil­ity of truth, a full truth pred­i­cate can­not be con­structed, but it’s pos­si­ble to ex­hibit a for­mula for which it’s prov­able that ( is the for­mula lay­ing out Tarski’s con­di­tions for some­thing to be a truth pred­i­cate). Also, if quan­tifier depth of , there’s a proof of ( is the sen­tence with its free vari­ables sub­sti­tuted for the el­e­ments enu­mer­ated in the list ) Also, there’s a proof that is pre­served un­der in­fer­ence rules and log­i­cal ax­ioms, as long as ev­ery­thing stays be­low a quan­tifier depth of .

All these proofs can be done in lines. One fac­tor of comes from the for­mula ab­bre­vi­ated as get­ting longer at a lin­ear rate, and the other fac­tor comes from hav­ing to prove for each seper­ately as an in­gre­di­ent for the next proof.

Com­bin­ing the two parts, the bound on the quan­tifier depth and the bound on how long it takes to prove stuff about the truth pred­i­cate, make it take steps to prove all the rele­vant the­o­rems about a suffi­ciently large bounded quan­tifier depth truth pred­i­cate, and then you can just go “the state­ment that we are claiming to have been proved must have ap­ply to it, and we’ve proved this is equiv­a­lent to the state­ment it­self”

As a fur­ther bonus, a sin­gle -length proof can es­tab­lish the con­sis­tency of the the­ory it­self for all -length proofs.

It seems like a use­ful pro­ject to de­velop a pro­gram that will au­to­mat­i­cally write a proof of this form, to as­sess whether ab­stract un­pack­ing of bounded proofs is us­able in prac­tice, but it will re­quire dig­ging into a bunch of finicky de­tails of ex­actly how to en­code a math the­ory in­side it­self.

• Caught a flaw with this pro­posal in the cur­rently stated form, though it is prob­a­bly patch­able.

When un­pack­ing a proof, at some point the sen­tence will be reached as a con­clu­sion, which is a false state­ment.

• I mi­s­un­der­stood your pro­posal, but you don’t need to do this work to get what you want. You can just take each sen­tence as an ax­iom, but de­clare that this ax­iom takes sym­bols to in­voke. This could be done by chang­ing the no­tion of length of a proof, or by tak­ing ax­ioms and with very long.