PRL Seminars 1998-99

Abstract

By the Goedel incompleteness theorem and the Loeb Theorem, some important properties of the reflection in Nuprl cannot be formally verified inside Nuprl itself. The traditional provability model based on the predicate Provable(F) also fails to justify the process of upgrading Nuprl by the tactics formally verified in Nurpl.

We suggest a new version of the Nuprl reflection rule which uses the explicit proof predicate Proof(t,F) meaning "t is a proof of F". The new reflection rule admits a formal verification inside Nurpl which allows to circumvent the restrictions imposed on the provability predicate by the Goedel and Loeb theorems. The use of the explicit provability as the verification model also allows us to establish that extensions of a theory by formally verified tactics are equivalent to the original theory. This provides an adequate justification of the verification + extension process in Nuprl and similar systems.