Decidability of independence-friendly modal logic (Q6829281)

This paper studies a certain `modal fragment' (IFML) of independence-friendly first-order logic, or, more precisely, a fragment of the variant of the latter that \textit{W. Hodges} [``Logics of imperfect information: why sets of assignments?'', Texts in Logic and Games 1, 117--133 (2007; Zbl 1203.03036)] has proposed to call slash logic. It is well known that sentences of slash logic have the same expressive power as sentences of existential second-order logic (ESO). The logic IFML is polymodal and it admits independence indications of the form \((O/W)\), where \(O\) may be either a quantifier or a propositional connective (disjunction or conjunction construed as a restricted quantifier over a finite index set) and \(W\) may contain both variables bound by syntactically preceding quantifiers and indices bound by syntactically preceding junctions.\N\NIt was proven in [\textit{T. Tulenheimo} and \textit{M. Sevenster}, ``Approaches to independence friendly modal logic'', Texts in Logic and Games 1, 247--280 (2007; Zbl 1203.03041)] that there is no truth-preserving translation of IFML into first-order logic. (On p. 416 the author erroneously attributes this proof to another paper by Tulenheimo and Sevenster.) This untranslatability result makes the main result of Sevenster's paper interesting: a fragment of ESO is disclosed whose satisfiability problem is decidable in non-deterministic double exponential time. The proof method yields as a corollary an analogue of the tree model property of basic modal logic: every satisfiable formula of IFML is true in a `truncated structure', i.e., a structure whose domain can be partitioned into some finite number \(n\) of layers \(L_i\) (\(1 \leq i \leq n\)) such that any pair belonging to the interpretation of a relation symbol belongs to some set \(L_i \times L_{i+1}\).\N\NThe author also takes up the result to the effect that adding identity among the accessibility relations of IFML yields a logic with an undecidable satisfiability problem. He mentions that this result appeared earlier in his Ph.D. thesis (2006). What he does not mention is that it stems from an unpublished manuscript of \textit{T. Hyttinen} and \textit{T. Tulenheimo} [``Decidability and undecidability results for some IF modal logics'', University of Helsinki (2005)] made privately available to the author in 2005.