Marginalia on sequent claculi. (English) Zbl 0924.03104

Troelstra, A. S.

Stud. Log. 62, No. 2, 291-303 (1999).

In this paper, the relations between natural deductions of D. Prawitz and Gentzen-style deductions are investigated. The latter are also ascribed to S. Jaśkowski [Stud. Log. No. 1, 5-32 (1934; Zbl 0011.09702)]. In particular the correspondence of normal deductions in the N-calculus and cutfree deductions in the G-calculus are examined. Generally speaking, both kinds of systems are all the same. But since Linear Logic directs attention to the details also with respect to the structural rules demanded, the differences are elaborated by several authors in a number of papers [G. Mints, in: P. Odifreddi (ed.), Kreiseliana: about and around Georg Kreisel, 469-492 (1996; Zbl 0897.03053), R. Dyckhoff and L. Pinto, Theor. Comput. Sci. 212, 141-155 (1999; Zbl 0913.68110), H. Schwichtenberg, ibid. 212, 247-260 (1999; Zbl 0913.68135), and L. Pinto and R. Dyckhoff, in: D. Galmiche (ed.), Workshop on proof search in type-theoretic languages, Lindau 1998, Electr. Notes Theor. Comput. Sci. 17, electr. paper No. 8 (1998; Zbl 0917.68198)]. Among other results it turned out that the order of discharging assumptions in N-systems is relevant, and this corresponds to term labeling of G-sequents. Among the different possibilities of discharching assumptions one is exceptional, the so-called complete discharge convention (CDC) by which open assumptions are always discharged at the earliest opportunity. The corresponding G-systems are those without term labeling. In the paper under review these kinds of systems are compared to see whether the derivations of one system can be associated injectively or surjectively to derivations of another system. Also questions of normalizability respectively strong normalization are investigated for different systems of the described kind. The other authors mentioned above did not concentrate their attention to this kind of systems. The methods applied here are similar to those used by others,but still more subtlety is needed. The expression “marginalia” in the title of the paper sounds too modest. It should be called supplement, amendment, clarification or even copestone of the literature on the subject. It is recommended to have the author’s joint monograph with H. Schwichtenberg [Basic proof theory (1996; Zbl 0868.03024)] at hand when reading the paper.

Reviewer: Helmut Pfeiffer (Hannover)

MSC:

03F07	Structure of proofs
03F05	Cut-elimination and normal-form theorems
03B35	Mechanization of proofs and logical operations

Keywords:

complete discharge convention; natural deduction; Gentzen-style deduction; normal deductions; cutfree deductions; structural rules; term labeling; normalization

Citations:

Zbl 0011.09702; Zbl 0897.03053; Zbl 0913.68110; Zbl 0913.68135; Zbl 0917.68198; Zbl 0868.03024