On Explicit Reflection in Theorem Proving and Formal Verification

We show that the stability requirement for a verication system yields the necessity of some sort of a reflection mechanism. However, the traditional reflection rule based on the Göodel implicit provability predicate leads to a “reflection tower” of theories which cannot be formally veried. We found natural lower and upper bounds on a metatheory capable of establishing stability of a given verication system. The paper also introduces an explicit reflection mechanism which can be veri ed internally. This circumvents the reflection tower and provides a theoretical justication for the verication process. On the practical side, the paper gives specic recommendations concerning verication of inference rules and building a veriable reflection mechanism for a theorem proving system.