Hostname: page-component-78c5997874-mlc7c Total loading time: 0 Render date: 2024-11-19T04:25:36.777Z Has data issue: false hasContentIssue false
  • English
  • Français

Sequent calculus in natural deduction style

Published online by Cambridge University Press:  12 March 2014

Sara Negri  and
Jan von Plato
Sara Negri
Affiliation:
University of Helsinki, Department of Philosophy, Helsinki, Finland, E-Mail: [email protected]
Jan von Plato
Affiliation:
University of Helsinki, Department of Philosophy, Helsinki, Finland, E-Mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract.

A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 66 , Issue 4 , December 2001 , pp. 1803 - 1816
Copyright
Copyright © Association for Symbolic Logic 2001

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

[1934–1935] Gentzen, G., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1934-35), pp. 176–210 and 405–431.CrossRefGoogle Scholar
[1936] Gentzen, G., Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112 (1936), pp. 493–565.CrossRefGoogle Scholar
[1969] Gentzen, G., The collected papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969, (Szabo, M., editor).Google Scholar
[2000] Negri, S., Natural deduction and normal form for intuitionistic linear logic, manuscript, 2000.Google Scholar
[1965] Prawitz, D., Natural deduction: A proof-theoretical study, Almqvist & Wicksell, Stockholm, 1965.Google Scholar
[1971] Prawitz, D., Ideas and results in proof theory, Proceedings of the second Scandinavian logic symposium (Fenstad, J., editor), North-Holland, 1971, pp. 235–308.CrossRefGoogle Scholar
[1984] Schroeder-Heister, P., A natural extension of natural deduction, this Journal, vol. 49 (1984), pp. 1284–1300.Google Scholar
[2001a] von Plato, J., Natural deduction with general elimination rules, Archive for Mathematical Logic, vol. 40 (2001), in press.CrossRefGoogle Scholar
[2001b] Prawitz, D., A proof of Gentzen's Hauptsatz without multicut, Archive for Mathematical Logic, vol. 40 (2001), pp. 9–18.Google Scholar