Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-26T19:31:06.708Z Has data issue: false hasContentIssue false
  • English
  • Français

FROM STENIUS’ CONSISTENCY PROOF TO SCHÜTTE’S CUT ELIMINATION FOR ω-ARITHMETIC

Published online by Cambridge University Press:  22 December 2015

ANNIKA SIDERS
ANNIKA SIDERS*
Affiliation:
University of Helsinki
*
*DEPARTMENT OF PHILOSOPHY P.O. BOX 24 (UNIONINKATU 40 A) FI - 00014 UNIVERSITY OF HELSINKI FINLAND E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The book Das Interpretationsproblem der Formalisierten Zahlentheorie und ihre Formale Widerspruchsfreiheit by Erik Stenius published in 1952 contains a consistency proof for infinite ω-arithmetic based on a semantical interpretation. Despite the proof’s reference to semantics the truth definition is in fact equivalent to a syntactical derivability or reduction condition. Based on this reduction condition Stenius proves that the complexity of formulas in a derivation can be limited by the complexity of the conclusion. This independent result can also be proved by cut elimination for ω-arithmetic which was done by Schütte in 1951.

In this paper we interpret the syntactic reduction in Stenius’ work as a method for cut elimination based on invertibility of the logical rules. Through this interpretation the constructivity of Stenius’ proof becomes apparent. This improvement was explicitly requested from Stenius by Paul Bernays in private correspondence (In a letter from Bernays begun on the 19th of September 1952 (Stenius & Bernays, 1951–75)). Bernays, who took a deep interest in Stenius’ manuscript, applied the described method in a proof Herbrand’s theorem. In this paper we prove Herbrand’s theorem, as an application of Stenius’ work, based on lecture notes of Bernays (Bernays, 1961). The main result completely resolves Bernays’ suggestions for improvement by eliminating references to Stenius’ semantics and by showing the constructive nature of the proof. A comparison with Schütte’s cut elimination proof shows how Stenius’ simplification of the reduction of universal cut formulas, which in Schütte’s proof requires duplication and repositioning of the cuts, shifts the problematic case of reduction to implications.

Type
Research Article
Information
The Review of Symbolic Logic , Volume 9 , Issue 1 , March 2016 , pp. 1 - 22
Copyright
Copyright © Association for Symbolic Logic 2015 

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

Bernays, P. (1952). Paul Bernays’ lecture on Erik Stenius’ das Interpretationsproblem … (Kept as Hs 973:86 “Betr. Abh. von Stenius” in the archive of the ETH Zurich).Google Scholar
Bernays, P. (1954). Über den Zusammenhang des Herbrandschen Satses mit den neueren Ergebnissen von Schütte and Stenius. In Proceedings of the International Congress of Mathematicians 1954, vol. II.Google Scholar
Bernays, P. (1961). Paul Bernays’ lectures on the aims and topics of proof theory (Kept as Hs 973:28 “Aims and topics of proof theory” in the archive of the ETH Zurich).Google Scholar
Bernays, P. (1970). On the Original Gentzen Consistency Proof for Number Theory, In Kino, Myhill & Vesley, , editors. Intuitionism and Proof Theory, pp. 409–417.Google Scholar
Buss, S. (1998). Handbook Proof Theory. Elsevier: Amsterdam.Google Scholar
Gentzen, G. (1934). Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, 39, 405–431.Google Scholar
Gentzen, G. (1938). Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie, Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, 4, 19–44.Google Scholar
Gentzen, G. (1974). Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie, Archiv für Mathematische Logik und Grundlagenforschung 16, 97–118.Google Scholar
Ketonen, O. (1944). Untersuchungen zum Prädikatenkalkül. Annales Academiae Scientarum Fennicae, Series A.1, 23.Google Scholar
Kreisel, G. (1953). Reviewed work(s): Das Interpretationsproblem der formalisierten Zahlentheorie und ihre formale Widerspruchsfreiheit by Erik Stenius. Journal of Symbolic Logic, 18(3): 262–263.Google Scholar
Negri, S. & von Plato, J. (1998). Cut elimination in the presence of axioms. The Bulletin of Symbolic Logic, 4, 418–435.Google Scholar
Negri, S. & von Plato, J. (2001). Structural Proof Theory. Cambridge University Press, Cambridge.Google Scholar
von Plato, J. (2001). A proof of Gentzen’s Hauptsatz without multicut. Archive for Mathematical Logic, 40, 9–18.Google Scholar
von Plato, J. (2006). Normal form and existence property for derivations in Heyting arithmetic. Acta Philosophica Fennica, 78, 159–163.Google Scholar
Schütte, K. (1951). Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie. Mathematische Annalen, 122(5), 369–389.CrossRefGoogle Scholar
Stenius, E. (1952). Das Interpretationsproblem der Formalisierten Zahlentheorie und ihre Formale Widerspruchsfreiheit. Acta Academiae Aboensis, Åbo.Google Scholar
Stenius, E. (1956). ‘Drafts for new versions of Das Interpretationsproblem from Stenius’ manuscripts’, kept as II.1 ‘Bevisteori. Utkast till ombearbetning av Das Interpretationsproblem -56. Kommentarer till Bernays, Büchli, Wright, Curry o.a’ in the archive of the National Library of Finland in Helsinki.Google Scholar
Stenius, E. & Bernays, P. (1951–75). Correspondence between Stenius and Bernays from Stenius’ manuscripts’, 8 letters from Bernays are kept as XII.1 and 5 letters to Bernays are kept as XII.2 in the archive of the National Library of Finland in Helsinki.Google Scholar
Tait, W. W. (2015). Gentzen’s original consistency proof and the Bar Theorem. In Kahle, & Rathjen, , editors. Gentzen’s Centenary: The Quest for Consistency, Berlin: Springer.Google Scholar