________if self.prove(p1,”forall s:(exists b2: p2(s,b2))=> (exists b1: p2(s,b1))”, b)
____________self.ps.append(p2)
prover=Prover()
prover.upgrade(PA, nPA, proof)
Where PA is a specific peano arithmatic proof checker. nPA is another proof checker. and ‘proof’ is a proof that anything nPA can prove, PA can prove too.
PA+1 can already provide this workflow: Given that nPA proves s and that PA proves all that nPA does, we can get that PA can prove s, and then use the +1 to prove s. And then nnPA can still be handled by PA+1.
Both blanks are the identity function.
Here is some psudo code
class Prover:
____def new(self):
________self.ps=[PA]
____def prove(self, p, s, b):
________assert p in self.ps
________return p(s,b)
____def upgrade(self, p1, p2, b):
________if self.prove(p1,”forall s:(exists b2: p2(s,b2))=> (exists b1: p2(s,b1))”, b)
____________self.ps.append(p2)
prover=Prover()
prover.upgrade(PA, nPA, proof)
Where PA is a specific peano arithmatic proof checker. nPA is another proof checker. and ‘proof’ is a proof that anything nPA can prove, PA can prove too.
PA+1 can already provide this workflow: Given that nPA proves s and that PA proves all that nPA does, we can get that PA can prove s, and then use the +1 to prove s. And then nnPA can still be handled by PA+1.