Automating Free Logic in HOL, with an Experimental Application in Category Theory
English
Benzmüller, Christoph[University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Scott, Dana[Berkeley University of California - UC Berkeley]
[en] 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 andverification of free logic theories. Subsequently, this approach is applied to aselected domain of mathematics: starting from a generalization of the standardaxioms for a monoid we present a stepwise development of various, mutuallyequivalent foundational axiom systems for category theory. As a side-effect ofthis work some (minor) issues in a prominent category theory textbook havebeen revealed.The purpose of this article is not to claim any novel results in category the-ory, but to demonstrate an elegant way to “implement” and utilize interactiveand automated reasoning in free logic, and to present illustrative experiments.
Benzmüller received funding from the German National Research Foundation DFG under Heisenberg grant Towards Computational Metaphysics (BE 2501/9-2) and from VolkswagenStiftung under grant Consistent Rational Argumentation in Politics (CRAP).
[University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
