A SEQUENT SYSTEM WITHOUT IMPROPER DERIVATIONS

In the natural deduction system for classical propositional logic given by G. Gentzen, there are some inference rules with assumptions discharged by the rule. D. Prawitz calls such inference rules improper, and others proper. Improper inference rules are more complicated and are often harder to understand than the proper ones. In the present paper, we distinguish between proper and improper derivations by using sequent systems. Specifically, we introduce a sequent system proves(Sc) for classical propositional logic with only structural rules, and prove that proves(Sc) does not allow improper derivations in general. For instance, the sequent double right arrow p -> q cannot be derived from the sequent p double right arrow q in proves(Sc). In order to prove the failure of improper derivations, we modify the usual notion of truth valuation, and using the modified valuation, we prove the completeness of proves(Sc). We also consider whether an improper derivation can be described generally by using proves(Sc).