Classical Natural Deduction

Gentzen introduced his sequent calculi LK and LJ, as well as his natural deduction systems NK and NJ, in his celebrated “Investigations into Logical Deduction” (1935). As far as classical logic is concerned both the natural deduction calculus NK and the sequent calculus LK run into serious difficulties from the computational viewpoint. In this work we argue that the origin of such computational problems can be traced back to the fact that, contrary to a widespread opinion, neither of these calculi provides an adequate representation of the classical notion of deduction (in particular of the bivalent semantics on which it is based), and propose an alternative approach: a new system of “classical natural deduction” which substantially differs from Gentzen’s one and closely corresponds to classical semantics. We then prove two main results: (i) a normalization theorem for our new classical system and (ii) an exponential speed-up of this system over Gentzen’s ones; normal deductions in our system are uniformly shorter, and often exponentially shorter, than normal (or cut-free) deductions in Gentzen’s systems