Preservation of structural properties in intuitionistic extensions of an inference relation

Bulletin of Symbolic Logic 24 (3):291-305 (2018)
Abstract
The article approaches cut elimination from a new angle. On the basis of an arbitrary inference relation among logically atomic formulae, an inference relation on a language possessing logical operators is defined by means of inductive clauses similar to the operator-introducing rules of a cut-free intuitionistic sequent calculus. The logical terminology of the richer language is not uniquely specified, but assumed to satisfy certain conditions of a general nature, allowing for, but not requiring, the existence of infinite conjunctions and disjunctions. We investigate to what extent structural properties of the given atomic relation are preserved through the extension to the full language. While closure under the Cut rule narrowly construed is not in general thus preserved, two properties jointly amounting to closure under the ordinary structural rules, including Cut, are. Attention is then narrowed down to the special case of a standard first-order language, where a similar result is obtained also for closure under substitution of terms for individual parameters. Taken together, the three preservation results imply the familiar cut-elimination theorem for pure first-order intuitionistic sequent calculus. In the interest of conceptual economy, all deducibility relations are specified purely inductively, rather than in terms of the existence of formal proofs of any kind.
Keywords cut elimination  intuitionistic logic  infinitary logic  first-order logic  structural rules  atomic inferences
Categories (categorize this paper)
DOI 10.1017/bsl.2017.26
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 36,555
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Infinitary Propositional Intuitionistic Logic.Craig Kalicki - 1980 - Notre Dame Journal of Formal Logic 21 (2):216-228.
Infinitary Intuitionistic Logic From a Classical Point of View.Mark E. Nadel - 1978 - Annals of Mathematical Logic 14 (2):159-191.
Infinitary Intuitionistic Logic From a Classical Point of View.M. E. Nadel - 1978 - Annals of Mathematical Logic 14 (2):159.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

The Preservation of Coherence.R. E. Jennings & P. K. Schotch - 1984 - Studia Logica 43 (1-2):89 - 106.
What is the Logic of Inference?Jaroslav Peregrin - 2008 - Studia Logica 88 (2):263-294.
What Are Structural Properties?†.Johannes Korbmacher & Georg Schiemer - 2018 - Philosophia Mathematica 26 (3):295-323.
7. Preserving Logical Structure.Gillman Payette - 2009 - In Raymond Jennings, Bryson Brown & Peter Schotch (eds.), On Preserving: Essays on Preservationism and Paraconsistent Logic. Toronto: University of Toronto Press. pp. 105-144.
Logic Reduced To (Proof-Theoretical) Bare Bones.Jaroslav Peregrin - 2015 - Journal of Logic, Language and Information 24 (2):193-209.
Coherence of Structural and Functional Descriptions of Technical Artefacts.Peter Kroes - 2006 - Studies in History and Philosophy of Science Part A 37 (1):137-151.
Coherence of Structural and Functional Descriptions of Technical Artefacts.Peter Kroes - 2006 - Studies in History and Philosophy of Science Part A 37 (1):137-151.
On the Beth Properties of Some Intuitionistic Modal Logics.C. Luppi - 2002 - Archive for Mathematical Logic 41 (5):443-454.

Analytics

Added to PP index
2018-10-27

Total downloads
6 ( #691,861 of 2,302,576 )

Recent downloads (6 months)
6 ( #97,469 of 2,302,576 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature