The “applications of cut elimination” in the title of this chapter may perhaps be described more appropriately as “applications of cutfree systems”, since the applications are obtained by analyzing the structure of cutfree proofs; and in order to prove that the various cutfree systems are adequate for our standard logics all we need to know is that these systems are closed under Cut (that is to say, Cut is a an admissible rule). Nevertheless there are good reasons to be interested in the process of cut elimination, as opposed to semantical proofs of closure under Cut. True, the usual semantical proofs establish not only closure under Cut, but also completeness for the semantics considered. On the other hand, the proof of cut elimination for G3c is at least as efficient as the semantical proof (although G3cp permits a very fast semantical proof of closure under Cut), and in the case of logics with a more complicated semantics (such as intuitionistic logic, and the modal logic S4 in chapter 9) often more efficient. For linear logic in section 9.3, so far no semantical proof of closure under Cut has been published. Other reasons for being interested in the process of cut elimination will be found in certain results in sections 5.1 and 6.9, which describe bounds on the increase in size of deductions under cut elimination and normalization respectively.