Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Survey on Ordinal Notations Around the Bachmann-Howard Ordinal Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

From Subsystems of Analysis to Subsystems of Set Theory

verfasst von : Wolfram Pohlers

Erschienen in: Advances in Proof Theory

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

To honor a part of Gerhard Jäger’s contributions to proof theory we give a non technical, personally biased account of how we got from the proof theory of subsystems of Analysis to the proof theory of subsystems of set theory.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Some Remarks on the Proof-Theory and the Semantics of Infinitary Modal Logic
Nächstes Kapitel Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut
Fußnoten
1
In case that \(\phi \) is a sentence not containing free variables, the calculus https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-29198-7_9/328363_1_En_9_IEq33_HTML.gif is just a verification of \(\phi \) in the structure \(\mathbb {N}\). Details about semi–formal systems in general and the verification calculus https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-29198-7_9/328363_1_En_9_IEq36_HTML.gif together with a proof of Theorem 2.1 can be found in [34].
 
2
This formulation is quite different from Gentzen’s approach who did not use infinitary logic. However, the idea of the proof is the same. In our formulation Gentzen’s result says that \(\omega ^\alpha \) is an upper bound for the order–type of \(\prec \). A result that sufficed to obtain the proof theoretic ordinal for Peano Arithmetic. Already Schütte improved Gentzen’s result in showing that the order–type of \(\prec \) is \(\le \omega \mathrel {\cdot }\alpha \) (cf. [38] Theorem 23.1).
 
3
I concentrate on the computation of upper bounds, since only there meta–mathematical methods are needed. Lower bounds are obtained by exhausting the mathematical power of an axiom system.
 
4
Again the formulation deviates considerably from Gentzen’s original theorem. He did not use infinitary derivations but obtained the result by a complicated assignment of ordinals to the nodes in a finite derivation.
 
5
In Sect. 3.3 I will briefly comment on Hilbert’s Programme.
 
6
There are variations of the comprehension scheme, e.g., choice schemata, and even stronger systems such as the system \(\textsf {ATR}_0\) of arithmetical transfinite recursion (cf. [39]) which can also be embedded into Ramified Analysis but this is inessential for our story.
 
7
Actually the system in my dissertation was weaker than Takeuti’s. The ordinal of the full system was not available in \(\Sigma \).
 
8
When formulating such rules I tacitly assume \(\alpha <\beta \). I mention the side formula \(\chi \) just to be not too severely cheating. A rigid definition is preferably done in the framework of some form of sequent calculus.
 
9
This is my naming to emphasize the relationship to the hyperjump operation.
 
10
Der Physiker verlangt gerade von einer Theorie, dass ohne die Heranziehung von anderweitigen Bedingungen aus den Naturgesetzen oder Hypothesen die besonderen Sätze allein durch Schlüsse, also auf Grund eines reinen Formelspiels abgeleitet werden. Nur gewisse Kombinationen und Folgerungen der physikalischen Gesetze können durch Experimente kontrolliert werden—so wie in meiner Beweistheorie nur die realen Aussagen unmittelbar einer Verifikation fähig sind. (Cited from [18]).
 
11
Here it is necessary to allow additional number parameters in \(\Pi ^0_2\)–sentences. A more elaborated discussion on the interaction of Hilbert’s programme and ordinal analysis will appear in [33].
 
12
Das Operieren mit dem Unendlichen kann nur durch das Endliche gesichert werden [17].
 
13
This, of course, does not mean that these rules are dubious. Contrarily I think that the power of these ingenious rules, especially in respect to second order systems, should be more extensively studied.
 
14
This is probably the right place to mention that Moschovakis’ book [25] was of central importance for the proof theoretic study of inductive definition.
 
15
For a rigid proof cf. [32].
 
16
A bound that in general is useless for proof theoretic studies.
 
17
In former publications I sometimes talked about “virtual ordinals”.
 
