Banishing Ultrafilters from Our Consciousness

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.