Full and relative awareness: A decidable logic for reasoning about knowledge of unawareness, in: Theoretical Aspects of Rationality and Knowledge

In the most popular logics combining knowl-edge and awareness, it is not possible to express statements about knowledge of unawareness such as “Ann knows that Bill is aware of something Ann is not aware of” – without using a stronger statement such as “Ann knows that Bill is aware of p and Ann is not aware of p”, for some particu-lar p. Recently, however, Halpern and Rêgo (2006) introduced a logic in which such state-ments about knowledge of unawareness can be expressed. The logic extends the tradi-tional framework with quantification over for-mulae, and is thus very expressive. As a con-sequence, it is not decidable. In this paper we introduce a decidable logic which can be used to reason about certain types of unawareness. The logic extends the traditional framework with an operator expressing full awareness, i.e., the fact that an agent is aware of every-thing, and another operator expressing rel-ative awareness, the fact that one agent is aware of everything another agent is aware of. The logic is less expressive than Halpern’s and Rêgo’s logic. It is, however, expressive enough to express all of Halpern’s and Rêgo’s motivating examples. In addition to proving that the logic is decidable and that its sat-isfiability problem is PSPACE-complete, we present an axiomatisation which we show is sound and complete.