Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-20T07:30:19.570Z Has data issue: false hasContentIssue false
  • English
  • Français

THE ELIMINATION OF ATOMIC CUTS AND THE SEMISHORTENING PROPERTY FOR GENTZEN’S SEQUENT CALCULUS WITH EQUALITY

Part of: Proof theory and constructive mathematics

Published online by Cambridge University Press:  13 August 2019

FRANCO PARLAMENTO  and
FLAVIO PREVIALE
FRANCO PARLAMENTO
Affiliation:
DEPARTMENT OF MATHEMATICS, COMPUTER SCIENCE AND PHYSICS UNIVERSITY OF UDINE VIA DELLE SCIENZE 206, 33100UDINE, ITALYE-mail: [email protected]
FLAVIO PREVIALE
Affiliation:
DEPARTMENT OF MATHEMATICS UNIVERSITY OF TURIN VIA CARLO ALBERTO 10, 10123TORINO, ITALYE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We study various extensions of Gentzen’s sequent calculus obtained by adding rules for equality. One of them is singled out as particularly natural and shown to satisfy full cut elimination, namely, also atomic cuts can be eliminated. Furthermore we tell apart the extensions that satisfy full cut elimination from those that do not and establish a strengthened form of the nonlenghtening property of Lifschitz and Orevkov.

Keywords

sequent calculuscut eliminationequality rules

MSC classification

Primary: 03F05: Cut-elimination and normal-form theorems
Type
Research Article
Information
The Review of Symbolic Logic , Volume 14 , Issue 4 , December 2021 , pp. 813 - 837
Check for updates
Copyright
© Association for Symbolic Logic 2019

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

BIBLIOGRAPHY

Baaz, M. & Leitsch, A. (2011). Methods of Cut-Elimination. Trends in Logic 34. Dordrecht: Springer.Google Scholar
Curry, H. B. (1977). Foundations of Mathematical Logic. New York: Dover.Google Scholar
Degtyarev, A. & Voronkov, A. (2001). Equality reasoning in sequent-based calculi. In Robinson, A. and Voronkov, A., editors. Handbook of Automated Reasoning, Vol. 1. Amsterdam: Elsevier, pp. 613–706.Google Scholar
Gentzen, G. (1935). Untersuchungen uber der logische Schliessen. Matematische Zeitschrift, 39, 176–210, 405–431.CrossRefGoogle Scholar
Gallier, J. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. NewYork: Harper & Row.Google Scholar
Kanger, S. (1963). A simplified proof method for elementary logic. In Braffort, P. and Hirshberg, D., editors. Computer Programming and Formal Systems. Amsterdam: North-Holland, pp. 87–94.CrossRefGoogle Scholar
Lifschitz, A. V. (1968). Specialization of the form of deduction in the predicate calculus with equality and function symbols (in Russian). In Trudy MIAN, vol. 98, pp. 5–25. English translation in: Orevkov, V.P. (ed), The Calculi of Symbolic Logic. I, Proceedings of the Steklov Institute of Mathematics, 98 (1971).Google Scholar
Negri, S. & von Plato, J. (1998). Cut elimination in the presence of axioms. The Bulletin of Symbolic Logic, 4 (4), 418–435.CrossRefGoogle Scholar
Negri, S. & von Plato, J. (2001). Structural Proof Theory. Cambridge University Press.CrossRefGoogle Scholar
Orevkov, V. P. (1969). On nonlengthening applications of equality rules (in Russian). Zapiski Nauchnyh Seminarov LOMI, vol. 16, pp. 152–156. English translation in: Slisenko, A.O. (ed), Studies in Constructive Logic, Seminars in Mathematics: Steklov Math. Inst. 16, Consultants Bureau, NY-London, 77–79 (1971).Google Scholar
Parlamento, F. & Previale, F. (2013). Cut elimination for Gentzen’s sequent calculus with equality and logic of partial terms. Lecture Notes in Computer Science, 7750, 161–172.CrossRefGoogle Scholar
Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Stockholm: Almquist & Wiksell.Google Scholar
Takeuti, G. (1987). Proof Theory (second edition). Studies in Logic and the Foundations of Mathematics, Vol. 81. Amsterdam: North Holland.Google Scholar
Troelstra, A. S. & Schwichtenberg, H. (1996). Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, Vol. 43. Cambridge: Cambridge University Press.Google Scholar
Troelstra, A. S. & Schwichtenberg, H. (2000). Basic Proof Theory (second edition). Cambridge: Cambridge University Press.CrossRefGoogle Scholar
Wang, H. (1960). Towards mechanical mathematics. IBM Journal of Research and Development, 4, 2–22.CrossRefGoogle Scholar