We present an embedding of the second-order fragment of the
Theory of Abstract Objects as described in Edward Zalta's
upcoming work Principia
Logico-Metaphysica (PLM) in the automated reasoning
framework Isabelle/HOL. The Theory of Abstract Objects is a
metaphysical theory that reifies property patterns, as they for
example occur in the abstract reasoning of mathematics, as
abstract objects and provides an axiomatic
framework that allows to reason about these objects. It thereby serves
as a fundamental metaphysical theory that can be used to axiomatize
and describe a wide range of philosophical objects, such as Platonic
forms or Leibniz' concepts, and has the ambition to function as a
foundational theory of mathematics. The target theory of our embedding
as described in chapters 7-9 of PLM employs a modal relational type
theory as logical foundation for which a representation in functional
type theory is known to
be challenging. Nevertheless we arrive
at a functioning representation of the theory in the functional logic
of Isabelle/HOL based on a semantical representation of an Aczel-model
of the theory. Based on this representation we construct an
implementation of the deductive system of PLM which allows to
automatically and interactively find and verify theorems of PLM.
Our work thereby supports the concept of shallow
semantical embeddings of logical systems in HOL as a universal tool
for logical reasoning as
promoted by Christoph Benzmüller.
The most notable result of the presented work is the
discovery of a previously unknown paradox in the formulation of the
Theory of Abstract Objects. The embedding of the theory in
Isabelle/HOL played a vital part in this discovery. Furthermore it was
possible to immediately offer several options to modify the theory to
guarantee its consistency. Thereby our work could provide a
significant contribution to the development of a proper grounding for
object theory. |