  Notice that the rules of weakening and contraction are available only for formulas marked with the exponential \(\bang\) on the left or \(\quest\) on the right of the sequent.  The \(\quest\)R and \(\bang\)L rules are often called “dereliction” rules. The \(\quest\)L and \(\bang\)R rules are often called “promotion” rules and are the same as the possibility and necessity rules found in Kripke’s S4 modal logic. The usual proviso for the \(\forall\)-right and \(\exists\)-left introduction rules are assumed: in particular, the variable \(y\) must not be free in the formulas of the lower sequent of those inference rules. Quantification here is assumed to be first-order: higher-order versions of linear logic can be written along standard lines.