Hostname: page-component-78c5997874-mlc7c Total loading time: 0 Render date: 2024-11-20T00:52:34.913Z Has data issue: false hasContentIssue false
  • English
  • Français

Hilbert's program relativized; Proof-theoretical and foundational reductions

Published online by Cambridge University Press:  12 March 2014

Solomon Feferman
Solomon Feferman*
Affiliation:
Department of Mathematics, Stanford University, Stanford, California 94305
Get access Rights & Permissions [Opens in a new window]

Extract

In the Symposium on Hilbert's Program to which the following was contributed, I was asked to talk about the metamathematical aspects of Hilbert's Program (H.P.), while the other two speakers (Simpson and Prawitz) were to deal with the mathematical and philosophical aspects respectively. However, more so than for other foundational schemes, these three aspects of H.P., both as originally conceived and in its subsequent developments, are intimately linked.

Here I shall survey a body of proof-theoretical results stemming from H.P., but organized in a way that is closely tied to various reductive foundational aims, albeit going beyond those advanced by Hilbert. I believe this view of reductive proof-theory (not original with me) helps one to better understand what has been achieved thereby than other, more familiar accounts.

Type
Survey/Expository Papers
Information
The Journal of Symbolic Logic , Volume 53 , Issue 2 , June 1988 , pp. 364 - 384
Copyright
Copyright © Association for Symbolic Logic 1988

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

