Logic for update products and steps into the past

AbstractThis paper provides a sound and complete proof system for a language Le+Y that adds to Dynamic Epistemic Logic (DEL) a discrete previous-time operator as well as single symbol formulas that partially reveal the most recent event that occurred. The completeness theorem is by filtration followed by model unraveling and other model transformations. Decidability follows from the completeness proof. The degree to which it is important to include the additional single symbol formulas is addressed in a discussion about the difficulties of the completeness for a language LY that only adds the previous-time operator to DEL. Discussion is also given regarding the completeness for a language obtained by removing common knowledge operators from Le+Y