(note: some readers may find the LaTeX easier to read on LessWrong)

The purpose of this post isn’t to convince you that cut elimination is important. See, for example, the nLab article. Rather, the purpose of this post is to (semi-formally) prove cut elimination in a way that I at least find easy to understand. I have consulted existing sources (such as these lecture notes), but have found it hard to fill in all the details, given the sparsity of the usual presentations. I’ll build on the previous post (on Gödel’s Completeness Theorem) and show cut elimination in the first-order sequent calculus defined in that post. Recall that the cut rule states:

We can think of as the assumptions, as the conclusion, and P as a lemma. Intuitively, this states that, if it’s possible to prove the conclusion or the lemma from the assumptions, and it’s possible to prove the conclusion from the assumptions and the lemma, then it’s possible to prove the conclusions from the assumptions. Cut-elimination is, therefore, the automated elimination of lemmas in a sequent proof. (As stated in the previous post, this presentation of the cut rule is somewhat nonstandard, but it can be shown equivalent to the standard form using weakening and contraction.)

Throughout the post, I will use the notion of the depth of a sentence, and the cut rank of a proof. The depth of a sentence is the depth of nesting of compound sentences; in particular, the depth of an atomic sentence is 0, the depth of a negation is one plus the depth of its inner sentence, the depth of a conjunction is one plus the maximum depth of the inner sentences, and the depth of a universal is one plus the depth of the inner sentence. The cut rank of a proof is a mapping , where is the number of times a cut is performed on a sentence of depth i; note that this is zero almost everywhere. We compare cut ranks lexicographically, with later entries counting more than previous ones.

Constant substitution

As a preliminary, we will show that constants can be substituted with terms in proofs without changing the proof structure (in particular, cut rank stays the same). As notation, if P is a term, sentence, or set of sentences, let P[t/c] indicate replacing the constant c with the term t anywhere in P. Suppose we have a proof of the judgment . We wish to show that there is a proof of with the same cut rank as the original proof.

Call the height of a sequent proof the longest path from top to bottom, counting by number of rule applications. I will show by induction that, for all natural , constant substitution holds for a proof whose height is n.

In the base case, the only rule is the assumption rule. Then and both contain some sentence P. So and both contain . So the assumption rule also shows .

In the inductive case, we consider different cases for the bottom-most rule. Suppose the bottom-most rule in the proof is the weakening rule. Then the proof looks like:

By the inductive assumption, we have a proof of . Then we straightforwardly show using weakening.

Suppose the bottom-most rule in the proof is the cut rule. Then the proof looks like:

By the inductive assumption, we have proofs of and . Now we cut on to get the result.

Suppose the bottom-most rule in the proof is the left negation rule. Then the proof looks like:

By the inductive assumption, we have a proof of . We apply the left negation rule on to get a proof of .

Most of the remaining rules are similar, so I will skip them. I will consider the non-trivial case of the right universal rule. In this case, the proof looks like this:

where d is a constant not appearing in , , or . Let d’ be a constant not appearing in , , , or t, and not equal to c. First we apply the inductive assumption to get a proof of or equivalently . Now we apply the inductive assumption again to get a proof of . Since d’ does not appear in t and is unequal to c, we can swap the substitution order to get a proof of . At this point, since d’ does not appear in , or , we can apply the right universal rule to get a proof of .

Eliminating weakening

It will be easier to show cut elimination in a logic without weakening. So it is more convenient to eliminate weakening before eliminating cut. This has the added benefit of eliminating weakening in addition to cut. Recall the weakening rule:

I will show by induction that, for all natural , weakening can be eliminated for a proof whose height is n+1, and whose last step is weakening.

Let’s consider the base case. If the proof has height 2, and the bottom-most rule is weakening, then the top-most rule must be the assumption rule. In this case, the assumption rule could have been applied to the pre-weakened judgment.

Let’s consider the inductive case. Suppose weakening can be eliminated form any proof whose height is at most n and whose last step is weakening. We now consider showing weakening can be eliminated from a proof whose height is n+1 and whose last step is weakening.

We do this by cases on the second-to-last rule. We have no need to handle the assumption rule, as that would make the height 2 (the base case).

Suppose the second-to-last rule is weakening. Then the two weakenings can be combined into one weakening. This reduces the height of the proof by one, so weakening can be eliminated inductively.

