The Operational Perspective: Three Routes

Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)


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.


Proof Theory Truth Predicate Substitution Rule Transfinite Induction Induction Axiom 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



I wish to thank Ulrik Buchholtz, Gerhard Jäger, Dieter Probst, Michael Rathjen, and Thomas Strahm for their helpful comments on a draft of this article.


  1. 1.
    P. Aczel, Describing ordinals using functionals of transfinite type. J. Symbolic Logic 37, 35–47 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 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–9Google Scholar
  3. 3.
    J. Avigad, On the relationship between ATR\(_{0}\) and \(\widehat{ID}_{<\omega }\), J. Symbolic Logic 61, 768–779 (1996)Google Scholar
  4. 4.
    H. Bachmann, Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen. Vierteljschr. Naturforsch. Ges. Zürich 95, 115–147 (1950)MathSciNetzbMATHGoogle Scholar
  5. 5.
    M.J. Beeson, Foundations of Constructive Mathematics. Metamathematical Studies (Springer, Berlin, 1985)Google Scholar
  6. 6.
    M.J. Beeson, Toward a computation system based on set theory. Theor. Comput. Sci. 60, 297–340 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    E. Bishop, Foundations of Constructive Analysis (McGraw Hill, New York, 1967)zbMATHGoogle Scholar
  8. 8.
    E. Bishop, D. Bridges, Constructive Analysis (Springer, Berlin, 1985)CrossRefzbMATHGoogle Scholar
  9. 9.
    U. Buchholtz, Unfolding of Systems of Inductive Definitions, Ph.D. thesis, Stanford University (2013).
  10. 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)Google Scholar
  11. 11.
    A. Cantini, Extending constructive operational set theory by impredicative principles. Math. Logic Q. 57, 299–322 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 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–83Google Scholar
  13. 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–240Google Scholar
  14. 14.
    A. Church, A set of postulates for the foundation of logic. Ann. Math. 33, 346–366 (1932)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    A. Church, A set of postulates for the foundation of logic (second paper). Ann. Math. 34, 839–864 (1933)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    S. Eberhard, T. Strahm, Towards the unfolding of feasible arithmetic (Abstract). Bull. Symbolic Logic 18, 474–475 (2012)Google Scholar
  17. 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)Google Scholar
  18. 18.
    F.B. Fitch, The system C\(\Delta \) of combinatory logic. J. Symbolic Logic 28, 87–97 (1963)MathSciNetCrossRefGoogle Scholar
  19. 19.
    S. Feferman, Systems of predicative analysis. J. Symbolic Logic 29, 1–30 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 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–135CrossRefGoogle Scholar
  21. 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–233Google Scholar
  22. 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–32Google Scholar
  23. 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–139Google Scholar
  24. 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–971CrossRefGoogle Scholar
  25. 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–224Google Scholar
  26. 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–93Google Scholar
  27. 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–89Google Scholar
  28. 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–283Google Scholar
  29. 29.
    S. Feferman, Reflecting on incompleteness. J. Symbolic Logic 56, 1–49 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 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–298Google Scholar
  31. 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–22Google Scholar
  32. 32.
    S. Feferman, In the Light of Logic (Oxford University Press, New York, 1998)zbMATHGoogle Scholar
  33. 33.
    S. Feferman, Notes on operational set theory I. Generalizations of “small” large cardinals and admissible set theory (2001).
  34. 34.
    S. Feferman, Operational set theory and small large cardinals. Inf. Computat. 207, 971–979 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    S. Feferman, How a little bit goes a long way: predicative foundations of analysis (2013).
  36. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    S. Feferman, G. Jäger, Systems of explicit mathematics with non-constructive \(\mu \)-operator I. Ann. Pure Appl. Logic 65, 243–263 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    S. Feferman, G. Jäger, Systems of explicit mathematics with non-constructive \(\mu \)-operator II. Ann. Pure Appl. Logic 79, 37–52 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  39. 39.
    S. Feferman, T. Strahm, The unfolding of non-finitist arithmetic. Ann. Pure Appl. Logic 104, 75–96 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    S. Feferman, T. Strahm, The unfolding of finitist arithmetic. Rev. Symbolic Logic 3, 665–689 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  41. 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–230CrossRefGoogle Scholar
  42. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  43. 43.
    T. Glass, T. Strahm, Systems of explicit mathematics with non-constructive \(\mu \)-operator and join. Ann. Pure Appl. Logic 82, 193–219 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  44. 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–187Google Scholar
  45. 45.
    K. Gödel, in Collected Works, Vol. II. Publications 1938–1974, ed. by S. Feferman, et al. (Oxford University Press, New York, 1990)Google Scholar
  46. 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)CrossRefzbMATHGoogle Scholar
  47. 47.
    G. Jäger, The strength of admissibility without foundation. J. Symbolic Logic 49, 867–879 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    G. Jäger, Theories for admissible sets: a unifying approach to proof theory, in Studies in Proof Theory, vol. 2 (Bibliopolis, Naples, 1986)Google Scholar
  49. 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–128Google Scholar
  50. 50.
    G. Jäger, On Feferman’s operational set theory OST. Ann. Pure Appl. Logic 150, 19–39 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  51. 51.
    G. Jäger, Full operational set theory with unbounded existential quantification and power set. Ann. Pure Appl. Logic 160, 33–52 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  52. 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–96Google Scholar
  53. 53.
    G. Jäger, Operational closure and stability. Ann. Pure Appl. Logic 164, 813–821 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  54. 54.
    G. Jäger, Relativizing Operational Set Theory (2015). (In preparation)Google Scholar
  55. 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–92Google Scholar
  56. 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–314Google Scholar
  57. 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–28Google Scholar
  58. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  59. 59.
    G. Jäger, T. Strahm, Totality in applicative theories. Ann. Pure Appl. Logic 74, 105–120 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  60. 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–292Google Scholar
  61. 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–324Google Scholar
  62. 62.
    G. Kreisel, Mathematical logic, in Lectures on Modern Mathematics, vol. III ed. by T.L. Saaty (Wiley, New York, 1965), pp. 95–195Google Scholar
  63. 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–516Google Scholar
  64. 64.
    S. Kripke, Outline of a theory of truth. J. Philos. 72, 690–716 (1975)CrossRefzbMATHGoogle Scholar
  65. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  66. 66.
    A.R.D. Mathias, The strength of Mac Lane set theory. Ann. Pure Appl. Logic 110, 107–234 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  67. 67.
    L.W. Miller, Normal functions and constructive ordinal notations. J. Symbolic Logic 41, 439–459 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  68. 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–335CrossRefGoogle Scholar
  69. 69.
    M. Rathjen, Monotone inductive definitions in explicit mathematics, J. Symbolic Logic 61, 125–146 (1996)Google Scholar
  70. 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)Google Scholar
  71. 71.
    M. Rathjen, Relativized ordinal analysis, The case of Power Kripke-Platek set theory. Ann. Pure Appl. Logic 165, 316–339 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  72. 72.
    M. Rathjen, Power Kripke-Platek and the Axiom of Choice (2014).
  73. 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–381Google Scholar
  74. 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)Google Scholar
  75. 75.
    K. Sato, R. Zumbrunnen, A New Model Construction by Making a Detour via Intuitionistic Theories I. Operational Set Theory Without Choice is \(\Pi \) \(_{1}\) Equivalent to KP (2014).
  76. 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)MathSciNetCrossRefzbMATHGoogle Scholar
  77. 77.
    S.G. Simpson, Subsystems of second order arithmetic, in Perspectives in Logic, (Springer, Berlin, 1988) 2nd edn. 2009Google Scholar
  78. 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)Google Scholar
  79. 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–127Google Scholar
  80. 80.
    S. Takahashi, Monotone inductive definitions in a constructive theory of functions and classes. Ann. Pure Appl. Logic 42, 255–297 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  81. 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–42Google Scholar
  82. 82.
    W.W. Tait, The Provenance of Pure Reason (Oxford University Press, New York, 2005)zbMATHGoogle Scholar
  83. 83.
    J. van Heijenoort (ed.), From Frege to Gödel, A source book in mathematical logic (Harvard Univ. Press, Cambridge, 1967)Google Scholar
  84. 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–413Google Scholar
  85. 85.
    H. Weyl, Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis (Veit, Leipzig, 1918)Google Scholar
  86. 86.
    E. Zermelo, Untersuchungen über die Grundlagen der Mengenlehre I, Mathematische Annalen 65, 261–281 (1908). English translation in van Heijenoort 1967, pp. 199–215Google Scholar
  87. 87.
    R. Zumbrunnen, Contributions to Operational Set Theory, Ph.D. thesis, University of Bern (2013).

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of Mathematics Stanford UniversityStanfordUSA

Personalised recommendations