Banishing Ultrafilters from Our Consciousness
Domenico Cantone, Eugenio G. Omodeo and Alberto Policriti
The reader who remembers these key points will do well in what follows. In particular, it is now quite all right to entirely forget how the nonstandard universe was defined and to banish ultrafilters from our consciousness.
(Martin Davis, Applied Nonstandard Analysis, 1977)
Abstract The way in which Martin Davis conceived the first chapter of his book “Applied nonstandard analysis” is a brilliant example of information hiding as a guiding principle for the design of widely applicable constructions and methods of proof. We discuss here a common trait that we see between that book and another writing of the year 1977, “Metamathematical extensibility for theorem provers and proof-checkers”, which Martin coauthored with Jacob T. Schwartz. To tie the said part of Martin’s study on nonstandard analysis to proof technology, we undertake a verification, by means of a proof-checker based on set theory, of key results of the non-standard approach to analysis.
Keywords Proof checking • Proof engineering • Nonstandard analysis • Foundations of infinitesimal calculus
D. Cantone (B)
E. G. Omodeo
© Springer International Publishing Switzerland 2016 255
E.G. Omodeo and A. Policriti (eds.), Martin Davis on Computability,
Computational Logic, and Mathematical Foundations,
Outstanding Contributions to Logic 10, DOI 10.1007/978-3-319-41842-1_10