In place of the customary conception in terms of syntax and semantics, Gentzen provided two alternative conceptualizations of the idea of completeness. The first is in terms of the previous chapter’s relational definition scheme which allows the idiosyncratic notion of individual pairs of rules being complete in isolation of the global system of inference. The second is in terms of the sequent calculus. Specifically, Gentzen’s cut elimination result is properly understood as a completeness theorem. To see this, we read the result against the background of Gentzen’s 1932 analysis of logical consequence. Our formulation of the sequent calculi LK and LI are modifications of Gentzen’s original presentation due to Ketonen. Their significance will be explained in the next chapter. The cut elimination procedure is in the direct style due to Sam Buss. In light of the earlier analysis of logical consequence, cut elimination is a verification that the operational rules suffice to derive all logical consequences of provable sequents. Those operational rules are thus seen to be “complete” in the sense that nothing that follows from logically true expressions is underivable with the operational rules. Gentzen demonstrated that those rules capture the full logical sense of the connectives they govern. Several immediate applications of cut elimination include the disjunction and existence properties for intuitionistic logic and the distinction between admissible and derivable rules. The distinction between structural and operational reasoning explicit in the sequent calculus leads to the distinction between additive and multiplicative rules and propositional linear logic. With these tools we complete the analysis begun in the previous chapter of the calculi NM and NR.