cut elimination

The cut rule is admissible in LJ.

The proof is by induction. The actual induction hypothesis is a little tricky, though: it is not as simple as saying that the number of cuts decreases at each step. Rather, we want to show that any derivation of the form

can be transformed into a derivation of in which the cuts themselves are in some sense “smaller” than the one we started with. To that end, we give a few definitions.

• The degree of a cut is the number of connectives in the cut formula (e.g., in the above cut).
• The rank of a cut is the sum of its left and right ranks, where the left rank is the length of the shortest path from the cut up to the point where the cut formula was introduced on the left, and the right rank is defined similarly.
• A cut is simpler than if the degree of is less than , or if their degrees are the same and the rank of is less than . In other words, the “simpler-than” relation is the lexicographic ordering by (degree, rank).

The induction hypothesis, then, is that any derivation rooted by its most complex cut can be transformed into a cut-free derivation of the same sequent.

Now we split into cases based on the rank of the root cut.

In this case, the derivation on either the left or the right is not rooted by a step that introduces . For example, the derivation on the left may be rooted by a step that introduces on the right.

But then we could have performed the cut before introducing .

Observe that the cut in this new derivation is simpler than the cut in the original derivation, since it is one step closer to the introduction of on the left, hence it has lower rank.

This is the general pattern: we split into cases based on which rule does not introduce , and we show how to transpose that rule with a final cut, resulting in a derivation with a simpler cut.