Barwise, J. and Schlipf, J. [1975] On recursively saturated models of arithmetic, Model theory and algebra, Lecture Notes in Mathematics, vol. 498, Springer-Verlag, Berlin, pp. 42–55.CrossRefGoogle Scholar
Beeson, M. [1985] Foundations of constructive mathematics. Metamathematical studies, Springer-Verlag, Berlin.CrossRefGoogle Scholar
Benacerraf, P. and Putnam, H. (editors) [1983] Philosophy of mathematics, 2nd ed., Cambridge University Press, Cambridge.Google Scholar
Bernays, P. [1967] Hilbert, David, Encyclopedia of philosophy. Vol. 3, Macmillan and Free Press, New York, pp. 496–504.Google Scholar
Buchholz, W., Feferman, S., Pohlers, W. and Sieg, W. [1981] Iterated inductive definitions and subsystems of analysis: recent proof-theoretic studies, Lecture Notes in Mathematics, vol. 897, Springer-Verlag, Berlin.Google Scholar
Feferman, S. [1964] Systems of predicative analysis, this Journal, vol. 29, pp. 1–30.Google Scholar
Feferman, S. [1970] Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, Intuitionism and proof theory, North-Holland, Amsterdam, pp. 303–326.Google Scholar
Feferman, S. [1971] Ordinals and functions in proof theory, Actes du Congrès International des Mathématiciens (Nice, 1970), Vol. 1, Gauthier-Villars, Paris, pp. 220–233.Google Scholar
Feferman, S. [1977] Theories of finite type related to mathematical practice, Handbook of mathematical logic, North-Holland, Amsterdam, pp. 913–971.CrossRefGoogle Scholar
Feferman, S. [1979] A more perspicuous system for predicativity, Konstruktionen vs. Positionen. I, de Gruyter Berlin, pp. 87–139.Google Scholar
Feferman, S. [1979a] Constructive theories of functions and classes, Logic Colloquium '78, North-Holland, Amsterdam, pp. 159–224.Google Scholar
Feferman, S. [1982] Iterated inductive fixed-point theories, Patras logic symposion, North-Holland, Amsterdam, pp. 171–196.CrossRefGoogle Scholar
Feferman, S. [1982a] Monotone inductive definitions, The L. E. J. Brouwer centenary symposium, North-Holland, Amsterdam, pp. 77–89.Google Scholar
Feferman, S. [1985] A theory of variable finite types, Revista Colombiana de Matemáticas, vol. 19, pp. 95–105.Google Scholar
Feferman, S. [1987] Proof theory: a personal report, Appendix to Takeuti [1987], pp. 447–485.Google Scholar
Feferman, S. and Jäger, G. [1983] Choice principles, the bar rule and iterated comprehension principles in analysis, this Journal, vol. 48, pp. 63–70.Google Scholar
Feferman, S. and Sieg, W. [1981] Iterated inductive definitions and subsystems of analysis, Chapter I in Buchholz, et al. [1981], pp. 16–77.CrossRefGoogle Scholar
Feferman, S. and Sieg, W. [1981a] Proof theoretic equivalences between classical and constructive theories for analysis, Chapter II in Buchholz, et al. [1981], pp. 78–142.CrossRefGoogle Scholar
Friedman, H. [1970] Iterated inductive definitions and , Intuitionism and proof theory, North-Holland, Amsterdam, pp. 435–442.Google Scholar
Friedman, H. [1976] Systems of second order arithmetic. I,II (abstracts), this Journal, vol. 41, pp. 557–559.Google Scholar
Friedman, H., McAloon, K. and Simpson, S. G. [1982] A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis, Patras logic symposion, North-Holland, Amsterdam, pp. 197–220.CrossRefGoogle Scholar
Gentzen, G. [1936] Die Widerspruchsfreikeit der reinen Zahlentheorie, Mathematische Annalen, vol. 112, pp. 493–565 (translated in Gentzen [1969], pp. 132–200).CrossRefGoogle Scholar
Gentzen, G. [1969] The collected papers of Gerhard Gentzen (Szabo, M. E., editor), North-Holland Amsterdam.Google Scholar
Gödel, K. [1931] Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme . I, Monatshefte für Mathematik und Physik, vol. 38, pp. 173–198 (reproduced, with translation, in Gödel [1986], pp. 144–195).CrossRefGoogle Scholar
Gödel, K. [1933] Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines Mathematischen Kolloquiums, vol. 4, pp. 34–38 (reproduced, with translation, in Gödel [1986], pp. 286–295).Google Scholar
Gödel, K. [1958] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, vol. 12, pp. 280–287.CrossRefGoogle Scholar
Gödel, K. [1986] Collected works. Vol. I: Publications 1929–1936 (Feferman, S. et al., editors), Oxford University Press, New York.Google Scholar
Hilbert, D. [1926] Über das Unendliche, Mathematische Annalen, vol. 95, pp. 161–190 (translated in van Heijenoort [1967], pp. 367–392).CrossRefGoogle Scholar
Hilbert, D. [1931] Beweis des tertium non datur, Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-Physikalische Klasse, pp. 120–125.Google Scholar
Hilbert, D. and Bernays, P. [1934] Grundlagen der Mathematik. Vol. I, Springer-Verlag, Berlin.Google Scholar
Hilbert, D. and Bernays, P. [1939] Grundlagen der Mathematik. Vol. II, Springer-Verlag, Berlin.Google Scholar
Jäger, G. [1983] A well-ordering proof for Feferman's theory T0 , Archiv für Mathematische Logik und Grundlagenforschung, vol. 23, pp. 65–77.CrossRefGoogle Scholar
Hilbert, D. and Bernays, P. [1984] Theories for admissible sets: a unifying approach to proof theory, Habilitationsschrift, Universität München.Google Scholar
Jäger, G. and Pohlers, W. [1982] Eine beweistheoretische Untersuchung von ( und verwandter Systeme, Sitzungsberichte der Bayerische Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse, pp. 1–28.Google Scholar
Kreisel, G. [1958] Ordinal logics and the characterization of informal concepts of proof, Proceedings of the International Congress of Mathematicians (Edinburgh, 1958), Cambridge University Press, Cambridge, 1960, pp. 289–299.Google Scholar
Kreisel, G. [1958a] Hilbert's programme, Dialectica, vol. 12, pp. 346–372 (revised, with Postscript, in Benacerraf and Putnam [1983], pp. 207–238).CrossRefGoogle Scholar
Kreisel, G. [1968] A survey of proof theory, this Journal, vol. 33, pp. 321–388.Google Scholar
Kreisel, G. [1976] What have we learned from Hilbert's second problem? Mathematical developments arising from Hilbert problems, Proceedings of Symposia in Pure Mathematics, vol. 28, American Mathematical Society, Providence, R.I., pp. 93–130.Google Scholar
Parsons, C. [1970] On a number-theoretic choice schema and its relation to induction, Intuitionism and proof theory, North-Holland, Amsterdam, pp. 459–473.Google Scholar
Pohlers, W. [1981] Proof-theoretical analysis of IDν by the method of local predicativity, in Buchholz, et al. [1981], pp. 261–237.CrossRefGoogle Scholar
Pohlers, W. [1987] Contributions of the Schütte school in Munich to proof theory, Appendix to Takeuti [1987].Google Scholar
Schütte, K. [1960] Beweistheorie, Springer-Verlag, Berlin.Google Scholar
Schütte, K. [1964] Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik, Archiv für Mathematische Logik und Grundlagenforschung, vol. 7, pp. 45–60.CrossRefGoogle Scholar
Schütte, K. [1965] Predicative well-orderings, Formal systems and recursive functions, North-Holland, Amsterdam, pp. 280–303.CrossRefGoogle Scholar
Schütte, K. [1977] Proof theory. Springer-Verlag, Berlin.Google Scholar
Shoenfield, J. [1954] A relative consistency proof, this Journal, vol. 19, pp. 21–28.Google Scholar
Sieg, W. [1981] Inductive definitions, constructive ordinals, and normal derivations, in Buchholz, et al. [1981], pp. 143–187.Google Scholar
Sieg, W. [1985] Fragments of arithmetic, Annals of Pure and Applied Logic, vol. 28, pp. 33–72.CrossRefGoogle Scholar
Sieg, W. [1988] Hilbert's program sixty years later, this Journal, vol. 53, pp. 338–348.Google Scholar
Simpson, S. G. [1984] Reverse mathematics, Recursion theory, Proceedings of Symposia in Pure Mathematics, vol. 42, American Mathematical Society, Providence, R.I., pp. 461–472.CrossRefGoogle Scholar
Simpson, S. G. [1985] Friedman's research on subsystems of second order arithmetic, Harvey Friedman's research in the foundations of mathematics, North-Holland, Amsterdam, pp. 137–159.CrossRefGoogle Scholar
Simpson, S. G. [1988] Partial realizations of Hilbert's program, this Journal, vol. 53, pp. 349–363.Google Scholar
Smoryński, C. [1985] Nonstandard models and related developments, Harvey Friedman's research in the foundations of mathematics, North-Holland, Amsterdam, pp. 179–229.CrossRefGoogle Scholar
Tait, W. W. [1981] Finitism, Journal of Philosophy, vol. 78, pp. 524–546.CrossRefGoogle Scholar
Takahashi, S. [1986] Monotone inductive definitions in a constructive theory of functions and classes, Dissertation, Stanford University.Google Scholar
Takeuti, G. [1975] Proof theory, North-Holland, Amsterdam.Google Scholar
Takeuti, G. [1978] Two applications of logic to mathematics, Publications of the Mathematical Society of Japan, vol. 13, Iwanami Shoten, Tokyo, and Princeton University Press, Princeton, N.J. Google Scholar
Takeuti, G. [1987] Proof theory, 2nd ed., North-Holland, Amsterdam.Google Scholar
Tarski, A., Mostowski, A. and Robinson, R. M. [1953] Undecidable theories, North-Holland, Amsterdam.Google Scholar
Troelstra, A. S. (editor) [1973] Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin.CrossRefGoogle Scholar
van Heijenoort, J. (editor) [1967] From Frege to Gödel: a source book in mathematical logic, 1897–1931, Harvard University Press, Cambridge, Mass. Google Scholar