Decision problem of some bundled FOML fragments

TL;DR

This paper investigates the decidability of various bundled fragments of First-Order Modal Logic (FOML) over different domain interpretations, extending known results and identifying new decidability and undecidability boundaries.

Contribution

It extends the understanding of decidability for bundled FOML fragments, showing that certain new combinations are decidable or undecidable under specific domain assumptions.

Findings

orallox and oxorall bundled fragments are decidable over increasing domains.

oxorall bundled fragment is undecidable over constant domains.

oxorall^2 extension is undecidable over constant domains.

Abstract

Over increasing domain interpretations, \exists\Box and \forall\Box bundled fragments are decidable and over constant domain interpretations, \exists\Box bundled fragment is decidable while \forall\Box bundled fragment is undecidable. Based on the existing results,we show that over increasing domain interpretations, \Box\exists and \Box\forall bundled fragments are decidable as well. On the other hand, over constant domain interpretations, \Box\forall bundled fragment is undecidable and \Box\exists^2 bundled fragment, an extension of \Box\exists bundled fragment, is undecidable neither.