## Abstract

We develop a cut-free nested sequent calculus as basis for a proof search procedure for an intuitionistic modal logic of actions and propositions. The actions act on propositions via a dynamic modality (the *weakest precondition* of program logics), whose left adjoint we refer to as “update” (the *strongest postcondition*). The logic has agent-indexed adjoint pairs of epistemic modalities: the left adjoints encode agents’ uncertainties and the right adjoints encode their beliefs. The rules for the “update” modality encode learning as a result of discarding uncertainty. We prove admissibility of *Cut*, and hence the soundness and completeness of the logic with respect to an algebraic semantics. We interpret the logic on epistemic scenarios that consist of honest and dishonest communication actions, add assumption rules to encode them, and prove that the

calculus with the assumption rules still has the admissibility results. We apply the calculus to encode (and allow reasoning about) the classic epistemic puzzles of

*dirty children* (aka “muddy children”) and *drinking logicians* and some versions with dishonesty or noise; we also give an application where the actions are movements of a robot rather than announcements.

Original language | English |
---|---|

Article number | 34 |

Number of pages | 38 |

Journal | ACM Transactions on Computational Logic |

Volume | 14 |

Issue number | 4 |

DOIs | |

Publication status | Published - Nov 2013 |

## Keywords

- Proof theory
- Cut admissibility
- Algebra
- Adjoint modalities
- actions
- Adjoint modal operators