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

The Operational Perspective: Three Routes

verfasst von : Solomon Feferman

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

Let me begin with a few personal words of appreciation, since Gerhard Jäger is one of my most valued friends and long time collaborators.

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 Intuitionistic Decision Procedures Since Gentzen
Nächstes Kapitel Some Remarks on the Proof-Theory and the Semantics of Infinitary Modal Logic
Fußnoten
1
Let me also take this opportunity to thank Thomas Strahm and Thomas Studer for organizing the December 2014 meeting in honor of Gerhard Jäger, and for arranging for me to participate via Skype since I was unable to attend in person.
 
2
There are several possible formulations of the definition by cases operator. In the one originally taken in [23], sometimes called definition by cases on V, this takes the form d xyuv = (x if \(u=v\), else y). However, when added to the axioms for k and s, extensionality is inconsistent for operations. More restrictive versions have subsequently been used, mainly definition by cases on the natural numbers, allowing both extensionality and totality of operations; cf. [59].
 
3
First steps in that direction had already been made in [19] via the system IR. For subsequent explorations cf. [20, 22, 26].
 
4
In [25] I also examined T\(_{0}\) within intuitionistic logic.
 
5
The scheme ECA can be finitely axiomatized by adding constants for the identity relation, the first-order logical operations for negation, conjunction, existential quantification, and inverse image of a class under an operation.
 
6
There is a difference in terminology, though: Jäger used ‘types’ for our classes.
 
7
In certain subsystems of T\(_{1}\) with restricted induction we need to add to the (\(\upmu )\) axiom that if \({\upmu }f \in \) N then\( f \in \) (N \(\rightarrow \) N).
 
8
Parts of T\(_{0}\) relate to Aczel’s Frege structures and Martin-Löf’s constructive theory of types; cf. for example, Beeson [5], Chaps. XI and XVII. But neither of these approaches goes on to the adjunction of non-constructive functional operators like \(\mu \) (or E\(_{0})\) and E\(_{1}\).
 
9
For the proof theory of systems of explicit mathematics with \({\mathbf {E}}_{1}\) see Jäger and Strahm [60] and Jäger and Probst [58].
 
10
Then Jäger [47] and Avigad [3] showed that they are of the same proof-theoretical strength, by proof-theoretical methods, the first via theories of iterated admissible sets without foundation and the second via fixed point theories.
 
11
In Sect. 4 below I conjecture that the unfolding of a suitable subsystem of T\(_{0}\) is equivalent in strength to predicative analysis.
 
12
Recently, Sato [74] has shown how to establish the reduction of \(\Delta ^{1}_{2}\) − CA + BI to T\(_{0}\) without going through the ordinal notation system for \(\kappa \).
 
13
Another interesting group of questions concerns the strength over T\(_{0}\) (or its restricted version \(\text {T}_0{\upharpoonright }\)) of the principle MID that I introduced in [27]. That expresses that if f is any monotone operation from classes to classes then f has a least fixed point. Takahashi [80] showed that \(\text {T}_0\) + MID is interpretable in \(\Pi ^1_2\) − CA + BI, and then Rathjen [69] showed that it is much stronger than T\(_{0}\). Next, exact strength of \(\text {T}_0{\upharpoonright }\) + MID was determined by Glass et al. [42]. A series of further results by Rathjen for the strength of \(\text {T}_0\) + MID and \(\text {T}_0\) + UMID, where UMID is a natural uniform version of the principle, are surveyed in the paper Rathjen [70].
 
14
To explain some anomalies of the dates of subsequent work on this subject, it should be noted that my 2009 paper was submitted to the journal Information and Control in December 2006 and in revised form in April 2008. In the meantime, Jäger [50] had appeared and so I could refer to it in that revised version.
 
15
Further important work is contained in Zumbrunnen [87] and Sato and Zumbrunnen [75]. Constructive operational theories of sets have been treated by Cantini and Crosilla [12, 13] and Cantini [11].
 
16
Rathjen [71] uses (Pow(P)) for our formulation in the language of KP as well, in order to distinguish it from the usual power set axiom formulated without the additional constant. It would have been better to do that in [34], but not having done so I here follow the notation from there.
 
17
An earlier such result for the system with a restricted form of set induction is due to Mathias [66].
 
18
However, I did say that I had not checked the details. In fact, I hadn’t thought them through at all.
 
19
Cf. Footnote 2.
 
20
Since referred to as KF in the literature.
 
