# Unfolding Schematic Systems

Chapter
Part of the Outstanding Contributions to Logic book series (OCTR, volume 13)

## Abstract

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.

## Keywords

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

## 2010 Mathematics Subject Classification

03F03 03F30 03D75

## References

1. 1.
Beeson, M.J.: Foundations of Constructive Mathematics: Metamathematical Studies. Springer, Berlin (1985)
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)
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)
11. 11.
Feferman, S.: Systems of predicative analysis. J. Symb. Log. 29(1), 1–30 (1964)
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)
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)
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)
20. 20.
Feferman, S., Strahm, T.: The unfolding of non-finitist arithmetic. Ann. Pure Appl. Log. 104(1–3), 75–96 (2000)
21. 21.
Feferman, S., Strahm, T.: Unfolding finitist arithmetic. Rev. Symb. Log. 3(4), 665–689 (2010)
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)
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)
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)
30. 30.
Rathjen, M.: The role of parameters in bar rule and bar induction. J. Symb. Log. 56(2), 715–730 (1991)
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)
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)
34. 34.
Tait, W.: Nested recursion. Mathematische Annalen 143, 236–250 (1961)
35. 35.
Tait, W.: Finitism. J. Philos. 78, 524–546 (1981)
36. 36.
Turing, A.: Systems of logic based on ordinals. Proc. London Math. Soc. 2nd Ser. 45(I), 161–228 (1939)Google Scholar