Formalizing Scientifically Applicable Mathematics in a Definitional Framework
DOI:
https://doi.org/10.6092/issn.1972-5787/4573Keywords:
MKM, Scientifically Applicable Mathematics, safety relationsAbstract
In [Arnon08, A framework for formalizing set theories based on the use of static set terms.] a new framework for formalizing mathematics was developed. The main new features of this framework are that it is based on the usual first-order set theoretical foundations of mathematics (in particular, it is type-free), but it reflects real mathematical practice in making an extensive use of statically defined abstract set terms of the form { x | p(i) }, in the same way they are used in ordinary mathematical discourse.
In this paper we show how large portions of fundamental, scientifically applicable mathematics can be developed in this framework in a straightforward way, using just a rather weak set theory which is predicatively acceptable and essentially first-order. The key property of that theory is that every object which is used in it is defined by some closed term of the theory. This allows for a very concrete, computationally-oriented interpretation of the theory. However, the development is not committed to such interpretation, and can easily be extended for handling stronger set theories (including ZF).
References
Arnon Avron. Formalizing set theory as it is actually used. In Mathematical Knowledge Management, pages 32--43. Springer, 2004.
Arnon Avron. Constructibility and decidability versus domain independence and absoluteness. Theoretical Computer Science, 394(3):144--158, 2008.
Arnon Avron. A framework for formalizing set theories based on the use of static set terms. In Pillars of computer science, pages 87--106. Springer, 2008.
Arnon Avron. A new approach to predicative set theory. Ways of Proof Theory, pages 31--63, 2010.
Robert Boyer et al. The qed manifesto. Automated Deduction--CADE, 12:238--251, 1994.
Adam Chlipala.An introduction to programming and proving with dependent types in Coq. Journal of Formalized Reasoning (JFR), 3(2):1--93, 2010.
Adam Chlipala. Certified Programming with Dependent Types. MIT Press, Cambridge, MA, 2013.
Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R.W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith.
Implementing mathematics with the Nuprl proof development
system.Prentice Hall, 1986.
N.G. de Bruijn. A survey of the project AUTOMATH.
Solomon Feferman. Systems of predicative analysis. Journal of Symbolic logic, pages 1--30, 1964.
Solomon Feferman. Systems of predicative analysis, ii: Representations of ordinals. Journal of Symbolic Logic, pages 193--220, 1968.
Solomon Feferman. A more perspicuous formal system for predicativity.
Konstruktionen versus Positionen, 1:68--93, 1978.
Abraham Adolf Fraenkel, Yehoshua Bar-Hillel, and Azriel Levy. Foundations of set theory. Elsevier, 1973.
Robin Oliver Gandy. Set-theoretic functions for elementary syntax. Proc. Symp. in Pure Math, volume~13, pages 103--126, 1974.
Michael Hallett. Cantorian set theory and limitation of size. Clarendon Press Oxford, 1984.
Karel Hrbacek and Thomas Jech. Introduction to Set Theory, Revised and Expanded, volume 220. Crc Press, 1999.
Albert E. Hurd and Peter A. Loeb. An introduction to nonstandard real analysis, volume 118. Academic Press, 1985.
R. Bj{"o}rn Jensen. The fine structure of the constructible hierarchy. Annals of Mathematical Logic, 4(3):229--308, 1972.
Kenneth Kunen. Set theory. an introduction to independence proofs, 2nd print. Studies in Logic and the Foundations of Mathematics, 102.
Azriel Levy. Basic set theory perspectives in mathematical logic. Berlim: Spring, 1979.
Elliott Mendelson. Introduction to mathematical logic. CRC press, 1997.
Rob P. Nederpelt, Jan~Herman Geuvers, and R.C. De Vrijer. Selected papers on Automath. Elsevier, 1994.
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer, 2002.
Piotr Rudnicki. An overview of the mizar project. Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 311--330, 1992.
Andrzej Trybulec and Howard A. Blair. Computer aided reasoning.
Logics of Programs, pages 406--412. Springer, 1985.
Jeffrey D. Ullman. Principles of Database and Knowledge-base Systems, Vol. I. Computer Science Press, Inc., New York, NY, USA, 1988.
Nik Weaver. Analysis in ${J}_2$. arXiv preprint math/0509245}, 2005.
Freek Wiedijk. The qed manifesto revisited. Studies in Logic, Grammar and Rhetoric, 10(23):121--133, 2007.
Jeff Zucker. Formalization of classical mathematics in automath. Studies in Logic and the Foundations of Mathematics, 133:127--139, 1994.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2016 Arnon Avron, Liron Cohen
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