21
This follows the proposed formulation of U(NFA) via a truth predicate in Feferman [31, p. 14].
 
22
Ulrik Buchholtz originally thought that \(\uppsi (\Gamma _{\Omega +1})\) is the same as the ordinal H(1) of Bachmann [4]. This seemed to be supported by Aczel [1] who wrote (p. 36) that H(1) may have proof theoretical significance related to those of the ordinals \(\varepsilon \), \(\Gamma _{0}\) and \(\upvarphi \varepsilon _{\Omega +1}\)0. And Miller [67, p. 451] had conjectured that “H(1) [is] the proof-theoretic ordinal of ID\(_{1}\)* which is related to ID\(_{1}\) as predicative analysis ID\(_{0}\)* is to first-order arithmetic ID\(_{0}\).” However, Wilfried Buchholz recently found that the above representation of H(1) in terms of the \(\uppsi \) function is incorrect. This suggests one should revisit the bases of Aczel’s and Miller’s conjectures.
 
23
Alternatively, one can of course work with the formulation of explicit mathematics in terms of the representation relation \(\mathfrak {R}(x\), X).
 
24
This would provide another answer to the question of finding a system of explicit mathematics of the same strength as predicative analysis.
 
Literatur
1.
2.
P. Aczel, W. Richter, in Inductive definitions and analogues of large cardinals, Conference in Mathematical Logic, London ’70, Lecture Notes in Mathematics, vol. 255, ed by W. Hodges (1972), pp. 1–9
3.
J. Avigad, On the relationship between ATR\(_{0}\) and \(\widehat{ID}_{<\omega }\), J. Symbolic Logic 61, 768–779 (1996)
4.
H. Bachmann, Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen. Vierteljschr. Naturforsch. Ges. Zürich 95, 115–147 (1950)MathSciNetMATH
5.
M.J. Beeson, Foundations of Constructive Mathematics. Metamathematical Studies (Springer, Berlin, 1985)
6.
7.
E. Bishop, Foundations of Constructive Analysis (McGraw Hill, New York, 1967)MATH
8.
9.
10.
U. Buchholtz, G. Jäger, T. Strahm, Theories of Proof-Theoretic Strength \(\psi (\Gamma \) \(_{\Omega +1})\) (2014). In: Probst, D. and Schuster, P. Concepts of Proof in Mathematics, Philosophy, and ComputerScience. De Gruyter (In Press)
11.
12.
A. Cantini, L. Crosilla (2008), Constructive set theory with operations, in Logic Colloquium ed. by A. Andretta et al., Lecture Notes in Logic, vol. 29 (2004), pp. 47–83
13.
A. Cantini, L. Crosilla, Elementary constructive operational set theory, in Ways of Proof Theory, ed. by R. Schindler (Ontos Verlag, Frankfurt, 2010), pp. 199–240
14.
15.
16.
S. Eberhard, T. Strahm, Towards the unfolding of feasible arithmetic (Abstract). Bull. Symbolic Logic 18, 474–475 (2012)
17.
S. Eberhard, T. Strahm, Unfolding feasible arithmetic and weak truth, in Unifying the Philosopy of Truth, ed. by T. Achourioti, et al. (Springer, Berlin, 2015)
18.
19.
20.
S. Feferman, Autonomous transfinite progressions and the extent of predicative mathematics, in Logic, Methodology, and Philosophy of Science III, ed. by B. van Rootselaar, J.F. Staal (North-Holland, Amsterdam, 1968), pp. 121–135CrossRef
21.
S. Feferman, Ordinals and functionals in proof theory, in Actes du Congrès International des Mathématiciens (Nice) 1970, vol. 1 (Gauthier-Villars, Paris, (1971) pp. 229–233
22.
S. Feferman, Predicatively reducible systems of set theory, in Axiomatic Set Theory ed. by D. Scott, Proceedings of Symposia in Pure Mathematics. XIII, Part 2 (American. Mathematical Society, Providence, 1974), pp. 11–32
23.
S. Feferman, A language and axioms for explicit mathematics, in Algebra and Logic ed. by J. Crossley, Lecture Notes in Mathematics, vol. 450 (1975), pp. 87–139
24.
S. Feferman, Theories of finite type related to mathematical practice, in Handbook of Mathematical Logic, ed. by J. Barwise (North-Holland, Amsterdam, 1977), pp. 913–971CrossRef
25.
S. Feferman, Constructive theories of functions and classes, in Logic Colloquium ’78, ed. by M. Boffa, et al. (North-Holland, Amsterdam, 1979), pp. 159–224
26.
S. Feferman, A more perspicuous formal system for predicativity, in Konstruktionen versus Positionen I, ed. by K. Lorenz (Walter de Gruyter, Berlin, 1979), pp. 68–93
27.
S. Feferman, Monotone inductive definitions, in The L. E. J. Brouwer Centenary Symposium, ed. by A.S. Troelstra, D. van Dalen (North-Holland, Amsterdam, 1982), pp. 77–89
28.
S. Feferman, Weyl vindicated: Das Kontinuum 70 years later, in Temi e prospettive della logica e della filosofia della scienza contemporanee, vol. I (CLUEB, Bologna, 1988), pp. 59–93; reprinted in Feferman [32], pp. 249–283
29.
30.
S. Feferman, Why a little bit goes a long way: logical foundations of scientifically applicable mathematics, in PSA 1992, vol. II (1993), pp. 442–455; reprinted in Feferman [32], pp. 284–298
31.
S. Feferman, Gödel’s program for new axioms: why, where, how and what?, in Gödel ’96, ed. by P. Hájek, Lecture Notes in Logic vol. 6 (1996), pp. 3–22
32.
S. Feferman, In the Light of Logic (Oxford University Press, New York, 1998)MATH
33.
34.
35.
36.
S. Feferman, G. Jäger, Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis. J. Symbolic Logic 48, 63–70 (1983)MathSciNetCrossRefMATH
37.
S. Feferman, G. Jäger, Systems of explicit mathematics with non-constructive \(\mu \)-operator I. Ann. Pure Appl. Logic 65, 243–263 (1993)MathSciNetCrossRefMATH
38.
S. Feferman, G. Jäger, Systems of explicit mathematics with non-constructive \(\mu \)-operator II. Ann. Pure Appl. Logic 79, 37–52 (1996)MathSciNetCrossRefMATH
39.
40.
41.
H. Friedman, K. McAloon, S.G. Simpson, A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis, in Patras Logic Symposion, ed. by G. Metakides (North-Holland, Amsterdam, 1982), pp. 197–230CrossRef
42.
T. Glass, M. Rathjen, A. Schlüter, On the proof-theoretic strength of monotone induction in explicit mathematics. Ann. Pure Appl. Logic 85, 1–46 (1997)MathSciNetCrossRefMATH
43.
T. Glass, T. Strahm, Systems of explicit mathematics with non-constructive \(\mu \)-operator and join. Ann. Pure Appl. Logic 82, 193–219 (1996)MathSciNetCrossRefMATH
44.
K. Gödel, What is Cantor’s continuum problem? Amer. Math. Monthly 54, 515–525 (1947); errata 55, 151; reprinted in Gödel (1990), 176–187
45.
K. Gödel, in Collected Works, Vol. II. Publications 1938–1974, ed. by S. Feferman, et al. (Oxford University Press, New York, 1990)
46.
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
47.
48.
G. Jäger, Theories for admissible sets: a unifying approach to proof theory, in Studies in Proof Theory, vol. 2 (Bibliopolis, Naples, 1986)
49.
G. Jäger, Induction in the elementary theory of types and names, in Computer Science Logic ’87, ed. by E. Börger, et al., Lecture Notes in Computer Science, vol. 329 (1988), pp. 118–128
50.
51.
G. Jäger, Full operational set theory with unbounded existential quantification and power set. Ann. Pure Appl. Logic 160, 33–52 (2009)MathSciNetCrossRefMATH
52.
G. Jäger, Operations, sets and classes, in Logic, Methodology and Philosophy of Science: Proceedings of the Thirteenth International Congress, ed. by C. Glymour et al. (College Publications, London, 2009), pp. 74–96
53.
54.
G. Jäger, Relativizing Operational Set Theory (2015). (In preparation)
55.
G. Jäger, R. Kahle, T. Strahm, On applicative theories, in Logic and Foundations of Mathematics, ed. by A. Cantini, et al. (Kluwer, Dordrecht, 1999), pp. 83–92
56.
G. Jäger, J. Krähenbuhl, \(\Sigma \) \(^{1}\) \(_{1 }\)choice in a theory of sets and classes, in Ways of Proof, ed. by R. Schindler (Ontos Verlag, Frankfurt, 2010), pp. 283–314
57.
G. Jäger, W. Pohlers, Eine beweistheoretische Untersuchung von \(\Delta \) \(^{1}\) \(_{2}\)-CA + BI und verwandter Systeme in (Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse (1982), pp. 1–28
58.
G. Jäger, D. Probst, The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories. Ann. Pure Appl. Logic 162, 647–660 (2011)MathSciNetCrossRefMATH
59.
60.
G. Jäger, T. Strahm, The proof-theoretic analysis of the Suslin operator in applicative theories, in Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, ed. by W. Sieg, R. Sommer, C. Talcott (AK Peters Ltd, Natick, MA, 2002), pp. 270–292
61.
G. Jäger, R. Zumbrunnen, About the strength of operational regularity, in Logic, Construction, Computation, ed. by U. Berger, et al. (Ontos Verlag, Frankfurt, 2012), pp. 305–324
62.
G. Kreisel, Mathematical logic, in Lectures on Modern Mathematics, vol. III ed. by T.L. Saaty (Wiley, New York, 1965), pp. 95–195
63.
G. Kreisel, Principles of proof and ordinals implicit in given concepts, in Intuitionism and Proof Theory, ed. by A. Kino, et al. (North-Holland, Amsterdam, 1970), pp. 489–516
64.
65.
M. Marzetta, T. Strahm, The \(\mu \) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals. Arch. Math. Logic 37, 391–413 (1988)MathSciNetCrossRefMATH
66.
67.
68.
W. Pohlers, Subsystems of set theory and second order number theory, in Handbook of Proof Theory, ed. by S. Buss (North-Holland, Amsterdam, 1998), pp. 209–335CrossRef
69.
M. Rathjen, Monotone inductive definitions in explicit mathematics, J. Symbolic Logic 61, 125–146 (1996)
70.
M. Rathjen, Explicit mathematics with monotone inductive definitions: a survey, in Reflections on the Foundations of Mathematics, ed. by W. Sieg, et al. (1998), pp. 329–346. Second printing, Lecture Notes in Logic, vol. 15 (2002)
71.
M. Rathjen, Relativized ordinal analysis, The case of Power Kripke-Platek set theory. Ann. Pure Appl. Logic 165, 316–339 (2014)MathSciNetCrossRefMATH
72.
73.
W. Richter, P. Aczel, Inductive definitions and reflecting properties of admissible ordinals, in Generalized Recursion Theory, ed. by J.E. Fenstad, P.G. Hinman (North-Holland, Amsterdam, 1974), pp. 301–381
74.
K. Sato, A new model construction by making a detour via intuitionistic theories II, in Interpretability lower bound of Feferman’s Explicit Mathematics T\(_{0}\) (t.a.) (2014)
75.
76.
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
77.
S.G. Simpson, Subsystems of second order arithmetic, in Perspectives in Logic, (Springer, Berlin, 1988) 2nd edn. 2009
78.
S.G. Simpson, Predicativity: the outer limits, in Reflections on the Foundations of Mathematics ed. by W. Sieg, et al. (1998), pp. 130–136; 2nd printing, Lecture Notes in Logic vol. 15 (2002)
79.
S.G. Simpson, The Gödel hierarchy and reverse mathematics, in Kurt Gödel. Essays for his Centennial, ed. by S. Feferman, et al. Lecture Notes in Logic, vol. 33 (2010) pp. 109–127
80.
S. Takahashi, Monotone inductive definitions in a constructive theory of functions and classes. Ann. Pure Appl. Logic 42, 255–297 (1989)MathSciNetCrossRefMATH
81.
W.W. Tait, Constructive reasoning, in Logic, Methodology and Philosophy of Science III (North-Holland, Amsterdam, 1981), pp. 185–199; reprinted in Tait [82], pp. 21–42
82.
W.W. Tait, The Provenance of Pure Reason (Oxford University Press, New York, 2005)MATH
83.
J. van Heijenoort (ed.), From Frege to Gödel, A source book in mathematical logic (Harvard Univ. Press, Cambridge, 1967)
84.
J. von Neumann, Eine Axiomatisierung derMengenlehre, J. für die reine und angewandte Mathematik 154, 219–240 (1925); English translation in van Heijenoort [83], pp. 393–413
85.
H. Weyl, Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis (Veit, Leipzig, 1918)
86.
E. Zermelo, Untersuchungen über die Grundlagen der Mengenlehre I, Mathematische Annalen 65, 261–281 (1908). English translation in van Heijenoort 1967, pp. 199–215
87.
Metadaten
Titel
The Operational Perspective: Three Routes
verfasst von
Solomon Feferman
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_7