Advertisement

Automating Free Logic in HOL, with an Experimental Application in Category Theory

  • Christoph BenzmüllerEmail author
  • Dana S. Scott
Article
  • 10 Downloads

Abstract

A shallow semantical embedding of free logic in classical higher-order logic is presented, which enables the off-the-shelf application of higher-order interactive and automated theorem provers for the formalisation and verification of free logic theories. Subsequently, this approach is applied to a selected domain of mathematics: starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. As a side-effect of this work some (minor) issues in a prominent category theory textbook have been revealed. The purpose of this article is not to claim any novel results in category theory, but to demonstrate an elegant way to “implement” and utilize interactive and automated reasoning in free logic, and to present illustrative experiments.

Keywords

Free logic Classical higher-order logic Category theory Interactive and automated theorem proving 

Notes

Acknowledgements

We thank Günter Rote, Lutz Schröder and and Emil Weydert for their comments to [10], which together with [9] forms the basis for this article. We also want to express our gratitude to the reviewers of this article. Their fruitful feedback definitely helped to improve the final version.

Supplementary material

10817_2018_9507_MOESM1_ESM.thy (34 kb)
Supplementary material 1 (thy 33 KB)
10817_2018_9507_MOESM2_ESM.thy (35 kb)
Supplementary material 2 (thy 35 KB)

References

  1. 1.
    Andrews, P.: General models and extensionality. J. Symb. Log. 37(2), 395–397 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Andrews, P.: Church’s type theory. In: Zalta, E. N (ed.) The Stanford Encyclopedia of Philosophy, Summer 2018 edn. Metaphysics Research Lab, Stanford University (2018). https://plato.stanford.edu/archives/sum2018/entries/type-theory-church/
  3. 3.
    Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, Cambridge (2013)CrossRefzbMATHGoogle Scholar
  4. 4.
    Benzmüller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) Proceedings of IJCAI-23. Beijing, China (2013)Google Scholar
  5. 5.
    Benzmüller, C.: Cut-elimination for quantified conditional logic. J. Philos. Log. 46, 333–353 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Benzmüller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027–1088 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Benzmüller, C., Brown, C., Kohlhase, M.: Cut-simulation and impredicativity. Log. Methods Comput. Sci. 5(1:6), 1–21 (2009)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J., Gabbay, D., Woods, J. (eds.) Handbook of the History of Logic, Volume 9—Logic and Computation. Elsevier, Amsterdam (2014)Google Scholar
  9. 9.
    Benzmüller, C., Scott, D.: Automating free logic in Isabelle/HOL. In: Greuel, G.M., Koch, T., Paule, P., Sommese, A. (eds.) Mathematical Software—ICMS 2016, 5th International Congress, Proceedings, LNCS, vol. 9725, pp. 43–50. Springer, Berlin, Germany (2016)Google Scholar
  10. 10.
    Benzmüller, C., Scott, D.S.: Axiomatizing category theory in free logic. CoRR (2016). arXiv:1609.01493
  11. 11.
    Benzmüller, C., Scott, D.S.: Axiom systems for category theory in free logic. Archive of Formal Proofs (2018). https://www.isa-afp.org/entries/AxiomaticCategoryTheory.html
  12. 12.
    Benzmüller, C., Steen, A., Wisniewski, M.: Leo-III version 1.1 (system description). In: Eiter, T., Sands, D. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)—Short Papers, Kalpa Puplications. EasyChair, Maun, Botswana (2017) (to appear) Google Scholar
  13. 13.
    Benzmüller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover Leo-II. J. Autom. Reason. 55(4), 389–404 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Blanchette, J.C.: Hammering Away—A Users Guide to Sledgehammer for Isabelle/HOL. Institut für Informatik, Technische Universität München (2018). https://isabelle.in.tum.de/doc/sledgehammer.pdf. With contributions from Lawrence C. Paulson
  15. 15.
    Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6172, pp. 131–146. Springer (2010)Google Scholar
  17. 17.
    Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle—superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving—Third International Conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7406, pp. 345–360. Springer (2012)Google Scholar
  18. 18.
    Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning—6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7364, pp. 111–117. Springer (2012)Google Scholar
  19. 19.
    Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: How it works, and how to use it. In: Claessen, K., Kuncak, V. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21–24, 2014, p. 7. IEEE (2014)Google Scholar
  21. 21.
    de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008)Google Scholar
  22. 22.
    Freyd, P.: Amplifications, Diminutions, Subscorings for Categories, Allegories (2016). University of Pennsylvania. Unpublished. https://www.math.upenn.edu/~pjf/amplifications.pdf. Accessed Aug 2016
  23. 23.
    Freyd, P., Scedrov, A.: Categories. North Holland, Allegories (1990)zbMATHGoogle Scholar
  24. 24.
    Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 1–35. Springer (2013)Google Scholar
  25. 25.
    Lambert, K.: The definition of e(xistence)! in free logic. In: Abstracts: The International Congress for Logic, Methodology and Philosophy of Science. Stanford University Press, Stanford (1960)Google Scholar
  26. 26.
    Lambert, K.: Free Logic: Selected Essays. Cambridge University Press, Cambridge (2002)CrossRefzbMATHGoogle Scholar
  27. 27.
    MacLane, S.: Groups, categories and duality. Proc. Nat. Acad. Sci. 34(6), 263–267 (1948)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Makarenko, I.: Automatisierung von Freier Logik in Logik Höherer Stufe. Bachelorarbeit. Freie Universität Berlin, Institut für Informatik (2016)Google Scholar
  29. 29.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. No. 2283 in LNCS. Springer (2002)Google Scholar
  30. 30.
    Nolt, J.: Free logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Fall 2018 edn. Metaphysics Research Lab, Stanford University (2018). https://plato.stanford.edu/archives/fall2018/entries/logic-free/
  31. 31.
    Schulz, S.: System description: E 1.8. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8312, pp. 735–743. Springer (2013). http://dx.doi.org/10.1007/978-3-642-45221-5
  32. 32.
    Scott, D.: Existence and description in formal logic. In: Schoenman, R. (ed.) Bertrand Russell: Philosopher of the Century, pp. 181–200. George Allen & Unwin, London (1967) (Reprinted with additions in: Philosophical Application of Free Logic, edited by K. Lambert. Oxford Universitry Press, 1991, pp. 28–48)Google Scholar
  33. 33.
    Scott, D.: Identity and existence in intuitionistic logic. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9–21, 1977, Lecture Notes in Mathematics, vol. 752, pp. 660–696. Springer, Berlin, Heidelberg (1979)Google Scholar
  34. 34.
    Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010)MathSciNetzbMATHGoogle Scholar
  35. 35.
    Wisniewski, M., Steen, A., Benzmüller, C.: TPTP and beyond: representation of quantified non-classical logics. In: Benzmüller, C., Otten, J. (eds.) ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics, vol. 1770, pp. 51–65. CEUR Workshop Proceedings. http://ceur-ws.org (2016)

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.Freie Universität BerlinBerlinGermany
  2. 2.University of LuxembourgEsch-sur-AlzetteLuxembourg
  3. 3.University of CaliforniaBerkeleyUSA

Personalised recommendations