{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,26]],"date-time":"2025-12-26T14:26:51Z","timestamp":1766759211822},"reference-count":18,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T00:00:00Z","timestamp":1562889600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2020,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Principia Logico-Metaphysica<\/jats:italic> contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory (inspired by ideas of Ernst Mally, formalized by Zalta) that distinguishes between ordinary and abstract objects.<\/jats:p><jats:p>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\u2019s 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, <jats:italic>computational metaphysics<\/jats:italic>.<\/jats:p><jats:p>Our results were made technically possible by a suitable adaptation of Benzm\u00fcller\u2019s 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.<\/jats:p>","DOI":"10.1017\/s1755020319000297","type":"journal-article","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T09:58:30Z","timestamp":1562925510000},"page":"206-218","source":"Crossref","is-referenced-by-count":5,"title":["MECHANIZING <i>PRINCIPIA LOGICO-METAPHYSICA<\/i> IN FUNCTIONAL TYPE-THEORY"],"prefix":"10.1017","volume":"13","author":[{"given":"DANIEL","family":"KIRCHNER","sequence":"first","affiliation":[]},{"given":"CHRISTOPH","family":"BENZM\u00dcLLER","sequence":"additional","affiliation":[]},{"given":"EDWARD N.","family":"ZALTA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"S1755020319000297_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-6980-3"},{"key":"S1755020319000297_ref16","author":"Zalta","year":"2018","journal-title":"Principia Logico-Metaphysica"},{"key":"S1755020319000297_ref15","author":"Wiedijk","journal-title":"The de Bruijn factor"},{"key":"S1755020319000297_ref11","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1174668386"},{"key":"S1755020319000297_ref9","volume-title":"Open Philosophy (Special Issue\u2014Computer Modeling in Philosophy)","author":"Kirchner","year":"2019"},{"key":"S1755020319000297_ref8","article-title":"Representation and partial automation of the principia logico-metaphysica in Isabelle\/HOL","author":"Kirchner","year":"2017","journal-title":"Archive of Formal Proofs"},{"key":"S1755020319000297_ref7","volume-title":"The Stanford Encyclopedia of Philosophy (Winter 2018 Edition)","author":"Hieke","year":"2018"},{"key":"S1755020319000297_ref6","volume-title":"Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens","author":"Frege","year":"1879"},{"key":"S1755020319000297_ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2214691"},{"key":"S1755020319000297_ref4","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S1755020319000297_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2018.10.008"},{"key":"S1755020319000297_ref12","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","volume":"Vol. 2283","author":"Nipkow","year":"2002"},{"key":"S1755020319000297_ref14","volume-title":"Principia Mathematica","author":"Whitehead","year":"1910\u20131913"},{"key":"S1755020319000297_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10670-013-9565-x"},{"key":"S1755020319000297_ref10","volume-title":"The Stanford Encyclopedia of Philosophy (Summer 2019 Edition)","author":"Linsky","year":"2019"},{"key":"S1755020319000297_ref13","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq017"},{"key":"S1755020319000297_ref2","first-page":"3","volume-title":"On Being and Saying","author":"Boolos","year":"1987"},{"key":"S1755020319000297_ref18","volume-title":"Intensional Logic and the Metaphysics of Intentionality","author":"Zalta","year":"1988"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020319000297","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,20]],"date-time":"2020-03-20T08:24:28Z","timestamp":1584692668000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020319000297\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,12]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["S1755020319000297"],"URL":"https:\/\/doi.org\/10.1017\/s1755020319000297","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,12]]}}}