Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-05T07:47:57.335Z Has data issue: false hasContentIssue false
  • English
  • Français

PRESERVATION OF STRUCTURAL PROPERTIES IN INTUITIONISTIC EXTENSIONS OF AN INFERENCE RELATION

Published online by Cambridge University Press:  25 October 2018

TOR SANDQVIST
TOR SANDQVIST*
Affiliation:
DIVISION OF PHILOSOPHY KTH ROYAL INSTITUTE OF TECHNOLOGY TEKNIKRINGEN 76 114 28 STOCKHOLM, SWEDENE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

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

03F05cut eliminationintuitionistic logicinfinitary logicfirst-order logicstructural rulesatomic inference
Type
Articles
Information
Bulletin of Symbolic Logic , Volume 24 , Issue 3 , September 2018 , pp. 291 - 305
Copyright
Copyright © The Association for Symbolic Logic 2018 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Gentzen, G., Investigations into logical deduction, The Collected Papers of Gerhard Gentzen (Szabo, M. E., editor), North-Holland, Amsterdam, 1969, pp. 68–131.Google Scholar
Kalicki, C., Infinitary propositional intuitionistic logic. Notre Dame Journal of Formal Logic, vol. 21 (1980), no. 2, pp. 216–228.CrossRefGoogle Scholar
Lorenzen, P., Einführung in die operative Logik und Mathematik, Springer, Berlin, 1955.CrossRefGoogle Scholar
Lorenzen, P., Metamathematik, Bibliographisches Institut AG, Mannheim, 1962.Google Scholar
Martin-Löf, P., Notes on Constructive Mathematics, Almqvist & Wiksell, Uppsala, 1970.Google Scholar
Nadel, M., Infinitary intuitionistic logic from a classical point of view. Annals of Mathematical Logic, vol. 14 (1978), no. 2, pp. 159–191.CrossRefGoogle Scholar
Novikoff, P. S., On the consistency of certain logical calculus. Matematičeskij Sbornik (Recueil Mathématique), vol. 12 (1943), no. 2, pp. 231–261.Google Scholar
Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Uppsala, 1965. Republished in 2006 by Dover Publications.Google Scholar