Suppose the second-to-last rule is cut. Then the proof looks like this:

Call the proof of the top-left judgment X and the proof of the top-right judgment Y. Then X and Y have height at most n-1. Now we consider re-writing the proof to put weakening higher:

The left proof of has height at most n, and the right proof of has height at most n. So weakening can be eliminated from both sides (using the inductive assumption).

Suppose the second-to-last rule is left negation. Then the proof looks like this:

As before, we re-write to move weakening higher:

And observe that the size of the proof with weakening at the bottom is now at most n, so weakening can be eliminated from it inductively.

I will skip most of the rules, as they are similar. The only nontrivial case is the right universal rule. The proof would look like this:

where c does not appear in , , or . Now we find a constant d which does not appear in , , , , or . We move weakening up:

We can convert the original proof of to one of equal height and cut rank proving using constant substitution. Now weakening can be eliminated from this proof using the inductive assumption.

Note that throughout this process, the structure of cuts has not been changed; the same cuts are applied to the same sentences. As such, the cut rank is the same.

As a corollary of weakening elimination, we can transform proofs so that, if a rule application is of the form

then and . This is because the non-weakening rules, such as the negation rules, have “implicit contraction” where there is no requirement to eliminate any sentence, and weakening elimination means these extra sentences in judgments are not a problem (as they could be eliminated with weakening anyway, and then the weakenings could be eliminated). I will call this transformation “redundant contraction”. Note also that this does not change the cut rank of the proof.

Making the assumption rule only apply to atoms

Recall that an atomic sentence is a predicate applied to some terms. The assumption rule may apply to arbitrary sentences. We would like to transform sequent proofs to ones that only apply the assumption rule to atomic sentences.

To do this, we will consider proving judgments of the form without using the assumption rule except on atomic sentences. We will do this by induction on the structure of P.

Now we consider what form P could take. If P is atomic, we simply apply the assumption rule. Suppose P is . Then we prove the judgment as follows:

with the top judgment proven by the inductive assumption.

Suppose P is . Then we prove the judgment as follows:

with the top judgments proven by the inductive assumption.

Suppose P is . Then we prove the judgment as follows:

with the top judgment proven by the inductive assumption, and where c is a constant not appearing in , , or .

The inversion lemma

The rules for compound sentences are, for the most part, invertible, in that if the bottom judgment is provable with no cuts, so is the top judgment. I will show invertibility for these rules, assuming no weakening and that the assumption rule only applies to atoms.

In general, these proofs will work by applying redundant contraction to the proof of the bottom judgment and observing that the proof steps work for a modified version of the judgments, except for certain rule applications. Note that we intentionally omit the left universal rule, as it is not invertible like the others. It will instead be handled manually later.

A property that will be true throughout is that, if the original proof has no cuts, neither does the inverted proof.

Left negation

Consider the left negation rule:

Suppose the bottom judgment is provable. Apply redundant contraction to the proof. We will do induction over the proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed on the left and P is added to the right. Every step in the proof will convert automatically except for instances of the left negation rule applied to . Those cases originally look like

and in the conversion we are trying to show . We can prove this by inductively converting the proof of .

Overall, the converted proof proves . And if the original proof has no cuts, neither does the converted proof.

Right negation

Consider the right negation rule:

Suppose the bottom judgment is provable. Symmetric with the left negation case, we convert the proof to a proof of . And if the original proof has no cuts, neither does the converted proof.

Left conjunction

Consider the left conjunction rule:

Suppose the bottom judgment is provable. Apply redundant contraction to the proof. We will do induction over the proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from and P and Q are added to the left. Every step in the proof will convert automatically except for when left conjunction is applied to . Those cases look like:

and in the conversion we are trying to show . We can prove this by inductively converting the proof of .

Overall, the converted proof proves , as desired. And if the original proof has no cuts, neither does the converted proof.

Right conjunction

Consider the right conjunction rule:

We will consider proofs of and separately.

First consider . Suppose the bottom judgment is provable. Apply redundant contraction to the proof. We will do induction over this proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from and P is added to the right side. Each step of the proof will convert automatically except for applications of the right conjunction rule to . Those cases look like:

and in the conversion we are trying to show . We prove this by inductively converting the proof of .

Overall, the converted proof proves , as desired.

Now consider . This is symmetric with the previous case, yielding a converted proof.

