Unfolding Schematic Systems

  • Thomas Strahm
Part of the Outstanding Contributions to Logic book series (OCTR, volume 13)


The notion of unfolding a schematic formal system was introduced by Feferman in 1996 in order to answer the following question: Given a schematic system \(\mathsf {S}\), which operations and predicates, and which principles concerning them, ought to be accepted if one has accepted \(\mathsf {S}\)? After a short summary of precursors of the unfolding program, we survey the unfolding procedure and discuss the main results obtained for various schematic systems S, including non-finitist arithmetic, finitist arithmetic, feasible arithmetic, and theories of inductive definitions.


Schematic systems Unfolding Finitist arithmetic Non-finitist arithmetic Feasible arithmetic Inductive definitions 

2010 Mathematics Subject Classification

03F03 03F30 03D75 


  1. 1.
    Beeson, M.J.: Foundations of Constructive Mathematics: Metamathematical Studies. Springer, Berlin (1985)CrossRefzbMATHGoogle Scholar
  2. 2.
    Buchholtz, U.: Unfolding of systems of inductive definitions. Ph.D. thesis, Stanford University (2013)Google Scholar
  3. 3.
    Buchholtz, U., Jäger, G., Strahm, T.: Theories of proof-theoretic strength \(\Psi (\Gamma _{\Omega +1})\). In: Probst, D., Schuster, P. (eds.) Concepts of Proof in Mathematics, Philosophy, and Computer Science of Ontos Mathematical Logic. vol. 6, pp. 115–140. De Gruyter (2016)Google Scholar
  4. 4.
    Clote, P.: Computation models and function algebras. In: Griffor, E. (ed.) Handbook of Computability Theory, pp. 589–681. Elsevier (1999)Google Scholar
  5. 5.
    Cobham, A.: The intrinsic computational difficulty of functions. In: Logic, Methodology and Philosophy of Science II, pp. 24–30. North Holland, Amsterdam (1965)Google Scholar
  6. 6.
    Eberhard, S.: Weak Applicative Theories, Truth, and Computational Complexity. Ph.D. thesis, Universität Bern (2013)Google Scholar
  7. 7.
    Eberhard, S.: A feasible theory of truth over combinatory algebra. Ann. Pure Appl. Log. 165(5), 1009–1033 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Eberhard, S., Strahm, T.: Weak theories of truth and explicit mathematics. In: Berger, U., Diener, H., Schuster, P., Seisenberger, M. (eds.) Logic, Construction, Computation, pp. 157–184. Ontos Verlag (2012)Google Scholar
  9. 9.
    Eberhard, S., Strahm, T.: Unfolding feasible arithmetic and weak truth. In: Achourioti, D., Galinon, H., Fujimoto, K., Martinez, J. (eds.) Unifying the Philosophy of Truth, pp. 153–167. Springer (2015)Google Scholar
  10. 10.
    Feferman, S.: Transfinite recursive progressions of axiomatic theories. J. Symb. Log. 27, 259–316 (1962)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Feferman, S.: Systems of predicative analysis. J. Symb. Log. 29(1), 1–30 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Feferman, S.: A language and axioms for explicit mathematics. In: Crossley, J. (ed.) Algebra and Logic of Lecture Notes in Mathematics, vol. 450, pp. 87–139. Springer (1975)Google Scholar
  13. 13.
    Feferman, S.: A more perspicuous system for predicativity. In: Konstruktionen vs. Positionen I. de Gruyter, pp. 87–139. Berlin (1979)Google Scholar
  14. 14.
    Feferman, S.: Reflecting on incompleteness. J. Symb. Log. 56(1), 1–49 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Feferman, S.: Gödel’s program for new axioms: Why, where, how and what? In: Hájek, P. (ed.) Gödel 1996 of Lecture Notes in Logic, vol. 6, pp. 3–22. Springer, Berlin (1996)Google Scholar
  16. 16.
    Feferman, S.: Operational set theory and small large cardinals. Inf. Comput. 207, 971–979 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Feferman, S.: Turing’s Thesis: Ordinal logics and oracle computability. In: Cooper, S.B., Van Leeuwen, J. (eds.) Alan Turing: His Work and Impact, pp. 145–150. Elsevier (2013)Google Scholar
  18. 18.
    Feferman, S.: The operational perspective: three routes. In: Kahle, R., Strahm, T., Studer, T. (eds.) Advances in Proof Theory of Progress in Computer Science and Applied Logic, vol. 28, pp. 269–289. Birkhäuser (2016)Google Scholar
  19. 19.
    Feferman, S., Spector, C.: Incompleteness along paths in progressions of theories. J. Symb. Log. 27, 383–390 (1962)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Feferman, S., Strahm, T.: The unfolding of non-finitist arithmetic. Ann. Pure Appl. Log. 104(1–3), 75–96 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Feferman, S., Strahm, T.: Unfolding finitist arithmetic. Rev. Symb. Log. 3(4), 665–689 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Ferreira, F.: Polynomial time computable arithmetic. In: Sieg, W. (ed.) Logic and Computation, Proceedings of a Workshop held at Carnegie Mellon University, 1987, Contemporary Mathematics, vol. 106, pp. 137–156. American Mathematical Society, Providence, Rhode Island (1990)Google Scholar
  23. 23.
    Franzén, T.: Transfinite progressions: a second look at completeness. Bull. Symb. Log. 10(3), 367–389 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Gödel, K.: Collected Works. In: Feferman, S. et al., (eds.) Vol. II. Oxford University Press, New York (1990)Google Scholar
  25. 25.
    Jäger, G.: On Feferman’s operational set theory OST. Ann. Pure Appl. Log. 150(1–3), 19–39 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Kreisel, G.: Ordinal logics and the characterization of informal concepts of proof. In: Proceedings International Congress of Mathematicians, 14–21 August 1958, pp. 289–299. Cambridge University Press, Cambridge (1960)Google Scholar
  27. 27.
    Kreisel, G.: Mathematical logic. In: Saaty, T.L. (ed.) Lectures on Modern Mathematics, vol. 3, pp. 95–195. Wiley, New York (1965)Google Scholar
  28. 28.
    Kreisel, G.: Principles of proof and ordinals implicit in given concepts. In: Kino, A., Myhill, J., Vesley, R.E. (eds.) Intuitionism and Proof Theory, pp. 489–516. North Holland, Amsterdam (1970)Google Scholar
  29. 29.
    Kripke, S.: Outline of a theory of truth. J. Philos. 72(19), 690–716 (1975)CrossRefzbMATHGoogle Scholar
  30. 30.
    Rathjen, M.: The role of parameters in bar rule and bar induction. J. Symb. Log. 56(2), 715–730 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Schütte, K.: Eine Grenze für die Beweisbarkeit der transfiniten Induktion in der verzweigten Typenlogik. Archiv für Mathematische Logik und Grundlagen der Mathematik 7, 45–60 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Sieg, W.: Herbrand analyses. Arch. Math. Log. 30(5+6), 409–441 (1991)Google Scholar
  33. 33.
    Strahm, T.: The non-constructive \(\mu \) operator, fixed point theories with ordinals, and the bar rule. Ann. Pure Appl. Log. 104(1–3), 305–324 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Tait, W.: Nested recursion. Mathematische Annalen 143, 236–250 (1961)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Tait, W.: Finitism. J. Philos. 78, 524–546 (1981)CrossRefGoogle Scholar
  36. 36.
    Turing, A.: Systems of logic based on ordinals. Proc. London Math. Soc. 2nd Ser. 45(I), 161–228 (1939)Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2017

Authors and Affiliations

  1. 1.Institut für InformatikUniversität BernBernSwitzerland

Personalised recommendations