
handle: 11392/1190920
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.
Natural Deduction; Classical semantics; Computational Complexity; Normalization
Natural Deduction; Classical semantics; Computational Complexity; Normalization
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
