Contraction-elimination for implicational logics

Annals of Pure and Applied Logic 84 (1):17-39 (1997)
  Copy   BIBTEX

Abstract

We establish the “contraction-elimination theorem” which means that if a sequent Γ A is provable in the implicational fragment of the Gentzen's sequent calculus LK and if it satisfies a certain condition on the number of the occurrences of propositional variables, then it is provable without the right contraction rule. By this theorem, we get the following.1. If an implicational formula A is a theorem of classical logic and is not a theorem of intuitionistic logic, then there is a propositional variable which occurs at least once positively and at least twice negatively in A → a) → a).2. If an implicational formula A is a theorem of intuitionistic logic and is not a theorem of BCK-logic, then there is a propositional variable which occurs at least twice positively and at least once negatively in A → a → b).We prove the contraction-elimination theorem by a fully syntactical method, which has some analogy with Gentzen's cut-elimination.

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 102,283

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.
LEt ® , LR °[^( ~ )], LK and cutfree proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.
A minimal classical sequent calculus free of structural rules.Dominic Hughes - 2010 - Annals of Pure and Applied Logic 161 (10):1244-1253.
Embedding classical in minimal implicational logic.Hajime Ishihara & Helmut Schwichtenberg - 2016 - Mathematical Logic Quarterly 62 (1-2):94-101.
New sequent calculi for Visser's Formal Propositional Logic.Katsumasa Ishii - 2003 - Mathematical Logic Quarterly 49 (5):525.
Rule-Elimination Theorems.Sayantan Roy - 2024 - Logica Universalis 18 (3):355-393.

Analytics

Added to PP
2014-01-16

Downloads
31 (#745,925)

6 months
9 (#493,407)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Investigations into a left-structural right-substructural sequent calculus.Lloyd Humberstone - 2007 - Journal of Logic, Language and Information 16 (2):141-171.
Rule-Elimination Theorems.Sayantan Roy - 2024 - Logica Universalis 18 (3):355-393.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.

Add more citations

References found in this work

Logics without the contraction rule.Hiroakira Ono & Yuichi Komori - 1985 - Journal of Symbolic Logic 50 (1):169-201.
Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt.S. Jaśkowski - 1963 - Mathematical Logic Quarterly 9 (12‐15):219-228.
Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt.S. Jaśkowski - 1963 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 9 (12-15):219-228.

Add more references