Simple Type Theory as Framework for Combining Logics

TL;DR

This paper demonstrates that simple type theory serves as an effective and expressive framework for embedding, combining, and reasoning about various classical and non-classical logics, supported by existing reasoning tools.

Contribution

It shows that simple type theory can elegantly embed and combine multiple logics, providing a uniform reasoning approach with well-understood semantics.

Findings

Prominent logics can be embedded in simple type theory

Simple type theory models combinations of embedded logics

Existing reasoning systems can be used for logic reasoning within this framework

Abstract

Simple type theory is suited as framework for combining classical and non-classical logics. This claim is based on the observation that various prominent logics, including (quantified) multimodal logics and intuitionistic logics, can be elegantly embedded in simple type theory. Furthermore, simple type theory is sufficiently expressive to model combinations of embedded logics and it has a well understood semantics. Off-the-shelf reasoning systems for simple type theory exist that can be uniformly employed for reasoning within and about combinations of logics.