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{\Gamma},A\left[p\right],A\left[p\right]\top \text{\Delta}}{\text{\Gamma},A\left[p\right]\top \text{\Delta}}LC& \frac{\text{\Gamma}\top A\left[p\right],A\left[p\right],\text{\Delta}}{\text{\Gamma}\top A\left[p\right],\text{\Delta}}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 ...

Start Free Trial

No credit card required