Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators
Roy Dyckhoff, Mehrnoosh Sadrzadeh, Julien Truffaut · ACM Transactions on Computational Logic · 2013
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 (theweakest preconditionof program logics), whose left adjoint we refer to as “update” (thestrongest 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 ofCut, 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 ofdirty children(a.k.a. “muddy children”) anddrinking logiciansand some versions with dishonesty or noise; we also give an application where the actions are movements of a robot rather than announcements.