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 information hiding as guiding principle for design widely applicable constructions and methods proof. We discuss here common trait that we see between another writing year 1977, “Metamathematical extensibility theorem provers proof-checkers”, coauthored with Jacob T. Schwartz . To tie said part Martin’s study on to proof technology, undertake verification, by means proof-checker based set theory, key results non-standard approach analysis.