18
To find the subsets of the class of ordinals with the adequate gaps is actually the most challenging task in the ordinal analysis of strong axiom systems.
 
19
A proof of this theorem (in a more modern form working already with operator controlled derivations which will be mentioned below) is in [32] Lemma 9.4.5.
 
20
Which says in its simplest form that for every \(\Sigma ^1_1\)–definable set M of well-orderings there is an ordinal \(\xi <\omega ^{ck}_1\) that bounds the order–types of the well–orderings in M. A fact which actually is a consequence of the Boundedness Theorem 2.2. Cf. [2].
 
21
During the preparation of this article I received a preprint by Kentaro Sato “A new model construction by making a detour via intutionistic theories. II: Interpretability lower bounds for Feferman’s explicit mathematics \(T_0\)” in which he establishes the equivalence without use of ordinal analysis.
 
Literatur
1.
J. Barwise, Admissible Sets and Structures, Perspectives in Mathematical Logic (Springer, Berlin, 1975)CrossRefMATH
2.
A. Beckmann, W. Pohlers, Application of cut-free infinitary derivations to generalized recursion theory. Ann. Pure Appl. Logic 94, 1–19 (1998)MathSciNetCrossRefMATH
3.
B. Blankertz, Beweistheoretischen Techniken zur Bestimmung von \(\Pi ^0_2\)–Skolem Funktionen, Dissertation, Westfälische Wilhelms-Universität, Münster, 1997
4.
B. Blankertz, A. Weiermann, How to Characterize Provably Total Functions by the Buchholz Operator Method, vol. 6, Lecture Notes in Logic (Springer, Heidelberg, 1996)MATH
5.
W. Buchholz, The \({\Omega }_{\mu +1}\)-rule, in Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, vol. 897, Lecture Notes in Mathematics, ed. by W. Buchholz, et al. (Springer, Heidelberg/New York, 1981), pp. 188–233CrossRef
6.
W. Buchholz, A simplified version of local predicativity, in Proof Theory, eds. by P. Aczel et al. (Cambridge University Press, Cambridge, 1992), pp. 115–147
7.
8.
W. Buchholz, E.A. Cichon, A. Weiermann, A uniform approach to fundamental sequences and hierarchies. Math. Logic Q. 40, 273–286 (1994)MathSciNetCrossRefMATH
9.
W. Buchholz, S. Feferman, W. Pohlers, W. Sieg (eds.), Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, vol. 897, Lecture Notes in Mathematics (Springer, Heidelberg/New York, 1981)MATH
10.
W. Buchholz, K. Schütte, Proof Theory of Impredicative Subsystems of Analysis, in Studies in Proof Theory: Monographs, vol. 2 (Bibliopolis, Naples, 1988)
11.
12.
S. Feferman, Formal theories for transfinite iteration of generalized inductive definitions and some subsystems of analysis, in Intuitionism and Proof Theory, Studies in Logic and the Foundations of Mathematics, ed. by A. Kino, et al. (North-Holland Publishing Company, Amsterdam, 1970), pp. 303–326
13.
S. Feferman, Predicatively reducible systems of set theory, in Axiomatic Set Theory, vol. 2, ed. by D.S. Scott, T.J. Jech, Proceedings of Symposia in Pure Mathematics, vol. 13, American Mathematical Society, Providence (1974), pp. 11–32
14.
15.
G. Gentzen, Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Math. Ann. 119, 140–161 (1943)MathSciNetCrossRefMATH
16.
17.
18.
D. Hilbert, Die Grundlagen, der Mathematik. Vortrag gehalten auf Einladung des Mathema-tischen Seminars im Juli, in Hamburg, Hamburger Mathematische Einzelschriften, vol. 5. Heft 1928, 1–21 (1927)
19.
20.
G. Jäger, Die konstruktible Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Mengenlehre und Analysis, Dissertation, Ludwig-Maximilians-Universität, Munich, 1979
21.
22.
G. Jäger, A well ordering proof for Feferman’s theory T\(_0\). Archiv für Mathematische Logik und Grundlagenforschung 23, 65–77 (1983)CrossRefMATH
23.
G. Jäger, Theories for Admissible Sets: A Unifying Approach to Proof Theory, vol. 2, Studies in Proof Theory, Lecture Notes (Bibliopolis, Naples, 1986)
24.
G. Jäger, W. Pohlers, Eine beweistheoretische Untersuchung von (\({\Delta }^1_2-{\rm CA})+({\rm BI})\) und verwandter Systeme, Bayerische Akademie der Wissenschaften, Sitzungsberichte 1982 (1983), pp. 1–28
25.
Y.N. Moschovakis, Elementary Induction on Abstract Structures, vol. 77, Studies in Logic and the Foundations of Mathematics (North-Holland Publishing Company, Amsterdam, 1974)MATH
26.
27.
W. Pohlers, An upper bound for the provability of transfinite induction, in \(\models \) ISILC Proof Theory Symposium, vol. 500, Lecture Notes in Mathematics, ed. by J. Diller, G.H. Müller (Springer, Heidelberg/New York, 1975), pp. 271–289
28.
W. Pohlers, Ordinals connected with formal theories for transfinitely iterated inductive definitions. J. Symb. Logic 43, 161–182 (1978)MathSciNetCrossRefMATH
29.
W. Pohlers, Cut-elimination for impredicative infinitary systems I. Ordinal analysis for ID\(_1\), Archiv für Mathematische Logik und Grundlagenforschung 21, 113–129 (1981)
30.
W. Pohlers, Proof-theoretical analysis of ID\(_{\nu }\) by the method of local predicativity, in Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, vol. 897, Lecture Notes in Mathematics ed. by W. Buchholz et al. (Springer, Heidelberg/New York, 1981), pp. 261–357
31.
W. Pohlers, Cut elimination for impredicative infinitary systems II. Ordinal analysis for iterated inductive definitions. Archiv für Mathematische Logik und Grundlagenforschung 22, 69–87 (1982)MathSciNetCrossRefMATH
32.
W. Pohlers, Proof Theory: The First Step into Impredicativity, Universitext (Springer, Berlin/Heidelberg/New York, 2009)MATH
33.
W. Pohlers, Hilbert’s programme and ordinal analysis, in Concepts of Proof in Mathematics, Philosophy, and Computer Science, ed. by Dieter Probst, Peter Schuster (DeGryuter, 2016), p. 32
34.
W. Pohlers, Semi-formal calculi and their applications, in Gentzen’s Centenary: The Quest for Consistency,ed. by R. Kahle, M. Rathjen (Springer, New York, 2015), pp. 195–232
35.
M. Rathjen, Eine Ordinalzahlanalyse der \({\Pi }_3\)-Reflexion (Westfälische Wilhelms-Universität, Münster, Habilitationsschrift, 1992)
36.
37.
K. Schütte, Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik. Archiv für Mathematische Logik und Grundlagenforschung 7, 45–60 (1965)MathSciNetCrossRefMATH
38.
K. Schütte, Proof Theory, Grundlehren der Mathematischen Wissenschaften, vol. 225 (Springer, Heidelberg/New York, 1977)
39.
S.G. Simpson, Subsystems of Second Order Arithmetic (Springer, Berlin/Heidelberg/New York, 1999)CrossRefMATH
40.
J.-C. Stegert, Ordinal proof theory of Kripke-Platek set theory augmented by strong reflection principles, Ph.D. thesis, Westfälische Wilhelms-Universität, Münster, 2011
41.
Metadaten
Titel
From Subsystems of Analysis to Subsystems of Set Theory
verfasst von
Wolfram Pohlers
Copyright-Jahr
2016
Buch
Advances in Proof Theory

Print ISBN: 978-3-319-29196-3

Electronic ISBN: 978-3-319-29198-7

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-29198-7_9