 The main practical problem with using this as a presentation of natural deduction is the tedium of writing and rewriting all the formulas which occur in the antecedents of multiple sequents. It was apparently first noticed in the elementary text, Suppes 1957, that there was an easy way to abbreviate and refer to these formulas: first, by identifying each sequent with a numeral (if there are currently \(n\) sequents in the proof up to this point, then the next sequent will be numbered \(n+1\)). And secondly by associating a label with that numeral used in a proof. The label for a premise of an argument is the same as its numeral; the label for an assumption (or “supposition”) is also the same as its numeral; and otherwise (when a new sequent is generated by appeal to previous sequents) there are two cases, depending on whether the rule is a “direct” rule or a “supposition-ending” rule. In the former case, as exemplified by \(\land\)-Introduction and \(\rightarrow\)-Elimination, the new sequent’s label is the set containing the labels of both formulas that are used in the rule. In the latter case, as exemplified by \(\rightarrow\)-Introduction, the new labels are the label-set of the numeral of the \(\rightarrow\)’s consequent minus the label of the \(\rightarrow\)’s  antecedent.[20]