Complete justifications

If there is enough information in a justification to generate the subgoals, then the tree of justifications and the top goal can generate the whole proof. Moreover, the tree of justifications can be combined into a single ``algebraic expression'' describing the whole proof. Indeed, the proof tree stripped of the sequents is just a parse tree for this expression.

If we present the justifications in the right way we can read the rules annotated by them as an attribute grammarattribute grammar (c.f. [101,100,56]) for generating an expression describing the proof called a proof expressionproof expression. Consider the case of the $\Rightarrow\!\!L$ and $\&\!L$ rules again. Suppose we let pand g denote proof expressions for the subgoals, then

$\bar{x}: \bar{H}, f:(P \Rightarrow Q), \bar{J}\, \vdash G\ \mbox{by}\ \Rightarrow\!\!L\ \ \mbox{on} \ f$

       -- $\ \ \ \vdash P \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \mbox{by}\ p(\bar{x})$

       --, $y:Q \vdash \ G\ \ \ \ \ \ \ \ \ \ \mbox{by}\ g(\bar{x}, y)$

If we think of the proof expressions $p(\bar{x})$ and $g(\bar{x}, y)$ as being synthesized up from the subtrees, then the complete proof information for the goal sequent is

$\Rightarrow\!\!L \ \ \mbox{on}\ f\ \mbox{from}\ p(\bar{x})\ \mbox{and from}\ g(\bar{x}, y)\ \mbox{with new}\ y$

Organizing this into a more compact expression and recognizing that y is a new bound variable, a suggestive expression is

$\Rightarrow\!\!L (f; p(\bar{x}); y\:. g(\bar{x}, y))$

Here we use the ``dot notation'' $y. g(\bar{x}, y)$ to indicate that y is a new bound label in the proof expression $g(\bar{x}, y)$. The dot notation is used with quantifiers as in $\forall x\!:\!A.\: F$ to separate the binding operator $\forall x\!:\!A$ from the formula F. Likewise, in the lambda notation,lambda notation $\lambda(x.b)$, the dot is used to indicate the beginning of the scope of the binding of x.

In the case of $\&\!L$, the rule with proof expressions looks like

	$\bar{x}\!:\!\bar{H}, z\!:\!P\&Q \vdash G\ \mbox{by}\ \&L\ \mbox{in}\ z\ \mbox{with new}\ u,v$
	$\bar{x}\!:\!\bar{H}, u\!:\!P, v\!:\!Q \vdash G\ \mbox{by}\ g(\bar{x}, u, v)$

A compact notation is

$$\&\!L (z; u, v.\: g(\bar{x}, u, v))$$

Here u, v are new labels which again behave like bound variables in the proof expression.

The justification for $P \vee \neg P$ will be the term magic(P)magic rule. This is the only justification term that requires the formula as a subterm.

With this basic typed predicate logic as a basis, we will now proceed to add a number of specific types, namely natural numbers, lists, functions, sets over a type, and so-called quotient types. Each of these shows an aspect of typed logic. Note, in these rules we are presupposing that P, Q, and the formulas in $\bar{H}$ are well-formed according to the definition of a formula and that the type expressions are also well-formed in accordance with the typing rules. As we introduce more types, it will be necessary to incorporate typing judgments as subgoals. The Nuprl logic of [28] relies on such subgoals from the beginning so that the caveat just stated for this table of rules is unnecessary there.