Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908528771334144 |
|---|---|
| author | Artale, Alessandro Hampson, Christopher Kontchakov, Roman Mazzullo, Andrea Wolter, Frank |
| author_facet | Artale, Alessandro Hampson, Christopher Kontchakov, Roman Mazzullo, Andrea Wolter, Frank |
| contents | While modal extensions of decidable fragments of first-order logic are usually undecidable, their monodic counterparts, in which formulas in the scope of modal operators have at most one free variable, are typically decidable. This only holds, however, under the provision that non-rigid constants, definite descriptions and non-trivial counting are not admitted. Indeed, several monodic fragments having at least one of these features are known to be undecidable. We investigate these features systematically and show that fundamental monodic fragments such as the two-variable fragment with counting and the guarded fragment of standard first-order modal logics $\mathbf{K}_{n}$ and $\mathbf{S5}_{n}$ are decidable. Tight complexity bounds are established as well. Under the expanding-domain semantics, we show decidability of the basic modal logic extended with the transitive closure operator on finite acyclic frames; this logic, however, is Ackermann-hard. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_08165 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions Artale, Alessandro Hampson, Christopher Kontchakov, Roman Mazzullo, Andrea Wolter, Frank Logic in Computer Science Logic While modal extensions of decidable fragments of first-order logic are usually undecidable, their monodic counterparts, in which formulas in the scope of modal operators have at most one free variable, are typically decidable. This only holds, however, under the provision that non-rigid constants, definite descriptions and non-trivial counting are not admitted. Indeed, several monodic fragments having at least one of these features are known to be undecidable. We investigate these features systematically and show that fundamental monodic fragments such as the two-variable fragment with counting and the guarded fragment of standard first-order modal logics $\mathbf{K}_{n}$ and $\mathbf{S5}_{n}$ are decidable. Tight complexity bounds are established as well. Under the expanding-domain semantics, we show decidability of the basic modal logic extended with the transitive closure operator on finite acyclic frames; this logic, however, is Ackermann-hard. |
| title | Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2509.08165 |