Kripke trick and decidability of monadic fragments of modal and superintuitionistic logics

TL;DR

This paper explores modifications of the Kripke trick to analyze the decidability of monadic fragments in modal and superintuitionistic logics, providing algorithmic upper bounds and identifying limitations.

Contribution

It introduces modified Kripke techniques for monadic fragments and establishes decidability bounds for certain modal and superintuitionistic logics.

Findings

Modified Kripke trick for monadic formulas

Decidability bounds for specific logics

Limitations of the Kripke trick in certain cases

Abstract

We discuss the modifications of the Kripke trick simulating binary predicate letters of classical first-order formulas with monadic modal first-order formulas and the situations where the trick does not work. As a result, we obtain results on algorithmic upper bounds for monadic fragments of some modal and superintuitionistic first-order logics.