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

2023/07/06 by Mikhail Rybakov, Dmitry Shkatov, Rybakov, M. +1
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Logic, Reasoning, and Knowledge

paper · pdf · doi:10.48550/arxiv.2307.02805

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.

Related

• Modelling of logical systems by means of their fragments
• Superintuitionistic predicate logics of linear frames: undecidability with two individual variables
• The Succinctness of First-order Logic over Modal Logic via a Formula Size Game
• Decidable fragments of first-order modal logics with counting quantifiers over varying domains
• Algorithmic complexity of monadic multimodal predicate logics with equality over finite Kripke frames