Rules

Proof rules are organized in the usual format of the single-conclusion sequent calculus. They appear in a table shortly. We explain now some entries of this table. There are two rules for each logical operator (connective or quantifier). The right rule for an operator tells how to decompose a conclusion formula built with that operator, and the left rule for an operator tells how to decompose such a formula when it is on the left, that is when it is a hypothesis. There are also trivial rules for the constants $\top$and $\bot$ and a rule for hypotheses. So the rules fit this pattern and are named as shown.

Left Right

&	&L	&R
$\vee$	$\vee$L	$\vee$Rl   $\vee$Rr
$\Rightarrow$	$\Rightarrow$L	$\Rightarrow$R
$\forall$	$\forall$L	$\forall$R
$\exists$	$\exists$L	$\exists$R
$\top$	-	$\top$R
$\bot$	$\bot$L	-

$x_1:H_1, \ldots, x_n: H_n \vdash H_i\ \mbox{by}\ hyp\; x_i$

$1 \leq i \leq n$

The $\vee$R rule splits into two, $\vee$Rl and $\vee$Rr. To prove $\bar{H} \vdash P \vee Q$ we can prove $\bar{H} \vdash P$ or we can prove $\bar{H} \vdash Q$. The first rule is $\vee$Rl because we try to prove the left disjunct. We pronounce these somewhat awkwardly as ``or right left'' and ``or right right.''

The other rules all have obvious pronunciations, e.g. ``and left'' for &L, ``and right'' for &R, etc. Some of them have ancient names, such as ex falso libet for ``false left'' (meaning ``anything follows from false''). In Nuprl we use any for $\bot$L. Sometimes $\vee$L is called ``cases'', and instead of ``by $\vee$L l'' we might say ``by cases on l'' for l a label. For $\forall$L on l with a term t we might say ``instantiating lwith t.''

The rule $\Rightarrow\!\!L$ is similar to the famous modus ponensmodus ponens rule usually written as

$$\frac{A\ \ A \Rightarrow B}{B}.$$

In top down form it would be

$A, A \Rightarrow B \vdash B$	by $\Rightarrow\!\!L$
$A, B \vdash B$
$A \vdash A$

Some of the rules such as $\forall$L and $\exists$R require parameters. For example, to decompose $\forall x: T. P(x)$ as a hypothesis, we need a term $t \in T$. So the rule is $\forall$L on t. For $\exists x\!:\!T.\:P(x)$ as a goal, to decompose it, we also need a term $t \in T$; the decomposition generates the subgoal P(t).