English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Principia Logico-Metaphysica contains a foundational logical theory formetaphysics, mathematics, and the sciences. It includes a canonical developmentof Abstract Object Theory [AOT], a metaphysical theory (inspired by ideas ofErnst Mally, formalized by Zalta) that distinguishes between ordinary andabstract objects.  This article reports on recent work in which AOT has been successfullyrepresented 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 ofcomplex terms is simply adjoined to AOT's specially-formulated comprehensionprinciple for relations. This result constitutes a new and important paradox,given how much expressive and analytic power is contributed by having the twokinds of complex terms in the system. Its discovery is the highlight of ourjoint project and provides strong evidence for a new kind of scientificpractice in philosophy, namely, computational metaphysics.  Our results were made technically possible by a suitable adaptation ofBenzm\"uller's metalogical approach to universal reasoning by semanticallyembedding theories in classical higher-order logic. This approach enables oneto reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL,for mechanizing and experimentally exploring challenging logics and theoriessuch as AOT. Our results also provide a fresh perspective on the question ofwhether relational type theory or functional type theory better serves as afoundation for logic and metaphysics.

Mechanizing Principia Logico-Metaphysica in Functional Type Theory