Formalization of Metaphysical Arguments in Higher-Order Modal Logics
Research areas
Description
Outline
Philosophy (especially Metaphysics) is full of interesting arguments whose formalization and automated verification require very expressive logics, capable of dealing with modalities and higher-order quantification.
One prominent example is Gödel's ontological argument (https://github.com/FormalTheology/GoedelGod/), which has been recently analyzed with the assistance of automated and interactive theorem provers. There are many variations of this argument and many possible variations of the underlying logics.
Goals of this project
This project will investigate and formalize variants of ontological arguments within various higher-order modal logics. Besides verifying the logical (in)correctness of such arguments, this project will also generate benchmarks for higher-order and modal theorem provers. Different embeddings of modal logics into higher-order logics will be tried and their efficiency will be evaluated and compared.
Requirements/Prerequisites
Some background in logic. Interest in philosophy.
Student Gain
Become acquainted with automated and intereactive theorem provers; gain experience in higher-order and modal logics; publish papers about the formalizations.
Background Literature
Our papers are available at: https://github.com/FormalTheology/GoedelGod/
Links
Our Coq, Isabelle and TPTP THF formalizations are available at: https://github.com/Paradoxika/Skeptik