To cut or not to cut...

In a Gentzen-like formulation of a logic, we take as axioms only those consecutions of the form A |- A. For a lot of sensible logics, we can even take A to be atomic. We then postulate a few rules for introducing connectives on both sides of |-. Most of these rules satisfy the subformula property, which is to say that any formula or structure appearing in the numerator (assumption) of the rule is a subformula of something appearing in the denominator (conclusion). Case in point, the contraction rule, one of whose variants is:

X, A, A |- Y
------------
X,A |- Y

In the above, X and Y are structures (multisets of formulae) and A is a formula. It says that if we can conclude Y from X and A and A, then we can conclude it from X and A also (this rule is present in classical logic but not in, say, linear logic).

One rule is a bit conniving and does not obey the subformula property: it is called cut, one version of which says that if you have X|- A and also A |- Y, then you can "cut out" A and conclude X |- Y (this is nothing but the transitivity of deduction).

But this is ok in sensible logics, for in these logics cut is admissable, which is to say that adding it as a rule does not give us anything new. This is quite an impressive result, since the cut rule is basically a rule which says that we can use lemmas. That it is admissable means that we do not need to use them. Actually, it says more than that. Good proofs of its admissability show how to explicitly transform a proof with cuts into one without. Crikey! To see cut elimination in action on a theorem from real analysis, look no further than the following (which also includes an introduction to sequent calculus and proof theory in general):

Making Proofs Without Modus Ponens A. Carbonne and S. Semmes

One very important consequence of cut elimination for a logic is consistency (although sometimes you need to use a bit of transfinite induction...). By eliminating the cut rule, we also ensure that (formal) proofs satisfy the subformula property. So, a proof of a formula (/structure/sequent/whatever) gives a method for constructing it. This leads, in one direction, to the field of logic programming, where one performs a backtrack search for a cut-free proof. See:

A Tutorial on Proof Theoretic Foundations of Logic Programming Paola Bruscoli and Alessio Guglielmi

The other side of the coin is that transforming a proof with cuts into one without cuts can lead to an exponential blowup in the length of the proof: obviously a bad thing.

So, what is a logician to do? One option is to only use a modified form of the cut rule, called an "analytic cut". In this version, we are only allowed to cut on a formula if it is a subformula of something in the conclusion. Ok, so this obviously lets us keep cut and still have the subformula property. So all is well right? Wrong! Surprisingly enough, there is trouble with this even in the case of propositional logic: a system with analytic cut is no better than truth tables. In technical terms, analytic tableaux cannot p-simulate truth tables.

Are Tableaux an Improvement on Truth-Tables? Marcello D'Agostino. Journal of Logic, Language and Information 1: 235 -- 252, 1992.

Although, this is not too surprising, since if a system with analytic cut did not give exponential length proofs of some propositional formulae, then we would have coNP = NP. More on this another time...