×

Automating free logic in HOL, with an experimental application in category theory. (English) Zbl 1434.68639

Summary: 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.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B16 Higher-order logic
03B35 Mechanization of proofs and logical operations
03B60 Other nonclassical logic
18A15 Foundations, relations to logic and deductive systems
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Andrews, P., General models and extensionality, J. Symb. Log., 37, 2, 395-397 (1972) · Zbl 0264.02050 · doi:10.2307/2272982
[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] Barendregt, H.; Dekkers, W.; Statman, R., Lambda Calculus with Types. Perspectives in Logic (2013), Cambridge: Cambridge University Press, Cambridge · Zbl 1347.03001
[4] Benzmüller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) Proceedings of IJCAI-23. Beijing, China (2013)
[5] Benzmüller, C., Cut-elimination for quantified conditional logic, J. Philos. Log., 46, 333-353 (2016) · Zbl 1417.03282 · doi:10.1007/s10992-016-9403-0
[6] Benzmüller, C.; Brown, C.; Kohlhase, M., Higher-order semantics and extensionality, J. Symb. Log., 69, 4, 1027-1088 (2004) · Zbl 1071.03024 · doi:10.2178/jsl/1102022211
[7] Benzmüller, C.; Brown, C.; Kohlhase, M., Cut-simulation and impredicativity, Log. Methods Comput. Sci., 5, 1-6, 1-21 (2009) · Zbl 1160.03004
[8] Benzmüller, C.; Miller, D.; Siekmann, J.; Gabbay, D.; Woods, J., Automation of higher-order logic, Handbook of the History of Logic, Volume 9—Logic and Computation (2014), Amsterdam: Elsevier, Amsterdam · Zbl 1311.03006
[9] Benzmüller, Christoph; Scott, Dana, Automating Free Logic in Isabelle/HOL, Mathematical Software - ICMS 2016, 43-50 (2016), Cham: Springer International Publishing, Cham · Zbl 1434.68638
[10] Benzmüller, C., Scott, D.S.: Axiomatizing category theory in free logic. CoRR (2016). arXiv:1609.01493 · Zbl 1434.68638
[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] 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)
[13] Benzmüller, C.; Sultana, N.; Paulson, Lc; Theiss, F., The higher-order prover Leo-II, J. Autom. Reason., 55, 4, 389-404 (2015) · Zbl 1356.68176 · doi:10.1007/s10817-015-9348-y
[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] Blanchette, Jc; Böhme, S.; Paulson, Lc, Extending Sledgehammer with SMT solvers, J. Autom. Reason., 51, 1, 109-128 (2013) · Zbl 1314.68272 · doi:10.1007/s10817-013-9278-5
[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) · Zbl 1291.68326
[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) · Zbl 1360.68742
[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) · Zbl 1358.68250
[19] Church, A., A formulation of the simple theory of types, J. Symb. Log., 5, 56-68 (1940) · Zbl 0023.28901 · doi:10.2307/2266170
[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)
[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)
[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] Freyd, P.; Scedrov, A., Categories (1990), Allegories: North Holland, Allegories · Zbl 0698.18002
[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)
[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)
[26] Lambert, K., Free Logic: Selected Essays (2002), Cambridge: Cambridge University Press, Cambridge
[27] Maclane, S., Groups, categories and duality, Proc. Nat. Acad. Sci., 34, 6, 263-267 (1948) · Zbl 0031.24702 · doi:10.1073/pnas.34.6.263
[28] Makarenko, I.: Automatisierung von Freier Logik in Logik Höherer Stufe. Bachelorarbeit. Freie Universität Berlin, Institut für Informatik (2016)
[29] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. No. 2283 in LNCS. Springer (2002) · Zbl 0994.68131
[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] 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). doi:10.1007/978-3-642-45221-5 · Zbl 1277.68016
[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)
[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) · Zbl 0418.03016
[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) · Zbl 1211.68371
[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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.