Hostname: page-component-cd9895bd7-gxg78 Total loading time: 0 Render date: 2024-12-25T01:31:52.906Z Has data issue: false hasContentIssue false
  • English
  • Français

Pure Proof Theory Aims, Methods and Results: Extended Version of Talks Given at Oberwolfach and Haifa

Published online by Cambridge University Press:  15 January 2014

Wolfram Pohlers
Wolfram Pohlers*
Affiliation:
Institute for Mathematical Logic and Foundational Research, University of Munster, Germany.E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and I apologize for not displaying these results as well.

Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.

1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.

By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.

Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 2 , Issue 2 , June 1996 , pp. 159 - 188
Copyright
Copyright © Association for Symbolic Logic 1986

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

[1] Barwise, J., Admissible Sets and Structures, Springer-Verlag, 1975.CrossRefGoogle Scholar
[2] Blankertz, B. and Weiermann, A., A uniform approach for characterizing the provably total number theoretic functions of KPM and its subsystems, to appear.Google Scholar
[3] Buchholz, W., A simplified version of localpredicativity, Proof Theory (Aczel, P., Simmons, H., and Wainer, S., editors), Cambridge University Press, 1992.Google Scholar
[4] Buchholz, W., Cichon, A., and Weiermann, A., A uniform approach to fundamental sequences and hierarchies, Mathematical Logic Quarterly, vol. 58 (1993), pp. 664–671.Google Scholar
[5] Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, Springer Lecture Notes in Mathematics, no. 897, Springer-Verlag, 1981.Google Scholar
[6] Feferman, S., Systems of predicative analysis, Journal of Symbolic Logic, vol. 19 (1964), pp. 1–30.CrossRefGoogle Scholar
[7] Feferman, S., A language and axioms for explicit mathematics, Springer Lecture Notes in Mathematics, no. 450, Springer-Verlag, 1975.CrossRefGoogle Scholar
[8] Jäger, G., A well-ordering proof for Fefermans theory T0 , Archive for Mathematical Logic, vol. 22 (1983).Google Scholar
[9] Jäger, G., Theories for Admissible Sets: A Unifying Approach to Proof Theory, Bibliopolis, 1986.Google Scholar
[10] Jäger, G. and Pohlers, W., Eine beweistheoretische Untersuchung von ( -CA) + (BI) und verwandter Systeme, Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematik-Naturwissenschaft Klasse, 1982, pp. 1–28.Google Scholar
[11] Pohlers, W., Cut elimination for impredicative infinitary systems, Part I, Archive for Mathematical Logic, vol. 21 (1981), pp. 69–87.Google Scholar
[12] Pohlers, W., Proof-theoretical analysis of IDv by the method of local predicativity , Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies (Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., editors), Springer Lecture Notes in Mathematics, no. 897, Springer-Verlag, 1981.Google Scholar
[13] Pohlers, W., Cut elimination for impredicative infinitary systems, Part II, Archive for Mathematical Logic, vol. 22 (1982), pp. 113–129.Google Scholar
[14] Pohlers, W., Proof Theory: An Introduction, Springer Lecture Notes in Mathematics, no. 1407, Springer-Verlag, 1989.CrossRefGoogle Scholar
[15] Pohlers, W., Proof theory and ordinal analysis, Archive for Mathematical Logic, vol. 30 (1991), pp. 311–376.CrossRefGoogle Scholar
[16] Pohlers, W., A short course in ordinal analysis, Proof Theory (Aczel, P., Simmons, H., and Wainer, S., editors), Cambridge University Press, 1992.Google Scholar
[17] Rathjen, M., Untersuchungen zu Teilsystemen der Zahlentheorie zweiter Stufe und der Mengenlehre mit einer zwischen ( -CA) und ( -CA) + (BI) liegenden Beweisstärke, Ph.D. thesis, Münster, 1989.Google Scholar
[18] Rathjen, M., Proof theoretic analysis of KPM, Archive for Mathematical Logic, vol. 30 (1991), pp. 377–403.CrossRefGoogle Scholar
[19] Rathjen, M., Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM, Archive for Mathematical Logic, vol. 33 (1994), pp. 35–55.CrossRefGoogle Scholar
[20] Rathjen, M., Proof theory of reflection, Annals of Pure and Applied Logic, vol. 68 (1994), pp. 181–224.CrossRefGoogle Scholar
[21] Schlüter, A., Zur Mengenexistenz in formalen Theorien der Mengenlehre, Ph.D. thesis, Münster, 1994.Google Scholar
[22] Schlüter, A., Provability in set theories with reflection, preprint Stanford, 1995.Google Scholar
[23] Schütte, K., Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik, Archive for Mathematical Logic, vol. 67 (1964), pp. 45–60.CrossRefGoogle Scholar
[24] Schütte, K., Predicative well-orderings, Formal Systems and Recursive Functions (Crossley, and Dummett, , editors), North-Holland, 1965, pp. 176–184.Google Scholar
[25] Schütte, K., Proof Theory, Springer-Verlag, 1977.CrossRefGoogle Scholar
[26] Takeuti, G., Proof Theory, North-Holland, 1975.Google Scholar
[27] Weiermann, A., How to characterize provably total functions by local predicativity, to appear in Journal of Symbolic Logic .Google Scholar