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

Dyckhoff, Roy

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

Keywords:

contraction rule; intuitionistic propositional calculus; modifications of natural deduction

Citations:

Zbl 0047.252

References:

[1]	Journal of Logic and Computation
[2]	DOI: 10.1007/3-540-52335-9_55 · 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 · doi:10.1002/malq.19870330509
[8]	Trudy Matematicheskogo Instituta imeni V. A. Steklova 52 pp 193– (1958)
[9]	DOI: 10.1145/359138.359142 · Zbl 0431.68016 · doi:10.1145/359138.359142
[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 · doi:10.1016/0743-1066(87)90020-3
[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 · 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)