Review of Symbolic Logic 13 (1):206-218 (2020)

Authors
Edward Zalta
Stanford University
Christoph Benzmueller
Freie Universität Berlin
Abstract
Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory that distinguishes between ordinary and abstract objects.This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms is simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics.Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics.
Keywords computational metaphysics  computer science
Categories (categorize this paper)
DOI 10.1017/s1755020319000297
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 53,548
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

A Formulation of the Simple Theory of Types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
Begriffschrift, eine der Arithmetischen nachgebildete Formelsprache des reinen Denkens.Gottlob Frege - 1879 - Revue Philosophique de la France Et de l'Etranger 8:108-109.
Principia Mathematica.Morris R. Cohen - 1912 - Philosophical Review 21 (1):87.
Intensional Models for the Theory of Types.Reinhard Muskens - 2007 - Journal of Symbolic Logic 72 (1):98-118.

View all 7 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
Logic in the 1930s: Type Theory and Model Theory.Georg Schiemer & Erich H. Reck - 2013 - Bulletin of Symbolic Logic 19 (4):433-472.
Quantification Theory in *9 of Principia Mathematica.Gregory Landini - 2000 - History and Philosophy of Logic 21 (1):57-77.
A Transfinite Type Theory with Type Variables. [REVIEW]J. M. P. - 1966 - Review of Metaphysics 20 (1):144-144.
An Overview of Type Theories.Nino Guallart - 2015 - Axiomathes 25 (1):61-77.
The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Steps Toward a Computational Metaphysics.Branden Fitelson & Edward N. Zalta - 2007 - Journal of Philosophical Logic 36 (2):227-247.

Analytics

Added to PP index
2020-03-21

Total views
18 ( #540,951 of 2,348,445 )

Recent downloads (6 months)
7 ( #99,301 of 2,348,445 )

How can I increase my downloads?

Downloads

My notes