 The foregoing results are solely concerned with pure logic. Formal theories that axiomatize mathematical structures or serve as formal frameworks for developing substantial chunks of mathematics are based on logic but have additional axioms germane to their purpose. If they are of the latter kind, such as first-order arithmetic or Zermelo-Fraenkel set theory, they will assert the existence of mathematical objects and their properties. What happens when we try to apply the procedure of cut elimination to theories? Axioms are usually detrimental to this procedure. It breaks down because the symmetry of the sequent calculus is lost. In general, one cannot remove cuts from deductions in a theory T when the cut formula is an axiom of T. However, sometimes the axioms of a theory are of bounded syntactic complexity. Then the procedure applies partially in that one can remove all cuts that exceed the complexity of the axioms of T. This gives rise to partial cut elimination. It is a very important tool in proof theory. For example, it can be used to analyze theories with restricted induction (such as fragments of PA; cf. Sieg 1985). It also works very well if the axioms of a theory can be presented as atomic intuitionist sequents (also called Horn clauses), yielding the completeness of Robinson’s resolution method (see Harrison 2009).