On the basic one-agent achievement-stit theory
Nuel Belnap, Michael Perloff, Ming Hui Xu · 2001
Abstract It turns out that this equivalence is valid for every BT+ AC structure for dstit, and it is valid for every BT+ I+ AC structure for astit iff the structure contains no busy choice sequences, and is therefore a BT+ I+ AC+ nbc structure; see chapter 15 and chapter 18 for details. (BT+ AC, BT+ I+ AC, and BT+ I+ AC+ nbc structures are defined in §2.) We showed in chapter 15 that the astit theory with a single agent and the refref equivalence (i.e., the set of all sentences, with a single agent term, valid for all BT+ I+ AC+ nbc structures) is decidable. The purpose of this chapter is to remove the no-busy-choice-sequence restriction and give an axiomatization for the resulting basic logic of astit.