We show that the stability requirement for a verification system yields the necessity of some sort of a reflection mechanism. However, the traditional reflection rule based on the Godel implicit provability predicate leads to a "reflection tower" of theories which cannot be formally verified. We found natural lower and upper bounds on a metatheory capable of establishing stability of a given verification system. The paper also introduces an explicit reflection mechanism which can be verified internally. This circumvents the reflection tower and provides a the-oretical justification for the verification process On the practical side, the paper gives specific recommendations concerning verification of inference rules and building a verifiable reflection mechanism for a theorem proving system.
展开▼
