The Basic Ideas

We used the Naive Type Theory of section 2 to present the Nuprl type theory, e. g. term is an inductive type. Nuprl is an approximation to the naive theory. A natural question to ask is whether we could use Nuprl to ``define itself.'' We know from Gödel's incompleteness theorem and Tarski's truth theorem that we cannot define Nuprl completely inside itself. But how close can we come?

It is easy to see that the basic syntax and the evaluation semantics can be completely defined. We already know similar results from experience defining Lisp evaluation in Lisp.

It is also easy to imagine that we can define the notion of a proof internally and the concept of a tactic. This again is clear from the ability to define these concepts nicely in ML as actually done in LCF, HOL, and Nuprl.

What is new and exciting here is this:

• We can define terms, evaluations, and proof naturally by just transcribing the informal definition. The formal definition clarifies the logic.
• The internal definition allows us to write theorem-proving tactics as Nuprl programs and prove properties of them.
• The internal account of proof enables us to define a new proof rule, the reflection rule, which is the basis for solving the design problem posed by decision procedures (see the introduction).

In this section we will examine the first two points and treat the last one in the next section. Most of this is conceptually clear, but the details are critical. I refer you to other writings for most of those. There are however a few subtle points to notice.

In reflecting the class term we will define an internal inductive type, Term. We have shown elsewhere that Term represents term. One tricky point here is to avoid the following infinite regress. For each operator name, like int or spread, we add a new operator name that denotes it, say int and spread. (We actually use opid{int:opname} and opid{spread:opname}.) Now we have new operators, int and spread, and we need names for them; we might try int1 and spread1 or something. But then we would need int2 and spread2, etc. How to stop the regress? First notice this; all reflected operators have the form opid{o:opname}, and this is the generic form of operators. So they get reflected like any other operator, essentially op{i:family} is represented as $a \ pair$, <reflected operator, reflection of the list of pairs of index and index family name>.

Another subtle point arises with reflecting evaluation. We do this by adding new operators Evals_To and Val. But we need to define evaluation fragments for them which are self-referential. This is explained in Aitken's thesis.

One of the most subtle points comes up in the definition of $proo\!f$.The reflected concept uses PreProof and Proof. We need to specify how tactics build proofs, and this must be part of the definition of $proo\!f$. But a tactic is a function that builds elements of Proof. So the definition of the informal concept of $proo\!f$ requires that we anticipate the definition of Proof and refer to it. This requires a delicate fixed point construction that appears in [6].

Dealing with these points correctly and formally takes a lot of care and relies on many details. But using the mechanism is quite natural. It is much like replacing ML or SML in a tactic-oriented prover with Nuprl's programming language.