Reflection Rule

The material in the section is from the article The Semantics of Reflected Proof [6]. We want to take full advantage of the fact that we can reason about tactics. In particular, if we demonstrate that a tactic t generates a proof of some sequent s, we would like to be able to cite this demonstration rather than run the tactic.

Our general plan for doing this is to add a rule that essentially asserts that if

$\exists p{\sf :Proof}. root(p)= rep(H\vdash G)$

then $H \vdash G$ is true, where rep(s) is the representation of a sequent s. The rule might be

$$Re\!f\!l H \vdash G$$

But the rule is not sound. From Löb's theorem on proof predicates [7], we suspect that this is not valid. Aitken discusses the situation in his thesis [3]. The idea is this. Given

$$% latex2html id marker 2322 \fbox {$\exists p:{\sf Proof}. root(p)=rep(H\vdash G) \vert R$}$$

to conclude $H \vdash G$ we need a new rule, say $Re\!fl$, but this is not part of $proo\!f$. If we add it, we get a new notion of $proo\!f_0$,say $proo\!f_1$. If we allow reflection over these, we get $proo\!f_2$, etc. Can we close this off? Almost! We can close it syntactically, but what does it mean? Notice that the extractor which is needed to build a canonical proof from depends on this meaning.

Reflected Pre-Proofs

To get syntactic closure under reflection, we want a rule like $Re\!fl$ above. Where Proof reps proof with Proof in the rule itself. To accomplish this, we first parameterize proof to $proo\!f(Q)$ where Q is the term used in the rule. This forces us to consider Proof(Q).

Syntactic Closure of Proof Definition

Define $proo\!f(Q)$ to allow the rule

$$H \vdash G \vdash\exists p:\begin{array}[t] {c} Q \uparrow \end{array} .root(p)=rep(H\vdash G)$$

In the [6] we show how to take a syntactic fixed point through Q.

Here is another approach.

Add to the library a definition

PF == Term representing proof(PF)

This is straightforward from PreProof since PF is just a term.

The actual rule uses an indexing mechanism to keep track of how deeply the use of reflection is nested. The function level(p) gives the maximum of the level numbers occurring in reflection rules of p. Using this we incorporate the rule in the definition of $proo\!f$ as follows.

               $proo\!f=\{p:pre\!-\!proo\!f \vert is\_a\_proo\!f(p)\}$

$$(<s, j, [p_1, \ldots, p_n]\gt)$$