Decidability of many-agent deliberative-stit theories
Nuel Belnap, Michael Perloff, Ming Hui Xu · 2001
Abstract In this chapter we give an axiomatization, Ldm, for the basic dstit logic, and prove its completeness and decidability by way of the finite model property. It is surely very natural to combine dstit theory with indeterminist tense logics, especially when we consider deliberative seeing to something to be connected with what the future will be like. In carrying out some basic technical work in dstit theory, however, we will use a formal language without tense operators, though we will use the historical necessity operator Sett:, §8F.4, as a primitive. In our formal language, we will introduce Chellas’s cstit operator, §8G.2, as an abbreviation, just as in §llA. The reader familiar with modal logic can easily see that the Chellas 1992 theory of cstit is decidable, since Chellas did not propose any condition concerning the relation among different agents.