DECIDABILITY OF INDEPENDENCE-FRIENDLY MODAL LOGIC

In this paper we consider an independence-friendly modal logic, IFML. It follows from results in the literature that qua expressive power, IFML is a fragment of second-order existential logic, E|, that cannot be translated into first-order logic. It is also known that IFML lacks the tree structure property. We show that IFML has the ʹtruncated structure propertyʹ, a weaker version of the tree structure property, and that its satisfiability problem is solvable in 2NEXP. This implies that this paper reveals a new decidable fragment of E J. We also show that IFML becomes undecidable if we add the identity symbol to its vocabulary by means of a reduction from the tiling problem.