A Decidable Fragment of First Order Modal Logic: Two Variable Term Modal Logic

First order modal logic (FOML) is built by extending First Order Logic (FO) with modal operators. A typical formula is of the form for all chi there exists y square P(x, y). Not only is FOML undecidable, even simple fragments like that of restriction to unary predicate symbols, guarded fragment and two variable fragment, which are all decidable for FO become undecidable for FOML. In this paper we study Term Modal logic (TML) which allows modal operators to be indexed by terms. A typical formula is of the form for all chi there exists y square P-x(x, y). There is a close correspondence between TML and FOML and we explore this relationship in detail in the paper. In contrast to FOML, we show that the two variable fragment (without constants, equality) of TML is decidable. Further, we prove that adding a single constant makes the two variable fragment of TML undecidable. On the other hand, when equality is added to the logic, it loses the finite model property.