[FOM] mechanical theorem metachecking

[Martin Davis]

On October 6 Hendrik wrote:
 >Let's say we have a formal system F.
 >
 >In F, we prove that the execution of some computer program P(x) will,
 >if it terminates, always generate a formula that is provable in F.
 >
 >Since execution of P on a machine may be more efficient than
 >checking the proof it generates, we're tempted to include a rule
 >that allows us to use such proved programs as proof rules in F.
 >
 >Under what circumstances is it possible to do this safely?

This question is discussed and a suitable meta-theorem proved in the paper:
Martin Davis & J.T. Schwartz, ``Metamathematical Extensibility for Theorem
Verifiers and Proof-Checkers,''  Computers and Mathematics with
Applications, vol.5(1979), pp. 217-230.

Martin


                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com