Proof normal forms

Normal forms for logical formulae are a simple, yet powerful tool. For instance, it is not hard to show that every propositional formula is equivalent to one which is in conjunctive normal form (CNF), that is a conjunction of disjunctions. This equivalence makes building software for satisfiability testing more streamlined, since one can consider only CNF formulae.

Similarly, one can study normal forms for proofs in sequent systems. For instance, one may assume without any loss of generality that a given proof in classical logic is cut free. This is all well and good, but it still does not give us a firm grip on how the proof behaves.

Considerations like this led Gentzen to his Sharpened Haupsatz or Midsequent Theorem. This theorem states that a proof in predicate logic may be rearranged so that all propositional inferences precede all quantifier inferences. The sequent resulting from the last propositional inference is known as the midsequent.

The midsequent theorem is a rather intuitive result. There is a more general phenomenon at play here, first expounded by Kleene:

Two Papers on the Predicate Calculus. S.C. Kleene. Memoirs of the American mathematical Society 10 (1952).

The first of the two papers concerns permutability of inferences in sequent calculi for classical and intuitionistic logic respectively. From the onset, Kleene works with a cut-free system. Hence, the whole paper may be seen as an exercise in finding out how much we can sharpen the cut elimination theorem. Kleene's first approach is to number each logical and nonlogical symbol appearing in the proof. This is sensible from an algorithmic point of view, as it allows one to trace where each symbol in the end sequent came from. By doing so, we can say slightly more. In particular, it turns out that for each logical symbol in the end sequent, there is only one possible type of inference that could have created it. That is, we can immediately point to a logical symbol in the end sequent and say whether it was introduced by the left or right introduction rule for that symbol.

Kleene's main result is a sort of generalised sharpened Haupsatz. In particular, look at the logical inferences that occur in a given proof of a sequent S. Now, partition this collection into C1, C2,...,Ck however you like, though satisfying a couple of natural conditions. Then, the proof of S can be rearranged so that on each branch no occurence of an inference in class j appears above an occurence of an inference in class i for i < j.

As a special case, we get the midsequent theorem. Quite easily in fact. Start by partitioning the inferences into two classes, the first of which contains all propositional inferences and the second of which all the quantifier inferences. Now, every predicate formula is equivalent to one in prenex normal form, that is, one which looks like Q1Q2...Qn(f) where each Qi is a quantifier and f is quantifier free (i.e. propositional). So, we may assume that the formula is prenex, from whence it is easy to verify the conditions of Kleene's theorem (Of course, by using prenex formulae, it is quite easy to prove the midsequent theorem without appealing to Kleene).