Abstract
The notion of proof-theoretical or finitistic reduction of one theory to another has a long tradition. Feferman and Sieg (Buchholz et al., Iterated inductive definitions and subsystems of analysis. Springer, Berlin, 1981, Chap. 1) and Feferman in (J Symbol Logic 53:364–384, 1988) made first steps to delineate it in more formal terms. The first goal of this paper is to corroborate their view that this notion has the greatest explanatory reach and is superior to others, especially in the context of foundational theories, i.e., theories devised for the purpose of formalizing and presenting various chunks of mathematics.
A second goal is to address a certain puzzlement that was expressed in Feferman’s title of his Clermont-Ferrand lectures at the Logic Colloquium 1994: “How is it that finitary proof theory became infinitary?” Hilbert’s aim was to use proof theory as a tool in his finitary consistency program to eliminate the actual infinite in mathematics from proofs of real statements. Beginning in the 1950s, however, proof theory began to employ infinitary methods. Infinitary rules and concepts, such as ordinals, entered the stage.
In general, the more that such infinitary methods were employed, the farther did proof theory depart from its initial aims and methods, and the closer did it come instead to ongoing developments in recursion theory, particularly as generalized to admissible sets; in both one makes use of analogues of regular cardinals, as well as “large” cardinals (inaccessible, Mahlo, etc.). (Feferman 1994).
The current paper aims to explain how these infinitary tools, despite appearances to the contrary, can be formalized in an intuitionistic theory that is finitistically reducible to (actually \(\Pi ^0_2\)-conservative over) intuitionistic first order arithmetic, also known as Heyting arithmetic. Thus we have a beautiful example of Hilbert’s program at work, exemplifying the Hilbertian goal of moving from the ideal to the real by eliminating ideal elements.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
See Centrone (2011).
- 2.
{x∣χ(x)} constitutes the domain over which the interpreted quantifiers of \(\mathcal {L}_1\)-formulas will be ranging; so quantifiers become relativized to {x∣χ(x)}.
- 3.
- 4.
Here \(\mathbf {I}\Sigma ^0_1\) stands for the fragment of PA with induction restricted to \(\Sigma ^0_1\)-formulas, PRA for primitive recursive arithmetic, and WKL 0 for a fragment of Z 2 in which weak König’s Lemma is the signature axiom. WKL 0 is a very famous system in the program of reverse mathematics (cf. Simpson 2009).
- 5.
A formula is almost negative if it does not contain ∨, and ∃ only immediately in front of \(\Delta ^0_0\) formulas.
- 6.
A geometric theory (sometimes called coherent theory) is one whose axioms are geometric implications, i.e. universal closures of implications of the form
, where each D
i is a positive formula, i.e. a formula built up from atoms using solely conjunction, disjunction and existential quantification. - 7.
\(\Sigma ^1_2\mbox{-}\mathbf {AC}\) is the schema ∀x∃Y B(x, Y ) →∃Z∀x B(x, Z x) with B(x, Y ) of complexity \(\Sigma ^1_2\) and Z x = {u∣2x3u ∈ Z}. Bar induction stands for the schema of transfinite induction along a well-founded set relation for all second order formulas. This theory is very strong from the point of view of reverse mathematics. In reverse mathematics one aims to calibrate the strength of theorems from ordinary mathematics, using as a scale certain natural subsystems of Z 2. It has turned out that there are five systems (dubbed the “big five”) that occur most often. All of them are much weaker than \(\Sigma ^1_2\mbox{-}\mathbf {AC} +\mbox{Bar Induction}\). Since the latter is reducible to Martin-Löf type theory, it follows that almost all \(\Pi ^0_2\)-theorems of ordinary mathematics are constructively true (for more on this see Rathjen 2005a).
- 8.
Recall that in 1905 several famous French analysts wanted to ban AC for uncountable families of sets from mathematics (see Jervell 1996).
- 9.
- 10.
I.e., going through the impossible and the imaginary, respectively.
- 11.
For a partial realization of Hilbert’s original program see Simpson (1988).
- 12.
At the time a particular focus of proof theorists was Spector’s 1960 functional interpretation of Z 2 via bar recursive functionals. The question whether such functionals are acceptable on constructive grounds was of great interest to proof theorists, constructivists and logicians who wanted to plumb the boundaries of constructivism (e.g. Gödel).
- 13.
Note that there have to be n 1 function symbols substituted into a function symbol with arity n 1.
- 14.
This is also the reason why complete proofs of Gödel’s second incompleteness theorem are hard to find in the literature.
, where each D
i is a positive formula, i.e. a formula built up from atoms using solely conjunction, disjunction and existential quantification.References
Aczel, P. (1982). The type theoretic interpretation of constructive set theory: Choice principles. In A. S. Troelstra & D. van Dalen (Eds.), The L.E.J. Brouwer centenary symposium (pp. 1–40). Amsterdam: North Holland.
Aczel, P. (1986). The type theoretic interpretation of constructive set theory: Inductive definitions. In R. B. Marcus et al. (Eds.), Logic, methodology and philosophy of science VII (pp. 17–49). Amsterdam: North Holland.
Aczel, P., & Rathjen, M. (2001). Notes on constructive set theory (Technical report 40), Institut Mittag-Leffler, The Royal Swedish Academy of Sciences. http://www.mittag-leffler.se/preprints/0001/, Preprint No. 40.
Aczel, P., & Rathjen, M. (2010). Notes on constructive set theory, Preprint, p. 243. http://www1.maths.leeds.ac.uk/~rathjen/book.pdf.
Achourioti, T., & van Lambalgen, M. (2017). Kant’s logic revisited. IfCoLog Journal of Logics and Their Applications, 4, 845–865.
Arai, T. (1998). Some results on cut-elimination, provable well-orderings, induction and reflection. Annals of Pure and Applied Logic, 95, 93–184.
Barr, M. (1974). Toposes without points. Journal of Pure and Applied Algebra, 5, 265–280.
Barwise, J. (1975). Admissible sets and structures. Berlin: Springer.
Barwise, J., & Schlipf, J. (1975). On recursively saturated models of arithmetic (Lecture notes in mathematics, Vol. 498, pp. 42–55). Berlin: Springer.
Buchholz, W. (1981). The Ωμ+1-Rule. In W. Buchholz, S. Feferman, W. Pohlers, & W. Sieg (Eds.), Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies. Berlin: Springer.
Buchholz, W. (1993). A simplified version of local predicativity. In P. Aczel, H. Simmons, & S. Wainer (Eds.), Leeds proof theory 90 (pp. 115–147). Cambridge: Cambridge University Press.
Buchholz, W. (1997). An intuitionistic fixed point theory. Archive for Mathematical Logic, 37, 21–27.
Buchholz, W., & Schütte, K. (1988). Proof theory of impredicative subsystems of analysis. Napoli: Bibliopolis.
Buchholz, W., Feferman, S., Pohlers, W., & Sieg, W. (1981). Iterated inductive definitions and subsystems of analysis. Berlin: Springer.
Caldon, P., & Ignjatović, A. (2005). On mathematical instrumentalism. Journal of Symbolic Logic, 70, 778–794.
Centrone, S. (2011). Husserls Doppelvortrag in der Mathematischen Gesellschaft in Göttingen 1901. In C. Beyer & K. Cramer (Hg.), Edmund Husserl 1859–2009. Beiträge aus Anlass der 150. Wiederkehr des Geburtstages des Philosophen, Abhandlungsreihe der Akademie der Wissenschaften zu Göttingen ADW 14 (pp. 107–128). Berlin: De Gruyter.
Crosilla, L., & Rathjen, M. (2002). Inaccessible set axioms may have little consistency strength. Annals of Pure and Applied Logic, 115, 33–70.
Dyckhoff, R., & Negri, S. (2015). Geometrization of first-order logic. The Bulletin of Symbolic Logic, 21, 123–163.
Feferman, S. (1982). Iterated inductive fixed-points theories: Application to Hancock’s conjecture. In G. Metakides (Ed.), Patras symposium (pp. 171–196). Amsterdam: North-Holland.
Feferman, S. (1988). Hilbert’s program relativized: Proof-theoretical and foundational reductions. Journal of Symbolic Logic, 53, 364–384.
Feferman, S. (1994). How is it that finitary proof theory became infinitary? Abstract for the ASL Logic Colloquium 1994 in Claremont-Ferrand.
Feferman, S. (2000). Does reductive proof theory have a viable rationale?. Erkenntnis, 53, 63–96.
Felgner, U. (1971). Comparison of the axioms of local and universal choice. Fundamenta Mathematicae, 71, 43–62.
Friedman, H. (1976). Systems of second order arithmetic with restricted induction, I, II (abstracts). Journal of Symbolic Logic, 41, 557–559.
Gentzen, G. (1933). Über das Verhältnis zwischen intuitionistischer und klassischer Logik. Originally to appear in the Mathematische Annalen, reached the stage of galley proofs but was withdrawn. It was finally published in 1974 in Arch. Math. Logik 16, 119–132.
Gödel, K. (1933). Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines mathematischen Kolloquiums, 4, 34–38.
Gödel, K. (1938). The consistency of the axiom of choice and of the generalized continuum-hypothesis. Proceedings of the National Academy of Sciences of the United States of America, 24, 556–557.
Gödel, K. (1940). The consistency of the continuum-hypothesis. Princeton, NJ: Princeton University Press.
Gödel, K. (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12, 280–287.
Goodman, N. (1976). The theory of the Gödel functionals. Journal of Symbolic Logic, 41, 574–583.
Goodman, N. (1978). Relativized realizability in intuitionistic arithmetic of all finite types. Journal of Symbolic Logic, 43, 23–44.
Hilbert, D. (1926). Über das Unendliche. Mathematische Annalen 95, 161–190. English translation. In J. van Heijenoort (Ed.), From frege to Gödel. A source book in mathematical logic, 1897–1931. Cambridge, MA: Harvard University Press (1967).
Hilbert, D., & Bernays, P. (1939). Grundlagen der Mathematik II. Berlin: Springer.
Husserl, E. (1983). Studien zur Arithmetik und Geometrie. Texte aus dem Nachlass 1886–1901. Husserliana Band XXI, I. Strohmeyer (Hrsg.). Den Haag: Martinus Nijhoff.
Jervell, H. (1996). From the axiom of choice to choice sequences. Nordic Journal of Philosophical Logic, 1, 95–98.
Kleene, S. C. (1945). On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10, 109–124.
Kolmogorov, A. N. (1925). On the principle of the excluded middle (Russian). Matematicheskii Sbornik, 32, 646–667. Translated in van Heijenoort (1967), 414–437.
Lindström, P. (1997). Aspects of incompleteness (Lecture notes in logic, Vol. 10). Berlin: Springer.
Niebergall, K.-G. (2000). On the logic of reducibility: Axioms and examples. Erkenntnis, 53, 27–61.
Parsons, C. (1970). On a number-theoretic choice schema and its relation to induction. In J. Myhill, A. Kino, & R. E. Vesley (Eds.), Intuitionism and proof theory (pp. 459–473). Amsterdam: North-Holland.
Platek, R. A. (1969). Eliminating the continuum hypothesis. Journal of Symbolic Logic, 34, 219–225.
Pohlers, W. (1981). Proof–theoretical analysis of ID ν by the method of local predicativity. In W. Buchholz, S. Feferman, W. Pohlers, & W. Sieg (Eds.), Iterated inductive definitions and subsystems of analysis (pp. 261–357). Berlin: Springer.
Rathjen, M. (1993). The strength of some Martin–Löf type theories. Preprint, Department of Mathematics, Ohio State University (p. 39).
Rathjen, M. (1994). Proof theory of reflection. Annals of Pure and Applied Logic, 68, 181–224.
Rathjen, M. (1999). The realm of ordinal analysis. In S. B. Cooper & J. K. Truss (Eds.), Set and Proofs (London mathematical society lecture note series, Vol. 258, pp. 219–279). Cambridge: Cambridge University Press.
Rathjen, M. (2005a). The constructive Hilbert programme and the limits of Martin-Löf type theory. Synthese, 147, 81–120.
Rathjen, M. (2005b). An ordinal analysis of stability. Archive for Mathematical Logic, 44, 1–62.
Rathjen, M. (2005c). An ordinal analysis of parameter-free \(\Pi ^1_2\)-comprehension. Archive for Mathematical Logic, 44, 263–362.
Rathjen, M. (2006). The art of ordinal analysis. In M. Sanz-Solé, J. Soria, J. L. Varona, & J. Verdera (Eds.), Proceedings of the International Congress of Mathematicians Madrid 2006 (Vol. II, pp. 45–69). European Mathematical Society.
Rathjen, M. (2016). Remarks on Barr’s theorem. Proofs in geometric theories. In D. Probst & P. Schuster (Eds.), Concepts of proof in mathematics, philosophy, and computer science (Ontos mathematical logic, Vol. 6, pp. 347–374). Berlin: Walter de Gruyter.
Rathjen, M. (2017). Proof theory of constructive systems: Inductive types and univalence. In G. Jäger & W. Sieg (Eds.), Feferman on foundations – logic, mathematics, philosophy (Outstanding contributions to logic, Vol. 13, pp. 385–419). Cham: Springer.
Rathjen, M., & Weiermann, A. (1993). Proof–theoretic investigations on Kruskal’s theorem. Annals of Pure and Applied Logic, 60, 49–88.
Rüede, C., & Strahm, T. (2002). Intuitionistic fixed point theories for strictly positive operators. Mathematical Logic Quarterly, 48(2), 195–202.
Schütte, K. (1977). Proof theory. Berlin: Springer.
Schwichtenberg, H. (1977). Proof theory: Some applications of cut-elimination. In J. Barwise (Ed.), Handbook of mathematical logic (pp. 867–895). Amsterdam: North Holland.
Setzer, T. (1993). Proof theoretical strength of Martin–Löf type theory with W–type and one universe. Thesis, University of Munich.
Setzer, A. (1998). A well-ordering proof for the proof theoretical strength of Martin-Löf type theory. Annals of Pure and Applied Logic, 92, 113–159.
Shoenfield, J. R. (1961). The problem of predicativity. In Essays on the foundation of mathematics (pp. 132–139). Amsterdam: North-Holland.
Simpson, S. (1988). Partial realizations of Hilbert’s program. Journal of Symbolic Logic, 53, 349–363.
Simpson, S. (2009). Subsystems of second order arithmetic (2nd ed.). New York: Cambridge University Press.
Smorynski, C. (1977). The incompleteness theorems. In J. Barwise (Ed.), Handbook of mathematical logic (pp. 821–865). Amsterdam: North Holland.
Tait, W. (1981). Finitism. Journal of Philosophy, 78, 524–546.
Takeuti, G. (1987). Proof theory (2nd ed.). Amsterdam: North-Holland.
Toppel, M. (2016). Complexities of proof-theoretical reductions. Ph.D. thesis, University of Leeds. Online accessible at: http://etheses.whiterose.ac.uk/16456/.
van Heijenoort, J. (Ed.). (1967). From Frege to Gödel. A source book in mathematical logic 1879–1931. Cambridge, MA: Harvard University Press.
Acknowledgements
This publication was made possible through the support of a grant from the John Templeton Foundation (“A new dawn of intuitionism: mathematical and philosophical advances,” ID 60842). The opinions expressed in this publication are those of the authors and do not necessarily reflect the views of the John Templeton Foundation.
A substantial part of this paper was written while the first author participated in the trimester Types, Sets and Constructions May – August 2018 at the Hausdorff Research Institute for Mathematics (HIM), University of Bonn. His visit was supported by the HIM. Both, the support and the hospitality of HIM, are gratefully acknowledged. The second author was supported by University Research Scholarship of the University of Leeds.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Rathjen, M., Toppel, M. (2019). On Relating Theories: Proof-Theoretical Reduction. In: Centrone, S., Negri, S., Sarikaya, D., Schuster, P.M. (eds) Mathesis Universalis, Computability and Proof. Synthese Library, vol 412. Springer, Cham. https://doi.org/10.1007/978-3-030-20447-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-20447-1_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20446-4
Online ISBN: 978-3-030-20447-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)