 Gentzen (1934) presented his natural deduction systems, \(\mathcal{NJ}\) and \(\mathcal{NK}\), for intuitionistic and classical logic (respectively), but he was not satisfied with \(\mathcal{NK}\): he didn’t see how to extend the normalization theorem (discussed below in  §5)  from \(\mathcal{NJ}\) to \(\mathcal{NK}\). He therefore introduced another pair of systems, \(\mathcal{LJ}\) and \(\mathcal{LK}\) (\(\mathcal{L}\) for logistisch), for the two logics, for which he was able to give a uniform proof of a closely related metatheorem. As with his presentation of natural deduction, a proof in one of his -systems is a tree, but whereas the nodes of the tree in an \(\mathcal{N}\)-system proof are occupied by single formulas, the nodes in an \(\mathcal{L}\)-system proof are occupied by sequents, where a sequent consists of a pair of (possibly null!) lists of formulas, separated by a special symbol,  \(\vdash\).[18]  (As a result, systems similar to Gentzen’s \(\mathcal{L}\)-systems are usually called sequent calculi.) The intuitive meaning of a sequent is that if all the formulas of the list to the left of the \(\vdash\) (the antecedent formulas) are true, then at least one of the formulas in the right-hand list (the succedent formulas) is true, or (to use a word hinting at the relation to natural deduction) the assumption that all the antecedent formulas are true justifies the conclusion that at least one of the succedent formulas is true. In line with standard usage of all and at least one of in modern mathematics, this is interpreted as covering the cases of sequents with null lists: if there are no antecedent formulas in a sequent, it is interpreted as meaning that at least one of the succedent formulas is true, if there are no succedent formulas the sequent is interpreted as meaning that at least one of the antecedent formulas is false, and if both lists are null—so the sequent is just a \(\vdash\) standing by itself—it is interpreted as expressing a necessary falsehood.