Allowing a formal proof system to self improve while avoiding Lobian obstacles.

[Epistemic sta­tus, can’t spot a mis­take, but am not con­fi­dant that there isn’t one, if you find any­thing please say so. Post­ing largely be­cause the com­mu­nity value of a new good idea is larger than any harm that might be caused by a flawed proof. ]

Sup­pose you have an au­to­matic proof checker. Its con­nected to a source of state­ments that are some­times cor­rect proofs, and some­times not. The proof checker wants to re­ject all false proofs, and ac­cept as many of the true proofs as pos­si­ble. It also wants to be able to up­date its own proof frame­work.

Define to be a set of state­ments in a par­tic­u­lar for­mal­ism, say those that are gram­mat­i­cally well defined in PA. Let be any se­quence from some alpha­bet of sym­bols. Let

and be the set of pro­grams that have the prop­erty that

In other words, is the set of all pro­grams that never prove false state­ments. We should never leave or need to talk about any pro­gram not in it.

For write to mean . Ie proves

A sim­ple setup would con­sist of a start­ing pro­gram and a rule that says,

If then you can add to your list of trusted provers. If proves the sound­ness of , then you can ac­cept any state­ment when given a proof of it in .

The lo­bian ob­sta­cle is that must be strictly weaker than , in that can prove any state­ment that can, but can prove the sound­ness of and can’t prove its own sound­ness. This means that each trusted prover has to be strictly weaker than the one that gen­er­ated it. You could start with PA+3^^^3 and say that a few weak­en­ings aren’t a prob­lem, but that isn’t an el­e­gant solu­tion.

Note: You can’t get around this prob­lem us­ing cy­cles. Suppose

This would imply

So any cy­cle could be shrunk by 1, and in­duc­tively, shrunk to a self trust­ing sys­tem.

I pro­pose in­stead that you use the rule.

If then ac­cept any fu­ture proofs that are ac­cepted by , and give all rights given to , in­clud­ing tak­ing to mean that is ac­cepted, and so on re­cur­sively. If is sound, then so any­thing that is proven by can be proven by . If isn’t sound, it can prove any­thing any­way.

Note that if is a straight­for­ward iso­mor­phism of then they are eas­ily proven equiv­a­lent. How­ever, if says “run Tur­ing ma­chine for steps, if it doesn’t halt, check if is a valid proof of , if does halt, re­turn ” then it could be equiv­a­lent to from a sec­ond or­der logic per­spec­tive, but can’t prove that never halts.

Still, this rule al­lows us to prove any­thing prov­able in and only things prov­able in , while also al­low­ing the user to add short­hands and se­man­tic sugar.

Note that the “proof” could just be the num­ber of pro­ces­sor cy­cles you want to run a proof search for be­fore giv­ing up. In fact, this frame­work lets you swap and mix be­tween hand proved re­sults, and au­to­mat­i­cally proved re­sults (with search time cut off) as you see fit.

This for­mal­ism al­lows a any sys­tem con­tain­ing a proof checker to au­to­mat­i­cally up­grade it­self to a ver­sion that has the same Godelian equiv­alence class, but is more suited to the hard­ware available.