Prawitz proves what he calls the normal deduction theorem for natural deduction, in minimal, intuitionistic, and classical flavors. Gentzen proved cut elimination (or Hauptsatz, as he called it) for his sequent calculus, in all three flavors as well. The two theorems do the same things. They guarantee that deductions have a certain nice form and nice properties, including the subformula property. The two theorems end up being equivalent in a sense. (I’m not sure how to prove their equivalence though). We do know that if A is deducible from \Gamma in natural deduction, then there is a sequent calculus deduction of it, and conversely. The proof of this provides a way of taking a proof in natural deduction or the sequent calculus and getting a proof of the other. There are two kinds of natural deduction systems that could be used here though. One is Prawitz’s natural deduction which treats each node as a formula. The other is the one we used in the class i took which treats each node as a sequent with open hypotheses made explicit to the left of the arrow. (This isn’t a sequent calculus though, since the sequent calculus only has intro rules.) The proof I’ve seen shows how to take a proof in natural deduction in the second sense to a sequent calculus proof, and vice versa. This somewhat foreshadows Hjortland’s point.

The sequent calculus has structural rules (weakening, e.g.). Natural deduction (in Prawitz’s sense) does not. It seems like we lose explicit information by doing proofs in natural deduction rather than sequent calculus. As Hjortland points out however, if we look carefully, they are still there. Prawitz defines a discharge function which takes care of which hypotheses are discharged where. The structural rules are realized in natural deduction by what sort of discharge functions are allowed. This is somewhat to be expected since we know there is a correspondence between natural deduction and sequent calculus derivations. To take this a step further, it seems like taking Hjortland’s point seriously, there should be a proof that constructively transforms ND proofs (in Prawitz’s sense) into sequent calculus proofs and vice versa that keeps the use of structural rules explicit.

Advertisements