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)

DMI, Universita di Catania, Viale A. Doria 6, 95125 Catania, Italy e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

E. G. Omodeo

DMG/DMI, Universita di Trieste, Via Valerio 12/1, 34127 Trieste, Italy e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

A. Policriti

DMIF, Universita di Udine, Via Delle Scienze 206, 33100 Udine, Italy e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

© 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

 
Source
< Prev   CONTENTS   Source   Next >