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.
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)
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Landmark contributions of Martin to automatic theorem-proving in 1st-order predicate logic have been [10, 13, 19, 20, 25], historically occurring between Paul C. Gilmore’s and Dag Prawitz’ methods, on the one hand, and J. Alan Robinson’s resolution principle on the other. Concerning the linked conjunct method then proposed by Martin and his team at Bell Labs , see [29, 39].
- 3.
- 4.
See [8, pp. 5–6]. In a recent personal web-page, David Aspinall (Univ. of Edinburgh) defines Proof Engineering to mean the activity on construction, maintenance, documentation and presentation of large formal proof developments. Within Proof Engineering , according to Aspinall, “Software Engineering provides the techniques to develop large, structured and well-specified repositories of computer code; proof checking provides the mechanisms to provide a complete semantics and formal correctness as an absolute quality criterion.”.
- 5.
In particular, when \(\mathsf {D}=\mathbb {R}\), we get a field, \({^*\!{\mathbb {R}}}\), of entities called hyperreal numbers. In \({^*\!{\mathbb {R}}}\) there are positive numbers lying infinitely close to zero; the reciprocals of such infinitesimals must, of course, exceed any positive integer.
- 6.
- 7.
A slicker characterization of ultrafilters will be shown in Fig. 10.7.
- 8.
In a similar attitude, [11, p. 54] states that “one possible view is that the integers are atoms and should not be viewed as sets. Even in this case, one might still wish to prevent the existence of unrestricted atoms. In any case, for the ‘genuine’ sets, Extensionality holds and the other sets are merely harmless curiosities.”.
- 9.
When the need will arise, we will adjust this notation also to terms, indicating by \(t(\varvec{c})\) a term devoid of variables resulting from replacement of a variable of t by a constant \(\varvec{c}\).
- 10.
About Ref’s built-in operator \(\varvec{arb}\left( X\right) \) that occurs thrice in Fig. 10.1, suffice it to say for the time being that it selects an element of its operand X when \(X\ne \emptyset \), and that \(\varvec{arb}\left( \emptyset \right) =\emptyset \).
- 11.
In a passage echoing Abraham Robinson’s ‘provocative remark’ which we have recalled in the Introduction through Martin’s words, Jack says about this ability of Theory s [35, p. 9]: “\(\cdots \)definitions serve to ‘instantiate’, that is, to introduce the objects whose special properties are crucial to an intended argument. Like the selection of crucial lines, points, and circles from the infinity of geometric elements that might be considered in a Euclidean argument, definitions of this kind often carry a proof’s most vital ideas”. A typical case of this kind is, in arithmetic, the selection of the least natural number that meets some key property.
- 12.
This is a specialized variant of the Theory \(\mathsf {reachability}\) presented in [35, Sect. 7.3]. As seen here, the formal output parameters of a Theory always carry a subscript \(\varTheta \).
- 13.
What follows is not meant to imply that the definition of \(\mathbb {N}\) shown is the ideal one.
- 14.
A common definition of ordinals , owing to a simplification due to Raphael Robinson , is:
$$ \begin{aligned} \mathsf {Ord}(U)\ \,\leftrightarrow _{\text {Def}}\,\ \forall \,x\,(x\in U{\varvec{\,\rightarrow \,}}x\subseteq U) \, \& \,\forall \,x\,\forall \,y\big (\left\{ x, y\right\} \subseteq U{\varvec{\,\rightarrow \,}}(x\in y\vee y\in x\vee x=y)\big )\,. \end{aligned}$$ - 15.
Natural numbers will play an irreplaceable role in the informal arguments providing the rationale for the formal constructions that follow; within the formal treatment, their collection \(\mathbb {N}\) will act as a set whose infinitude is easiest to prove (and infinite sets will be crucial in Sect. 10.8).
- 16.
One way of implementing lists is discussed in [30, pp. 127–128].
- 17.
This way of representing formulae in conjunctive normal form is widely used today. In recent years [32] resorted to it, to give a Ref-based correctness proof for the DPLL satisfiability algorithm.
- 18.
A website reporting on our experiment is at http://www2.units.it/eomodeo/InitialSetupForNonStandardAnalysis.html, http://aetnanova.units.it/scenarios/InitialSetupForNonStandardAnalysis/.
- 19.
In Ref the well-foundendess of membership and statements of the axiom of choice easily result from the availability of the construct \(\varvec{arb}\) discussed in Sect. 10.6, thanks to the interplay of \(\varvec{arb}\) with abstract set formers; infinity is embodied by Ref’s built-in constant \(\varvec{\sigma }_{\!\infty }\).
- 20.
References
Anastasio, S. (Coordinating Editor) (2015). In memory of Jacob Schwartz. Notices of the AMS, 473–490.
Ballantyne, A. M. (1991). The Metatheorist: Automatic proofs of theorems in analysis using non-standard techniques, Part II. In R. S. Boyer (Ed.), Automated reasoning: Essays in Honor of Woody Bledsoe (pp. 61–75). Dordrecht, The Netherlands: Kluwer Academic.
Ballantyne, A. M., & Bledsoe, W. W. (1977). Automatic proofs of theorems in analysis using nonstandard techniques. Journal of the ACM, 24(3), 353–374.
Blass, A. (1978). Book reviews of Applied nonstandard analysis, by Martin Davis, Introduction to the theory of infinitesimals, by K. D. Stroyan and W. A. J. Luxemburg, and Foundations of infinitesimal calculus, by H. Jerome Keisler. Bull. Amer. Math. Soc., 84(1):34–41, 1978.
Bledsoe, W. W. (1977). Non-resolution theorem proving. Artificial Intelligence, 9(1), 1–35.
Boldo, S., Lelay, C., & Melquiond, G. (2015). Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 38 pp.
Burstall, R., & Goguen, J. (1977). Putting theories together to make specifications. In R. Reddy (Ed.), Proceedings of the 5th International Joint Conference on Artificial Intelligence (pp. 1045–1058). Cambridge, MA.
Cantone, D., Omodeo, E. G., & Policriti, A. (2001). Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer.
Ceterchi, R., Omodeo, E. G., & Tomescu, A. I. (2014). The representation of Boolean algebras in the spotlight of a proof checker. In L. Giordano, V. Gliozzi, & G. L. Pozzato, (Eds.), CILC 2014: Italian Conference on Computational Logic, volume 1195 http://ceur-ws.org/Vol-1195/, ISSN 1613-0073, pp. 287–301. CEUR Workshop Proceedings, July 2014.
Chinlund, T. J., Davis, M., Hinman, P. G., & McIlroy, M. D. (1964). Theorem-proving by matching. Technical report, Bell Telephone Laboratories, Incorporated, Murray Hill, New Jersey.
Cohen, P. J. (1966). Set Theory and the Continuum Hypothesis. Mathematics Lecture Note Series. Reading, Massachusetts: W. A. Benjamin, Inc.
Davis, M. (1960). A program for Presburger’s algorithm. Summaries of talks presented at the Summer Institute of Symbolic Logic in 1957 at Cornell University (vol. 2, pp. 215–223). Princeton, NJ. Communications Research Division, Institute for Defense Analyses. Reprinted as “A computer program for Presburger’s algorithm” in [36, pp. 41–48].
Davis, M. (1963). Eliminating the irrelevant from mechanical proofs. Proceedings of Symposia in Applied Mathematics (vol. 15, pp. 15–30). Providence, RI: AMS. Reprinted in [36, pp. 315–330]; Russian transl. in Kiberneticheskiy sbornik. Novaya seriya, 7, 1970, pp. 160–179.
Davis, M. (1977). Applied nonstandard analysis. Wiley. Reprinted with corrections Dover, 2005. Russian translation, Izdatel’stvo Mir, Moscow 1980. Japanese translation 1977.
Davis, M. (2001). The early history of automated deduction. In J. A. Robinson & A Voronkov, (Eds.), Handbook of Automated Reasoning (pp. 3–15). Elsevier and MIT Press.
Davis, M. (2013). Jack Schwartz meets Karl Marx. In [22, pp. 23–37].
Davis, M., & Fechter, R. (1991). A free variable version of the first-order predicate calculus. Journal of Logic and Computation, 1(4), 431–451.
Davis, M., & Hersh, R. (1972). Nonstandard analysis. Scientific American, 226, 78–86.
Davis, M., & Putnam, H. (1958). Feasible computational methods in the propositional calculus. Technical report, Rensselaer Polytechnic Institute, Research Division, Troy, New York.
Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM, 7(3):201–215. Reprinted in [36, pp. 125–139].
Davis, M., & Schonberg, E. (2011). Jacob Theodore Schwartz 1930–2009. Biographical Memoirs of the National Academy of Sciences,19 pp.
Davis, M., & Schonberg, E. (Eds.). (2013). From Linear Operators to Computational Biology: Essays in Memory of Jacob T. Schwartz. Springer.
Davis, M. & Schwartz, J. T. (1977). Correct-program technology/Extensibility of verifiers—Two papers on Program Verification with Appendix of Edith Deak. Technical Report No. NSO-12, Courant Institute of Mathematical Sciences, New York University.
Davis, M. & Schwartz, J. T. (1979). Metamathematical extensibility for theorem verifiers and proof-checkers. Computers and Mathematics with Applications, 5, 217–230. Also in [25, pp. 120–146].
Davis, M., Logemann, G., & Loveland, D. W. (1962). A machine program for theorem-proving. Communications of the Association for Computing. Machinery, 5(7), 394–397.
Fleuriot, J. D. (2000). On the mechanization of real analysis in Isabelle/HOL. In M. Aagaard & J. Harrison, (Eds.), Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, 14–18 August 2000, Proceedings, volume 1869 of Lecture Notes in Computer Science (pp. 145–161). Springer.
Gamboa, R., & Kaufmann, M. (2001). Nonstandard analysis in ACL2. Journal of Automated Reasoning, 27(4), 323–351.
Keisler, H. J. (1976). Foundations of infinitesimal calcuus. Boston, MA: Prindle, Weber & Schmidt, Inc.
Omodeo, E. G. (1982). The Linked Conjunct method for automatic deduction and related search techniques. Computers and Mathematics with Applications, 8, 185–203.
Omodeo, E. G. (2012). The Ref proof-checker and its “common shared scenario”. In M. Davis & E. Schonberg, (Eds.), From Linear Operators to Computational Biology: Essays in Memory of Jacob T. Schwartz (pp. 121–131). Springer.
Omodeo, E. G., & Schwartz, J. T. (2002). A ‘Theory’ mechanism for a proof-verifier based on first-order set theory. In A. Kakas & F. Sadri, (Eds.), Computational logic: Logic programming and beyond—Essays in honour of Bob Kowalski, part II (vol. 2408, pp. 214–230). Springer.
Omodeo, E. G., & Tomescu, A. I. (2008). Using ÆtnaNova to formally prove that the Davis-Putnam satisfiability test is correct. Le Matematiche, 63(1), 85–105.
Policriti, A. (1988). Decision procedures for elementary sublanguages of set theory. IX. Unsolvability of the decision problem for a restricted class of the \(\Delta _0\)-formulas in set theory. Communications on Pure and Applied Mathematics 41(2), 221–251.
Robinson, J. A. (1967). Review: Martin Davis, Eliminating the irrelevant from mechanical proofs. Journal of Symbolic Logic, 32(1), 118–119.
Schwartz, J. T., Cantone, D., & Omodeo, E. G. (2011). Computational logic and set theory—Applying formalized logic to analysis. Springer.
Siekmann, J., & Wrightson, G. (Eds.). (1983). Automation of reasoning 1: Classical papers on computational logic 1957–1966. Berlin, Heidelberg: Springer.
Turing, A. M. (1939). Systems of logic based on ordinals. Proceedings of the London Mathematical Society, 2(45), 161–228.
Weyhrauch, R. W. (1977). A users manual for FOL. Technical Report MEMO AIM-235.1, Stanford University, Stanford, CA, USA.
Yarmush, D. L. (1976). The Linked Conjunct and other algorithms for mechanical theorem-proving. Technical Report IMM 412, Courant Institute of Mathematical Sciences, New York University.
Acknowledgements
Discussions with Francesco Di Cosmo helped in polishing this paper. The first author acknowledges partial support from the Polish National Science Centre research project DEC-2011/02/A/HS1/00395; and the second author from the project FRA-UniTS (2014) “Learning specifications and robustness in signal analysis.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Cantone, D., Omodeo, E.G., Policriti, A. (2016). Banishing Ultrafilters from Our Consciousness. In: Omodeo, E., Policriti, A. (eds) Martin Davis on Computability, Computational Logic, and Mathematical Foundations. Outstanding Contributions to Logic, vol 10. Springer, Cham. https://doi.org/10.1007/978-3-319-41842-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-41842-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41841-4
Online ISBN: 978-3-319-41842-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)