Knowledge forgetting: properties and applications (Q1045992)

The concept of `forgetting' an elementary letter in a propositional formula has a neat syntactic definition in the context of classical logic: just take the disjunction of the result of substituting the falsum and the truum respectively in the formula. But this definition is not suitable in nonclassical contexts, in particular modal ones. For example, in the modal logic S5, such an operation applied to a formula expressing the contingency of a letter would give a contradiction. In the last few years a semantic definition of forgetting a letter in a formula of S5 (called knowledge forgetting) has gained acceptance, but to now it has lacked a syntactic characterization. This paper fills the gap, giving four sound postulates and proving their completeness. It goes on to compare forgetting in S5 with updating in the same context as the latter is defined in an earlier paper of \textit{C. Baral} and \textit{Y. Zhang} [``Knowledge updates: Semantics and complexity issues'', Artif. Intell. 164, No.~1--2, 209--243 (2005; Zbl 1132.68720)]. The most straightforward way of defining update from forgetting in the S5 context fails to satisfy the Katsuno-Mendelzon postulate (U8); but a more complex definition is formulated and shown to yield all of those postulates, at least in the finite case. Finally, the paper studies an application of the notion of forgetting in the S5 context, to the analysis of a certain game with bounded memory.