Computer-Verified Foundations of Metaphysics

We report on recent successes in the application of computational methods and automated reasoning techniques to a foundational theory of metaphysics: in [13], we utilize and extend the method of shallow semantic embeddings (SSEs) in classical higher-order logic (HOL) to construct a custom theorem proving environment for abstract object theory (AOT) on the basis of Isabelle/HOL.

Isabelle/HOL [17] is the most developed object logic in the generic proof assistant Isabelle and implements a version of classical higher-order logic. It provides access to sophisticated automation tools like sledgehammer [20] and model finding tools like nitpick [9]. These tools in turn interface with first-order provers like E [22], SPASS [24] and Vampire [21], SMT solvers like veriT [10] and Z3 [16], as well as higher-order provers like Zipperposition [23].

SSEs are a means for universal logical reasoning by translating a target logic to HOL using a representation of its semantics (see [1]). They form a cornerstone of the more recent development of the LogiKEy framework that focuses on the application of the method to ethical reasoning, normative theories and deontic logics [3, 5].

The target theory of our work, AOT, is a foundational metaphysical theory, developed by Edward Zalta, that explains the objects presupposed by the sciences as abstract objects that reify property patterns. The most recent canonical presentation of AOT can be found in a regularly updated online monograph called Principia Logico-Metaphysica (PLM) [33]. The theory is also the subject of two books [28, 29] and various scientific articles.

Our work in [13] focuses in particular on AOT’s aspiration to provide a philosophically grounded basis for the construction and analysis of the objects of mathematics. We can support this claim by verifying Uri Nodelman’s and Edward Zalta’s reconstruction of Frege’s theorem: we confirm that the Dedekind-Peano postulates for natural numbers are consistently derivable in AOT using Frege’s method. Furthermore, we can suggest and discuss generalizations and variants of the construction and can thereby provide theoretical insights into, and contribute to the philosophical justification of, the construction.

In the process, we can demonstrate that our method allows for a nearly transparent exchange of results between traditional pen-and-paper-based reasoning and the computerized implementation, which in turn can retain the automation mechanisms available for our meta-logic Isabelle/HOL.

During our work, we could significantly contribute to the evolution of our target theory itself, while simultaneously solving the technical challenge of using an SSE to implement a theory that is based on logical foundations that significantly differ from the meta-logic HOL.

In general, our results demonstrate the fruitfulness of the practice of Computational Metaphysics, i.e. the application of computational methods to metaphysical questions and theories (see [14]). Furthermore, our method allows for the transferal of existing technology for automated reasoning to new domains and for the computer-aided experimental investigation of variations and different axiomatizations of complex foundational logical theories with large bodies of theorems.

Prior to our work, SSEs were primarily applied to isolated logical arguments [4, 7, 11] and logics that are closely related to the meta-logic HOL like higher-order modal logic [2, 6, 8]. In contrast, our target, AOT, is a full logical theory that positions itself as a foundational framework and involves hyperintensional relations, a free logic governing its complex terms, and an additional mode of predication besides classical exemplification called encoding. Furthermore, it is based on a relational type theory that was previously argued to be incompatible with, and not representable in, systems based on functional type theory like Isabelle/HOL (see [19]).

In successfully implementing AOT, our work shows that the SSE approach scales to challenging logics, even if they extend classical logic significantly, and that the approach can be used to represent full theories by faithfully reconstructing their axioms and deductive system. We demonstrate that not only the logical structure of a theory can be technically implemented, but also that its syntax and reasoning flow can be preserved. To that end, we utilize Isabelle’s mechanisms for constructing custom inner syntax and, further, by extending Isabelle’s outer syntax with customized commands that allow a concise reproduction of the meta-theoretical mechanisms employed in the presentation of the target theory. This includes, for example, specialized commands for introducing new definitions and restricted variables, for which AOT imposes specific inferential roles and restrictions that otherwise could not be concisely captured by the existing infrastructure Isabelle provides.¹

As a result, we arrive at a customized theorem proving environment for AOT that guarantees to only accept valid reasoning according to AOT’s own deductive system and, in particular, avoids artifactual theorems. This is achieved by constructing a so-called abstraction layer that restricts automation to only rely on the reconstruction of the axioms and derivation rules of AOT, while barring the derivation of theorems that are mere artifacts of the underlying model construction. This enables the safe use of tools like sledgehammer for proving theorems of our target theory.

At the same time, we use a semantic representation in HOL as back-end, that is based on a newly developed extension of the partial, set-theoretic Aczel models (see [30]) of AOT. This allows for the experimental exploration of variations and extensions of the theory and its axiom system, while guaranteeing consistency relative to the meta-logic HOL.

This setup allowed us to significantly contribute to the evolution of our target theory, including the extension of its free logic, that was previously restricted to its individual terms, to relation terms, and the refinement of its axiom system, leading to an improved understanding of the conditions under which relations exist in the theory, which enabled new theoretical results in the construction of natural numbers.

By implementing Nodelman and Zalta’s construction of natural numbers as given in chapter 14 of [26] and verifying their derivation of the Dedekind-Peano postulates, we demonstrate that our method allows one to capture even complex constructions and reasoning in the target system.

The presentation of our work in [13] utilizes Isabelle’s document generation mechanism (see [25]), and thereby ensures that formal statements (apart from a few exceptions that are explicitly marked) are verified against the computerized implementation.

The technical implementation used as a basis for the thesis is preserved as an entry in the archive of formal proofs [12], which ensures that it will remain up-to-date with future changes to Isabelle/HOL and allows it to continue to be used as a basis for future explorations of the target theory.

Our work supports the use of SSEs as a powerful mechanism for universal logical reasoning that enables the application of existing automation infrastructure to new formalisms. We show that this remains feasible even if the target theory is based on logical foundations that significantly differ from the used meta-logic. Our method is general and can be applied to a multitude of logical systems, paving the way for future computational explorations of formalisms that so far may not have received the same attention in the development of automation infrastructure as classical approaches.

Furthermore, we strengthen the position of our target theory AOT as an expressive foundational theory that may serve as a philosophically grounded and logically structured basis for knowledge representation.

In this context, an interesting open question is the feasibility of an implementation of the generalized typed version of object theory, which not only involves abstract objects, but also abstract relations of arbitrary order and arity. This generalization is of particular interest, since it allows one to represent and analyze existing independent domain theories, like mathematical theories as ZF, themselves as abstract objects in a shared reasoning framework (see [15, 31, 32] and chapter 15 of PLM [33]).²

However, since the relative strength of this typed version of object theory may exceed that of ZF,³ and thereby that of HOL, a provably sound implementation using an SSE is likely to require the use of a stronger extension of Isabelle/HOL, as for example HOLZF [18] or beyond, as a basis and so far remains an unsolved challenge for future research.