A Minimal Computational Theory of a Minimal Computational Universe

  • Arnon Avron
  • Liron CohenEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


In [3] a general logical framework for formalizing set theories of different strength was suggested. We here employ that framework, focusing on the exploration of computational theories. That is, theories whose set of closed terms suffices for denoting every concrete set (including infinite ones) that might be needed in applications, as well as for computations with sets. We demonstrate that already the minimal computational level of the framework, in which only a minimal computational theory and a minimal computational universe are employed, suffices for developing large portions of scientifically applicable mathematics.


Formalized mathematics Computational theories Computational universes Rudimentary set theory 



The second author is supported by: Fulbright Post-doctoral Scholar program; Weizmann Institute of Science – National Postdoctoral Award program for Advancing Women in Science; Eric and Wendy Schmidt Postdoctoral Award program for Women in Mathematical and Computing Sciences.


  1. 1.
    Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical report 40, Mittag-Leffler (2001)Google Scholar
  2. 2.
    Avigad, J., Harrison, J.: Formally verified mathematics. Commun. ACM 57(4), 66–75 (2014)CrossRefGoogle Scholar
  3. 3.
    Avron, A.: A framework for formalizing set theories based on the use of static set terms. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 87–106. Springer, Heidelberg (2008). CrossRefGoogle Scholar
  4. 4.
    Avron, A.: A new approach to predicative set theory. In: Schindler, R. (ed.) Ways of Proof Theory, Onto Series in Mathematical Logic, pp. 31–63. Verlag (2010)Google Scholar
  5. 5.
    Avron, A., Cohen, L.: Formalizing scientifically applicable mathematics in a definitional framework. J. Formalized Reasoning 9(1), 53–70 (2016)MathSciNetGoogle Scholar
  6. 6.
    Beckmann, A., Buss, S.R., Friedman, S.D.: Safe recursive set functions. J. Symbolic Logic 80(3), 730–762 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Beeson, M.J.: Foundations of Constructive Mathematics: Metamathematical Studies, vol. 6. Springer Science & Business Media, Boston (2012)zbMATHGoogle Scholar
  8. 8.
    Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.): CICM 2008. LNCS, vol. 5144. Springer, Heidelberg (2008). Google Scholar
  9. 9.
    Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing: From Decision Procedures to Declarative Programming with Sets. Springer, New York (2001)CrossRefzbMATHGoogle Scholar
  10. 10.
    Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2013)zbMATHGoogle Scholar
  11. 11.
    Cohen, L., Avron, A.: The middle ground-ancestral logic. Synthese, 1–23 (2015)Google Scholar
  12. 12.
    Constable, R.L., Allen, S.F., Bromley, M., Cleaveland, R., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)Google Scholar
  13. 13.
    Corcoran, J., Hatcher, W., Herring, J.: Variable binding term operators. Math. Logic Q. 18(12), 177–182 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Devlin, K.: Constructibility. Perspectives in Mathematical Logic. Springer, Heidelberg (1984)CrossRefzbMATHGoogle Scholar
  15. 15.
    Feferman, S.: Systems of predicative analysis. J. Symbolic Logic 29(01), 1–30 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Feferman, S.: Systems of predicative analysis, II: representations of ordinals. J. Symbolic Logic 33(02), 193–220 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Feferman, S.: Why a little bit goes a long way: logical foundations of scientifically applicable mathematics. In: PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association, pp. 442–455. JSTOR (1992)Google Scholar
  18. 18.
    Feferman, S.: Operational set theory and small large cardinals. Inf. Comput. 207(10), 971–979 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Friedman, H.: Set theoretic foundations for constructive analysis. Ann. Math. 105(1), 1–28 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Gandy, R.O.: Set-theoretic functions for elementary syntax. In: Proceedings of Symposia in Pure Mathematics, vol. 13, pp. 103–126 (1974)Google Scholar
  21. 21.
    Jäger, G., Zumbrunnen, R.: Explicit mathematics and operational set theory: some ontological comparisons. Bull. Symbolic Logic 20(3), 275–292 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Jensen, R.B.: The fine structure of the constructible hierarchy. Ann. Math. Logic 4(3), 229–308 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Kamareddine, F.D.: Thirty Five Years of Automating Mathematics, vol. 28. Springer, Netherlands (2003)zbMATHGoogle Scholar
  24. 24.
    Mathias, A.R.D., Bowler, N.J., et al.: Rudimentary recursion, gentle functions and provident sets. Notre Dame J. Formal Logic 56(1), 3–60 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Megill, N.: Metamath: A Computer Language for Pure Mathematics. Elsevier Science, Amsterdam (1997)Google Scholar
  26. 26.
    Myhill, J.: Constructive set theory. J. Symbolic Logic 40(03), 347–382 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). zbMATHGoogle Scholar
  28. 28.
    Risch, R.H.: Algebraic properties of the elementary functions of analysis. Am. J. Math. 101(4), 743–759 (1979)CrossRefzbMATHGoogle Scholar
  29. 29.
    Rudnicki, P.: An overview of the MIZAR project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311–330 (1992)Google Scholar
  30. 30.
    Schwartz, J.T., Dewar, R.B., Schonberg, E., Dubinsky, E.: Programming with Sets: An Introduction to SETL. Springer-Verlag New York Inc., New York (1986). CrossRefzbMATHGoogle Scholar
  31. 31.
    Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Oxford University Press, Oxford (1991)zbMATHGoogle Scholar
  32. 32.
    Simpson, S.G.: Subsystems of Second Order Arithmetic, vol. 1. Cambridge University Press, Cambridge (2009)CrossRefzbMATHGoogle Scholar
  33. 33.
    Weaver, N.: Analysis in \({J}_2\). arXiv preprint arXiv:math/0509245 (2005)
  34. 34.
    Weyl, H.: Das Kontinuum: Kritische Untersuchungen über die Grundlagen der Analysis. W. de Gruyter (1932)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Tel Aviv UniversityTel-AvivIsrael
  2. 2.Cornell UniversityIthacaUSA

Personalised recommendations