John Harrison.
Technical Report CRC-053,
SRI International Cambridge Computer Science Research
Centre, 1995.

## Abstract:

One way to ensure correctness of the inference performed by computer theorem
provers is to force all proofs to be done step by step in a simple, more or
less traditional, deductive system. Using techniques pioneered in Edinburgh
LCF, this can be made palatable. However, some believe such an approach will
never be efficient enough for large, complex proofs. One alternative, commonly
called *reflection*, is to analyze proofs using a second layer of logic, a
*metalogic*, and so justify abbreviating or simplifying proofs, making the
kinds of shortcuts humans often do or appealing to specialized decision
algorithms. In this paper we contrast the fully-expansive LCF approach with the
use of reflection. We put forward arguments to suggest that the inadequacy of
the LCF approach has not been adequately demonstrated, and neither has the
practical utility of reflection (notwithstanding its undoubted intellectual
interest). The LCF system with which we are most concerned is the HOL proof
assistant.
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.

## Bibtex entry:

@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+}"}