Normality, non-contamination and logical depth in classical natural deduction (Q2307304)

For classical logic, with its duality between conjunction and disjunction mediated by negation, as also between the universal and existential quantifiers, one would hope to have corresponding symmetries in whatever recursive apparatus is used to generate the logic. Such symmetry is not only aesthetically pleasing, but also offers prospects of more elegant formulation and proof, and more efficient techniques of automated theorem-proving. Symmetry in the generative process comes easily for truth-trees, but for Frege-style axiomatizations it appears to be impossible, while for natural deduction and single-conclusion consecution systems it faces difficulties. In the latter context, Gentzen obtained symmetries in the rules by allowing multi-conclusion consecutions. In the former context, however, that move is unattractive as it deviates far from the way human reasoning takes place. For this reason, accounts of natural deduction have hitherto tolerated imperfect symmetry in the rules employed, specifically for contrarian connectives (those that come out false when all components are true; every functionally complete set of primitive connectives must contain at least one of them, usually chosen to be negation or falsum). Since 1978 there has been a marginal tradition in the philosophical literature of formulating systems of natural deduction that use signed formulae, that is, formulae labelled (say, with 1 or 0) for assertion and rejection. This has generally been done from an inferentialist perspective, according to which propositional connectives should, as a matter of principle, be defined in terms of the intelim rules that they satisfy rather than in terms of their truth conditions. The paper under review takes up the idea of using signed formulae in natural deduction, but without the inferentialist agenda, and gives it a sustained formal elaboration in the context of propositional logic with an eye on computational benefits. Unlike both the usual unsigned systems as well as previous signed ones, the natural deduction system presented in this paper has the feature that only one of its rules involves discharge of an assumption. That rule, which may be seen as structural rather than intelim, tells us that if we have successfully proven \(v: B \) from each of \(1: A\) and \(0: A\) considered separately (where \(v\) can be \(0\) or \(1\)) then we are entitled to conclude \(v: B\) from whatever other signed hypotheses were used in those two proofs. This parsimony of discharge allows the authors to establish normal form theorems that are unavailable for natural deduction systems in the style of Gentzen and Prawitz. Final sections give an alternative presentation in terms of truth-trees, and show that a notion of the depth of a derivation in normal form provides a hierarchy of computationally tractable approximations to classical propositional logic.