In both cases, if the original proof has no cuts, neither does the converted proof.

Right universal

Consider the right universal rule:

where c does not appear in . Suppose the bottom judgment is provable. Apply redundant contraction to this proof. We will do induction over the proof to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from and is added to the right, where c’ is a constant appearing nowhere in the proof. Every step will convert automatically except for applications of the right universal rule to . Those cases look like:

where d is a constant not appearing in , and in the conversion we are trying to show . We inductively convert the proof of to get a proof of . Then we apply constant substitution to this proof, replacing d with c’, to get a proof of .

Overall, the converted proof proves . Now we apply constant substitution again to get a proof of . And if the original proof has no cuts, neither does the converted proof.

Showing cut elimination

We are now ready to eliminate cut from an arbitrary proof. Assume the proof has no weakening and that the assumption rule is only used on atoms (we have already shown how to convert a proof to one of this form). An instance of the cut rule looks like this:

We consider different forms P could take in turn. Each time, we eliminate one instance of cut from the proof (a “cut reduction”), in a way that reduces the cut rank of the overall proof. We only eliminate cuts where the proofs of the premises do not themselves have any cuts; if the proof has at least one cut, a cut exists whose premise proofs don’t have any cuts, so this is not an obstacle to the algorithm.

Atomic sentences

Suppose P is atomic. Assume the proofs of and are cut-free. Apply redundant contraction to the first proof. Each leaf of this proof now uses the assumption rule to prove where and . Now we consider eliminating P from the right hand side of every judgment in this proof (so the converted “proof” now “proves” ); every non-assumption rule can still be applied, but some of the leaves will now fail to be proven with the assumption rule. In those cases, when the judgment of the leaf is , we know , as the elimination of P from the right caused a failure of the assumption rule. In those cases, it is sufficient to show , by weakening elimination (since and ). But we already have a cut-free proof of this, the original cut-free proof of . By repairing the leaves, we now have a cut-free proof of .

Negations

Suppose . Then the premises of the cut rule imply we have proofs of and . Assume these proofs are cut-free. Using invertibility, we can get cut-free proofs of and . Then apply cut on Q:

This reduces the cut rank because cut is applied to a simpler sentence.

Conjunctions

Suppose . Then the premises of the cut rule imply we have proofs of and . Assume these proofs are cut-free. Using invertibility we can get cut-free proofs of , , and . Then apply cut twice:

This reduces the cut rank because cut is applied to simpler sentences. Note that we can convert the proof of to one of using weakening elimination.

Universals

Suppose . Then the premises of the cut rule imply that we have proofs of and . Assume both these proofs are cut-free, and apply redundant contraction to the second. Using invertibility on the first proof, we can get a cut-free proof of where c is a constant not appearing in .

We will do induction over the proof of to show that each sub-proof of a judgment can be converted to one of a converted form of the judgment, where is removed from the left, and where we only introduce cuts on sentences of the form . Each step of the proof will convert automatically except for applications of the left universal rule, of the form

where and . In the converted proof, we are instead trying to show . We can prove this by inductively converting the proof of to one of , and then applying cut:

We can show by applying constant substitution to our cut-free proof of to get a cut-free proof of , and then applying weakening elimination.

While we introduce more cuts into the proof, these all apply to a sentences of the form , which have lower depth than the original universal , so this still decreases the cut rank.

Summary

To summarize, we first modify our proof to have no weakening and to only apply the assumption rule to atoms. Then we find an instance of cut where the proofs of the premises are cut-free. Depending on what sentence is cut, we find a way to remove this cut, only replacing it with cuts on sentences with lower depth. Overall, this succeeds in reducing the cut rank of the proof. Since the set of cut ranks (assumed to be zero almost everywhere) are well-ordered, this iterative process will eventually eliminate all cuts from the proof.

Conclusion

Cut elimination is a fundamental theorem of formal logic. I have shown cut elimination for the first-order sequent calculus described in the post on Gödel’s completeness theorem, which is a simplified form of system LK. Compared to explanations of cut elimination I have found in the literature, this is a relatively complete proof relative to its simplicity. It helps me at least understand how cut elimination can proceed in an algorithmic, syntactic manner on the proof tree. While applications of cut elimination are beyond the scope of this post, understanding the actual proof might help to understand how these applications work.