Email Gateway (Aug 22 2022 at 16:09): Email Gateway (Aug 22 2022 at 16:09):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Representation and Partial Automation of the Principia Logico-Metaphysica in
Isabelle/HOL
by Daniel Kirchner
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.
For further details, see https://www.isa-afp.org/entries/PLM.html
Enjoy this new entry,
René
Last updated: Nov 21 2024 at 12:39 UTC