I’ve spotted a mistake, I think: the relationship inside the first prover should be an if and only if relationship. This is because if p2 says everything is a theorem, then p2[s]⟹p1[s] trivially holds. Thus, the condition to give p2 “proof privileges” should be p1[p2[s]⟺p1[s]]. There might still be some problems from the modal logic, I’ll check when I have some more time.
I can’t believe that I was the first one to spot this. The post also has very few upvotes. Did nobody that knows this stuff see this and spot the mistake immediately? Was the post dismissed to start with? (in my opinion unfairly, but perhaps not).
I’ve spotted a mistake, I think: the relationship inside the first prover should be an if and only if relationship. This is because if p2 says everything is a theorem, then p2[s]⟹p1[s] trivially holds. Thus, the condition to give p2 “proof privileges” should be p1[p2[s]⟺p1[s]]. There might still be some problems from the modal logic, I’ll check when I have some more time.
I can’t believe that I was the first one to spot this. The post also has very few upvotes. Did nobody that knows this stuff see this and spot the mistake immediately? Was the post dismissed to start with? (in my opinion unfairly, but perhaps not).