
doi: 10.1145/3593584
First order modal logic (饾枼饾柈饾柆饾柅) is built by extending First Order Logic (饾枼饾柈) with modal operators. A typical formula is of the form \(\forall x \exists y \Box P(x,y)\) . Not only is 饾枼饾柈饾柆饾柅 undecidable, even simple fragments like that of restriction to unary predicate symbols, guarded fragment and two variable fragment, which are all decidable for 饾枼饾柈 become undecidable for 饾枼饾柈饾柆饾柅. In this paper we study Term Modal logic (饾柍饾柆饾柅) which allows modal operators to be indexed by terms. A typical formula is of the form \(\forall x \exists y~\Box _x P(x,y)\) . There is a close correspondence between 饾柍饾柆饾柅 and 饾枼饾柈饾柆饾柅 and we explore this relationship in detail in the paper. In contrast to 饾枼饾柈饾柆饾柅, we show that the two variable fragment (without constants, equality) of 饾柍饾柆饾柅 is decidable. Further, we prove that adding a single constant makes the two variable fragment of 饾柍饾柆饾柅 undecidable. On the other hand, when equality is added to the logic, it loses the finite model property.
two variable fragment, Logic in computer science, normal form, decidability, term modal logic, equality, Computer science
two variable fragment, Logic in computer science, normal form, decidability, term modal logic, equality, Computer science
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
