Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-29T05:49:16.987Z Has data issue: false hasContentIssue false
  • English
  • Français

Mechanizing Nonstandard Real Analysis

Published online by Cambridge University Press:  01 February 2010

Jacques D. Fleuriot  and
Lawrence C. Paulson
Jacques D. Fleuriot
Affiliation:
Institute for Representation and Reasoning, Division of Informatics, University of Edinburgh, [email protected]
Lawrence C. Paulson
Affiliation:
Computer Laboratory, University of Cambridge, [email protected]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This paper first describes the construction and use of the hyperreals in the theorem-prover Isabelle within the framework of higher-order logic (HOL). The theory, which includes infinitesimals and infinite numbers, is based on the hyperreal number system developed by Abraham Robinson in his nonstandard analysis (NSA). The construction of the hyperreal number system has been carried out strictly through the use of definitions to ensure that the foundations of NSA in Isabelle are sound. Mechanizing the construction has required that various number systems including the rationals and the reals be built up first. Moreover, to construct the hyperreals from the reals has required developing a theory of filters and ultrafilters and proving Zorn's lemma, an equivalent form of the axiom of choice.

This paper also describes the use of the new types of numbers and new relations on them to formalize familiar concepts from analysis. The current work provides both standard and nonstandard definitions for the various notions, and proves their equivalence in each case. To achieve this aim, systematic methods, through which sets and functions are extended to the hyperreals, are developed in the framework. The merits of the nonstandard approach with respect to the practice of analysis and mechanical theorem-proving are highlighted throughout the exposition.

Type
Research Article
Information
LMS Journal of Computation and Mathematics , Volume 3 , 2000 , pp. 140 - 190
Copyright
Copyright © London Mathematical Society 2000

References

1. Abrial, J. R. and Laffitte, G., ‘Towards the mechanization of the proofs of some classical theorems of set theory‘, Preprint, February 1993.Google Scholar
2. Ballantyne, A. M. and Bledsoe, W. W., ‘Automatic proofs of theorems in analysis using nonstandard analysis’, J. ACM 24 (1977) 353–374.Google Scholar
3. Bedrax, T., ‘Infmal: prototype of an interactive theorem prover based on infinitesimal analysis’, Master's thesis, Pontifica Universidad Catolica de Chile, 1993. Liciendoen Mathematica con Mencion en Computation Thesis.Google Scholar
4. Beeson, M., ‘Using nonstandard analysis to ensure the correctness of symbolic computations’, Internal. J. Found. Comput. Sci. 6 (1995) 299–338.CrossRefGoogle Scholar
5. Burkill, J. C. and Burkill, H., A second course in mathematical analysis (Cambridge University Press, 1970).Google Scholar
6. Chuaqui, R. and Suppes, P., ‘Free-variable axiomatic foundations of infinitesimal analysis: a fragment with finitary consistency proof’, J. Symbolic Logic 60 (1995) 122–159.CrossRefGoogle Scholar
7. Church, A., ‘A formulation of the simple theory of type’, J. Symbolic Logic 5 (1940) 56–68.CrossRefGoogle Scholar
8. Conway, J. H., On numbers and games (Academic Press Inc. (London) Ltd, 1976).Google Scholar
9. Davis, P. J. and Hersh, R., The mathematical experience (Harmondsworth, Penguin, 1983).Google Scholar
10. Fleuriot, J. D. and Paulson, L. C., ‘A combination of geometry theorem proving and nonstandard analysis, with application to Newton's Principia’, Automated deduction —CADE-15 (ed. Kirchner, C and Kirchner, H.), Lecture Notes in Artificial Intelligence 1421 (Springer-Verlag, 1998) 3‘16.Google Scholar
11. Gleason, A. M., Fundamentals of abstract analysis, Series in Mathematics (Addison-Wesley, 1966).Google Scholar
12. Gordon, M. and Melham, T., Introduction to HOL: a theorem proving environment for higher order logic (Cambridge University Press, 1993).Google Scholar
13. Harrison, John, ‘Constructing the real numbers in HOL’, Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications (ed. Claesen, L. J. M. and Gordon, M. J. C.), IFIP Trans. A: Comput. Sci. Tech., vol. A-20 (North-Holland, IMEC, Leuven, Belgium, 1992) 145–164.Google Scholar
14. Harrison, John, Theorem proving with the real numbers (Springer-Verlag, 1998). Also published as Technical Report 408 of the Computer Laboratory, University of Cambridge, 1996.CrossRefGoogle Scholar
15. Henle, J. M. and Kleinberg, E. M., Infinitesimal calculus (The MIT Press, 1979).Google Scholar
16. Hoskins, R. F., Standard and nonstandard analysis, Math. Appl. (Ellis Horwood Limited, 1990).Google Scholar
17. Hurd, A. E. and P. A. LOEB, An introduction to nonstandard real analysis, Pure Appl. Math. 118 (Academic Press Inc., Boston, MA, 1985).Google Scholar
18. ‘Isabelle-online’, http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/HOL-Real/index.htmlGoogle Scholar
19. Jutting, L. S., ‘Checking Landau's “Grundlagen” in the Automath system’, Ph.D. thesis, Eindhoven University of Technology, 1977.Google Scholar
20. Keisler, H. J., Foundations of infinitesimal calculus (Prindle, Weber & Schmidt, 1976).Google Scholar
21. Landau, E., Foundations of analysis (Chelsea, 1951).Google Scholar
22. Laugwitz, D., ‘Infinitely small quantities in Cauchy's textbooks’, Historia Math. 14 (1987) 258–274.CrossRefGoogle Scholar
23. Lindstrøm, T., ‘An invitation to nonstandard analysis’, Nonstandard analysis and its applications (ed. Cutland, N.), London Math. Soc. Student Texts 10 (Cambridge University Press, 1988) 1–105.Google Scholar
24. Nipkow, T. and Von Oheimb, D., ‘Javalight is type-safe — definitely’, Proc. 25th ACM Symp. Principles of Programming Languages (ACM Press, New York, 1998) 161–170.Google Scholar
25. Paulson, L. C., Isabelle: a generic theorem prover, Lecture Notes in Comput. Sci. 828 (Springer, 1994).Google Scholar
26. Paulson, L. C., ‘The inductive approach to verifying cryptographic protocols’, J. Computer Security (1998) 85–128.CrossRefGoogle Scholar
27. Paulson, L. C., ‘Isabelle's object-logics’, Tech. Rep. 286, Computer Laboratory, University of Cambridge (February 1998).Google Scholar
28. Paulson, L. C. and K. Grąbczewski, ‘Mechanizing set theory: cardinal arithmetic and the axiom of choice’, Journal of Automat. Reason. 17 (1996) 291–323.Google Scholar
29. Robinson, A., Non-standard analysis (North-Holland, 1980).Google Scholar
30. Schechter, E., Handbook of analysis and its foundations (Academic Press, 1997).Google Scholar
31. Simpson, A. P., ‘The Infidel is innocent’, Math. Intelligencer 12 (1990) 43–51.CrossRefGoogle Scholar
32. Stroyan, K. D. and Luxemburg, W. A. J., Introduction to the theory of infinitesimals (Academic Press, 1976).Google Scholar
33. Vesley, R., ‘An intuitionistic infinitesimal calculus’, Constructive Mathematics (ed. Richman, F.), Lecture Notes in Math. 873 (Springer, 1983).Google Scholar
Supplementary material: File

Fleuriot and Paulson Appendix

Appendix

Download Fleuriot and Paulson Appendix(File)
File 863.4 KB