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