Mechanizing Principia Logico-Metaphysica in Functional Type Theory


Authors
Edward Zalta
Stanford University
Christoph Benzmueller
Freie Universität Berlin
Abstract
*Principia Logico-Metaphysica* (a developing, online manuscript) contains a foundational logical theory for metaphysics, mathematics, and the sciences. It contains a canonical development of Abstract Object Theory [AOT], a metaphysical theory (inspired by ideas of Ernst Mally, formalized by Zalta) that differentiates 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\"uller's metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables the fruitful reuse of 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 own   Higher Order Logic   Universal Reasoning   Rational Argumentation   Human-Machine Interaction
Categories (categorize this paper)
Reprint years 2018
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 42,401
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

Begriffschrift, eine der Arithmetischen nachgebildete Formelsprache des reinen Denkens.Gottlob Frege - 1879 - Revue Philosophique de la France Et de l'Etranger 8:108-109.
[Omnibus Review].Alonzo Church - 1945 - Journal of Symbolic Logic 10 (4):132-133.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Higher Order Modal Logic.Reinhard Muskens - 2006 - In Patrick Blackburn, Johan Van Benthem & Frank Wolter (eds.), Handbook of Modal Logic. Elsevier. pp. 621-653.
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.
Pushing the Bounds of Rationality: Argumentation and Extended Cognition.David Godden - 2016 - In Fabio Paglieri, Laura Bonelli & Silvia Felletti (eds.), The psychology of argument: Cognitive approaches to argumentation and persuasion. London: College Publications. pp. 67-83.
Logic and Social Cognition.Rineke Verbrugge - 2009 - Journal of Philosophical Logic 38 (6):649-680.

Analytics

Added to PP index
2017-12-04

Total views
33 ( #250,854 of 2,255,372 )

Recent downloads (6 months)
22 ( #35,585 of 2,255,372 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature