Let f map each prover p1 to one adding (at least) the rule of inference of “If _(p1) proves that _(p1) proves all that p2 does, then f(p1) proves all that p2 does.”
It is unclear which blanks are filled with f and which with the identity function to match your proposal. The last f must be there because we can only have the new prover prove additional things. If all blanks are filled with f, f(p1) is inconsistent by Löb’s theorem and taking p2 to be inconsistent.
________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.
Let f map each prover p1 to one adding (at least) the rule of inference of “If _(p1) proves that _(p1) proves all that p2 does, then f(p1) proves all that p2 does.”
It is unclear which blanks are filled with f and which with the identity function to match your proposal. The last f must be there because we can only have the new prover prove additional things. If all blanks are filled with f, f(p1) is inconsistent by Löb’s theorem and taking p2 to be inconsistent.
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.