The paper: M.D. Davis & J.T. Schwartz "Metamathematical Extensibility for Theorem Verifiers and Proof-Checkers,'' Computers and Mathematics with Applications, vol.5(1979), pp. 217-230 addresses the problem of retaining certainty when adjoining more powerful proof methods to an existing proof checker. Martin