Metamathematical extensibility for theorem verifiers and proof-checkers

AbstractInformal mathematical reasoning has a strong metamathematical component, which is used to expand the rules of proof once theorems which (informally) justify such expansion have been proved. For use of mechanised proof verifier systems to remain comfortable over a wide range of applications, they will have to include corresponding mechanisms. This paper formalizes these mechanisms, and also shows how verifier systems can be expanded by the progressive compilation of additional internal routines but without loss of logical soundness