Banishing ultrafilters from our consciousness

The way in which Martin Davis conceived the first chapter of his book ``emph{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 see there a common trait between that book and another writing of the year 1977, ``emph{Metamathematical extensibility for theorem provers and proof-checkers}'', which Martin coauthored with Jacob T. Schwartz. To underline the contribution of the said part of Martin's study on nonstandard analysis to proof technology, we prepare the ground for its detailed verification with a proof-checker based on set theory.