Quantified Multimodal Logics in Simple Type Theory

TL;DR

This paper introduces a simple embedding of quantified multimodal logic into simple type theory, enabling automated reasoning and proofs using existing higher-order theorem provers.

Contribution

It provides a novel embedding method that facilitates automated reasoning in quantified multimodal logic within simple type theory.

Findings

Embedding is sound and complete.

Automated proofs are achievable with existing theorem provers.

The approach enables reasoning about meta properties of multimodal logic.

Abstract

We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple experiments, using existing higher-order theorem provers, to demonstrate that the embedding allows automated proofs of statements in these logics, as well as meta properties of them.