In this chapter, we give a method of adding axioms to sequent calculus, in the form of nonlogical rules of inference. When formulated in a suitable way, cut elimination will not be lost by such addition. By the conversion of axioms into rules, it becomes possible to prove properties of systems by induction on the height of derivations.

The method of extension by nonlogical rules works uniformly for systems

based on classical logic. For constructive systems, there will be some special forms

of axioms, notably (P ⊃ Q) ⊃ R, that cannot be treated through cut-free rules.

In the conversion of axiom systems into systems with nonlogical rules, the multisuccedent calculi G3im and G3c are most useful. All structural rules will be admissible in extensions of these calculi, which has profound consequences for the structure of derivations. The first application is a cut-free system of predicate logic with equality. In earlier systems, cut was reduced to cuts on atomic formulas in instances of the equality axioms, but by the method of this chapter, there will be no cuts anywhere. Other applications of the structural proof analysis of mathematical theories include elementary theories of equality and apartness, order and lattices, and elementary geometry.

FROM AXIOMS TO RULES

When classical logic is used, all free-variable axioms (purely universal axioms) can be turned into rules of inference that permit cut elimination. The constructive case is more complicated, and we shall deal with it first.