# 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.

• I’ve spot­ted a mis­take, I think: the re­la­tion­ship in­side the first prover should be an if and only if re­la­tion­ship. This is be­cause if says ev­ery­thing is a the­o­rem, then triv­ially holds. Thus, the con­di­tion to give “proof priv­ileges” should be . There might still be some prob­lems from the modal logic, I’ll check when I have some more time.

I can’t be­lieve that I was the first one to spot this. The post also has very few up­votes. Did no­body that knows this stuff see this and spot the mis­take im­me­di­ately? Was the post dis­missed to start with? (in my opinion un­fairly, but per­haps not).

• Let f map each prover p1 to one adding (at least) the rule of in­fer­ence of “If _(p1) proves that _(p1) proves all that p2 does, then f(p1) proves all that p2 does.”

It is un­clear which blanks are filled with f and which with the iden­tity func­tion to match your pro­posal. The last f must be there be­cause we can only have the new prover prove ad­di­tional things. If all blanks are filled with f, f(p1) is in­con­sis­tent by Löb’s the­o­rem and tak­ing p2 to be in­con­sis­tent.

• Both blanks are the iden­tity func­tion.

Here is some psudo code

class Prover:

____def new(self):

________self.ps=[PA]

____def prove(self, p, s, b):

________as­sert p in self.ps

________re­turn p(s,b)