Justifications

justification The rule names and parameters to them make up a very important part of the proof called the justificationjustification of the inference step. We can think of the justification as an operator on sequents which decomposes the goal sequent into a subgoal sequents. This format for the justification reveals that role graphically.

$\bar{x}: \bar{H} \vdash G$	by $r(\bar{x}; \bar{t})$
$1. \bar{H}_1 \vdash G_1$
$\vdots$
$k. \bar{H}_k \vdash G_k$

For example

$\bar{H} \vdash (P \vee Q)\ \mbox{by} \vee\!\!R l$
$1. \bar{H} \vdash P$

The justification takes the variables and labels of $\bar{x}$ plus some parameters $\bar{t}$ and generates the k subgoals $\bar{H}_i \vdash G_i$. The hypothesis rule generates no subgoals and so terminates a branch of the proof tree. Such rules are thus found at the leaves.

By putting into the justifications still more information, we can reveal all the links between a goal and its subgoals. To illustrate this information, consider the $\Rightarrow$L rule and the $\&$L rule.

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

      $1.\ \ \bar{H}, f:(P\Rightarrow Q), \bar{J}\ \ \ \ \ \ \ \vdash P$

      $2.\ \ \bar{H}, f: (P \Rightarrow Q), \bar{J}, y\!:\!Q \vdash G$

       $\bar{H}, pq\!:\!P\: \&\: Q \vdash G\ \mbox{by}\ \&\!L$

$\ \ \bar{H}, pq\!:\!P\: \&\: Q, p\!:\!P, q\!:\!Q, \bar{J} \vdash G$   

If the $\Rightarrow$R justification provided the label y, then all the information for generating the subgoal would be present. If the &L rule provided the labels p, q then the data is present for generating its subgoals as well. So we will add this information to form a complete justificationcomplete justification.

Notice that these labels behave like the variable names x_i in the sense that we can systematically rename them without changing the meaning of a sequent or a justification. They act like bound variables in the sequent. The phrase new u, v in a justification allows us to explicitly name these bound variables.