PRL Seminars 1998-99
On the Reflection Mechanism in Nuprl
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.