Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre, 1995.
The plan of the paper is as follows. We examine ways of providing user extensibility for theorem provers, which naturally places the LCF and reflective approaches in opposition. A detailed introduction to LCF is provided, emphasizing ways in which it can be made efficient. Next, we present a short introduction to metatheory and its usefulness, and, starting from Gödel's proofs and Feferman's transfinite progressions of theories, look at logical `reflection principles'. We show how to introduce computational `reflection principles' which do not extend the power of the logic, but may make deductions in it more efficient, and speculate about their practical usefulness. Applications or proposed applications of computational reflection in theorem proving are surveyed, following which we draw some conclusions. In an appendix, we attempt to clarify a couple of other notions of `reflection' often encountered in the literature.
The paper questions the too-easy acceptance of reflection principles as a practical necessity. However I hope it also serves as an adequate introduction to the concepts involved in reflection and a survey of relevant work. To this end, a rather extensive bibliography is provided.
@TECHREPORT{harrison-reflection, author = "John Harrison", title = "Metatheory and Reflection in Theorem Proving: A Survey and Critique", institution = "SRI Cambridge", address = "Millers Yard, Cambridge, UK", year = 1995, type = "Technical Report", number = "CRC-053", note = "Available on the Web as {\verb+http://www.cl.cam.ac.uk/~jrh13/papers/reflect.dvi.gz+}"}