Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions

Organizzato da: Eugenio Orlandelli
In collaborazione con: Guido Gherardi

Mentre le estensioni modali di frammenti decidibili della logica del primo ordine sono generalmente indecidibili, le loro controparti monodiche, in cui le formule nel campo degli operatori modali hanno al massimo una variabile libera, sono tipicamente decidibili. Questo vale, però, solo a condizione che non siano ammesse costanti non rigide, descrizioni definite e conteggi non banali. Infatti, diversi frammenti monodici che presentano almeno una di queste caratteristiche sono noti per essere indecidibili. I nostri risultati più recenti su queste caratteristiche (frutto di un lavoro congiunto con Alessandro Artale, Christopher Hampson, Roman Kontchakov e Frank Wolter) mostrano che frammenti monodici fondamentali delle logiche modali del primo ordine standard K_n e S5_n, come il frammento a due variabili con conteggio e il frammento guarded, sono decidibili. Sono inoltre stabiliti limiti precisi di complessità. Sotto la semantica a domini in espansione, dimostriamo la decidibilità (anche se con un limite inferiore non primitivo-ricorsivo) della logica modale di base estesa con l’operatore di chiusura transitiva su frame finiti aciclici.

---

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. Our recent results on these features (from a joint work with Alessandro Artale, Christopher Hampson, Roman Kontchakov, and Frank Wolter) show that fundamental monodic fragments of standard first-order modal logics K_n and S5_n, such as the two-variable fragment with counting and the guarded fragment, are decidable. Tight complexity bounds are established as well. Under the expanding-domain semantics, we show decidability (albeit with a non primitive-recursive lower bound) of the basic modal logic extended with the transitive closure operator on finite acyclic frames.