A decidable fragment of first order modal logic: two variable term modal logic

Padmanabha, Anantha and Ramanujam, R (2023) A decidable fragment of first order modal logic: two variable term modal logic. ACM Transactions on Computational Logic. pp. 1-37.

Text - Accepted Version
Restricted to Repository staff only
Download (1MB) | Request a copy

Abstract

First order modal logic (FOML) is built by extending First Order Logic (FO) with modal operators. A typical formula is of the form ∀x∃y□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 ∀x∃y □xP(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 looses the finite model property.

Item Type:

Article

Authors:

Padmanabha, Anantha and Ramanujam, R

Document Language: