Contraction-free sequent calculi for intuitionistic logic.(English)Zbl 0761.03004

J. Symb. Log. 57, No. 3, 795-807 (1992); correction ibid. 83, No. 4, 1680-1682 (2018).
As the author points out, the present article may be regarded in part as a restatement of relatively old work by N. N. Vorob’ev [Dokl. Akad. Nauk SSSR, N. Ser. 85, 689-692 (1952; Zbl 0047.252)]. It provides familiar reduction of the contraction rule for the intuitionistic propositional calculus to its instances combined with the rule for implications in the antecedent:
$$B,A,\Gamma\Rightarrow G/A\supset B,A,\Gamma\Rightarrow G$$ for atomic $$A$$;
$$C\supset(D\supset B)$$, $$\Gamma\Rightarrow G/(C\& D)\supset B$$, $$\Gamma\Rightarrow G$$;
$$C\supset B$$, $$D\supset B$$, $$\Gamma\Rightarrow G/(C\lor D)\supset B$$, $$\Gamma\Rightarrow G$$;
$$D\supset B$$, $$\Gamma\Rightarrow C\supset D\quad B,\Gamma\Rightarrow G/(C\supset D)\supset B$$, $$\Gamma\Rightarrow G$$.
Similar modifications of natural deduction are also presented.
Reviewer: G.Mints (Stanford)

MSC:

 03B20 Subsystems of classical logic (including intuitionistic logic) 03F05 Cut-elimination and normal-form theorems

Zbl 0047.252
Full Text:

References:

 [1] Journal of Logic and Computation [2] DOI: 10.1007/3-540-52335-9_55 [3] Computerised Logic Teaching Bulletin 2 pp 51– (1989) [4] Elements of intuitionism (1977) · Zbl 0358.02032 [5] Mathematical intuitionism–introduction to proof theory 67 (1988) · Zbl 0634.03054 [6] Automated deduction in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics (1990) · Zbl 0782.03003 [7] DOI: 10.1002/malq.19870330509 · Zbl 0612.03010 [8] Trudy Matematicheskogo Instituta imeni V. A. Steklova 52 pp 193– (1958) [9] DOI: 10.1145/359138.359142 · Zbl 0431.68016 [10] Doklady Akademii Nauk SSSR 85 pp 689– (1952) [11] Polish Academy of Sciences, Institute of Philosophy and Sociology, Bulletin of the Section of Logic 6 pp 2– (1977) [12] DOI: 10.1016/0743-1066(87)90020-3 · Zbl 0608.68006 [13] Some applications of Gentzen’s proof theory in automated deduction, Extensions of logic programming workshop, 1989 475 pp 101– (1991) [14] Computational logic (1991) [15] Computational interpretations of linear logic · Zbl 0791.03003 [16] Introduction to metamathematics (1964) [17] Tableau and sequent calculus method in minimal logic theorem proving (1990) [18] Natural deduction (1965) [19] A Prolog program for intuitionistic logic (1988) [20] Sixth annual IEEE symposium on Logic in Computer Science: proceedings, Amsterdam, 1991 pp 32– (1991) [21] Proofs and types (1989) · Zbl 0671.68002 [22] The collected papers of Gerhard Gentzen (1969) [23] DOI: 10.1007/3-540-54487-9_58 [24] Journal of Logic and Computation [25] Algorithmic aspects of intuitionistic propositional logic I & II (1987) [26] First-order logic and automated theorem proving (1990) · Zbl 0692.68002 [27] Sixth annual IEEE symposium on Logic in Computer Science: proceedings, Amsterdam, 1991 pp 51– (1991) [28] Two papers on the predicate calculus pp 1– (1951) [29] Journal of Automated Reasoning 4 pp 191– (1988) [30] Proof methods for modal and intuitionistic logics (1983) · Zbl 0523.03013 [31] On an interpretation of second order quantification in first-order intuitionistic propositional logic 57 pp 33– (1992) · Zbl 0763.03009 [32] Logics without the contraction rule 50 pp 169– (1985) · Zbl 0583.03018 [33] Proof theory in the USSR 1925-1969 56 pp 385– (1991) [34] Extensions of logic programming workshop, 1989 475 pp 157– (1991)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.