Explicit Reflection in Theorem Proving and Formal Verification

摘要

The basic properties of soundness, extensibility, and stability required from a verification system V taken in full yield the necessity of having a reflection rule in every such V. However, the reflection rule based on the Godel provability predicate (implicit provability predicate) leads to a 'reflection tower' of theories which cannot be formally verified. The paper introduces an explicit reflection mechanism which can be verified inside the system. This circumvents the reflection tower and provides a strict justification for the verification process. On the practical side, the paper gives specific recommendations concerning the verification of inference rules and building a verifiable reflection mechanism for a theorem proving system.