# Two variable fragment of Term Modal Logic

## TL;DR

This paper proves that a specific two-variable fragment of Term Modal Logic is decidable, contrasting with the undecidability of similar fragments in first-order modal logic.

## Contribution

It establishes the decidability of the two-variable fragment of Term Modal Logic, a notable exception in the landscape of undecidable modal logics.

## Key findings

- Two-variable fragment of TML is decidable.
- Contrasts with undecidability of two-variable first-order modal logic.
- Provides a new decidability result for complex modal logics.

## Abstract

Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form $\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$. Like First order modal logic, TML is also "notoriously" undecidable, in the sense that even very simple fragments are undecidable. In this paper, we show the decidability of one interesting fragment, that of two variable TML. This is in contrast to two-variable First order modal logic, which is undecidable.