Handbook of Automated Reasoning

4.1 Free variable systems

The free variable sequent calculus adopts the structural LK rules in figure 1 with the proviso that the rules now operate on labelled formulae. Contraction hence looks like this:

$\begin{array}{cc}\frac{\text{Γ},A\left[p\right],A\left[p\right]\top \text{Δ}}{\text{Γ},A\left[p\right]\top \text{Δ}}LC& \frac{\text{Γ}\top A\left[p\right],A\left[p\right],\text{Δ}}{\text{Γ}\top A\left[p\right],\text{Δ}}RC\end{array}$

The logical rules are given in figure 6. Recall that the symbol p ranges over labels, which means that it can be either ε or a prefix term or a sequence of prefix terms. The inferences of type R⊃ and R¬ are parameter–labelled. Instances of L⊃ and L-¬ are variable–labelled. If r is one of the parameter–labelled ...