Mechanizing Principia Logico-Metaphysica in functional type-theory.

*(English)*Zbl 07181947Summary: 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 (inspired by ideas of Ernst Mally, formalized by Zalta) 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.

##### MSC:

03A05 | Philosophical and critical aspects of logic and foundations |

03B35 | Mechanization of proofs and logical operations |

03B45 | Modal logic (including the logic of norms) |

03B60 | Other nonclassical logic |

03B80 | Other applications of logic |

68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |

68T27 | Logic in artificial intelligence |

68T30 | Knowledge representation |

##### Keywords:

computational metaphysics; abstract object theory; shallow semantical embedding; higher-order logic; theorem proving; universal reasoning
PDF
BibTeX
XML
Cite

\textit{D. Kirchner} et al., Rev. Symb. Log. 13, No. 1, 206--218 (2020; Zbl 07181947)

Full Text:
DOI

##### References:

[1] | Benzmüller, C. (2019). Universal (meta-)logical reasoning: Recent successes. Science of Computer Programming, 172, 48-62. |

[2] | Boolos, G. (1987). The consistency of Frege’s foundations of arithmetic. In Thomson, J., editor. On Being and Saying. Cambridge, MA: MIT Press, pp. 3-20. |

[3] | Bueno, O., Menzel, C., & Zalta, E. N. (2014). Worlds and propositions set free. Erkenntnis, 79, 797-820. · Zbl 1304.03015 |

[4] | Church, A. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2), 56-68. · JFM 66.1192.06 |

[5] | Clark, R. (1978). Not every object of thought has being: A paradox in naive predication theory. Noûs, 12(2), 181-188. · Zbl 1366.03041 |

[6] | Frege, G. (1879). Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle: Verlag von Louis Nebert. |

[7] | Hieke, A. & Zecha, G. (2018). Ernst Mally. In Zalta, E. N., editor. The Stanford Encyclopedia of Philosophy (Winter 2018 Edition). Metaphysics Research Lab, Stanford University. |

[8] | Kirchner, D. (2017). Representation and partial automation of the principia logico-metaphysica in Isabelle/HOL. Archive of Formal Proofs, http://isa-afp.org/entries/PLM.html. |

[9] | Kirchner, D., Benzmüller, C., & Zalta, E. N. (2019). Computer science and metaphysics: A cross-fertilization.Open Philosophy (Special Issue—Computer Modeling in Philosophy), forthcoming, doi: 10.1515/opphil-2019-0015, preprint: https://arxiv.org/abs/1905.00787. |

[10] | Linsky, B. & Irvine, A. D. (2019). Principia mathematica. In Zalta, E. N., editor. The Stanford Encyclopedia of Philosophy (Summer 2019 Edition). Metaphysics Research Lab, Stanford University. |

[11] | Muskens, R. (2007). Intensional models for the theory of types. The Journal of Symbolic Logic, 72(1), 98-118. · Zbl 1116.03008 |

[12] | Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Berlin: Springer-Verlag. · Zbl 0994.68131 |

[13] | Oppenheimer, P. E. & Zalta, E. N. (2011). Relations versus functions at the foundations of logic: Type-theoretic considerations. Journal of Logic and Computation, 21(2), 351-374. · Zbl 1234.03007 |

[14] | Whitehead, A. N. & Russell, B. (1910-1913). Principia Mathematica (first edition). Cambridge: Cambridge University Press. · JFM 61.0061.03 |

[15] | Wiedijk, F.The de Bruijn factor. Available at: http://www.cs.ru.nl/F.Wiedijk/factor/factor.pdf/. · Zbl 1114.03007 |

[16] | Zalta, E. N. (2018). Principia Logico-Metaphysica. Available at: http://mally.stanford.edu/principia.pdf (Draft/Excerpt). |

[17] | Zalta, E. N. (1983). Abstract Objects: An Introduction to Axiomatic Metaphysics. Dordrecht: D. Reidel. |

[18] | Zalta, E. N. (1988). Intensional Logic and the Metaphysics of Intentionality. Cambridge, MA: MIT Press. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.