Skip to content

Research at St Andrews

Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators

Research output: Contribution to journalArticle



Roy Dyckhoff, Mehrnoosh Sadrzadeh, Julien Truffaut

School/Research organisations


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 languageEnglish
Article number34
Number of pages38
JournalACM Transactions on Computational Logic
Issue number4
Publication statusPublished - Nov 2013

    Research areas

  • Proof theory, Cut admissibility, Algebra, Adjoint modalities, actions, Adjoint modal operators

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Contraction-free sequent calculi in intuitionistic logic: a correction

    Dyckhoff, R., Dec 2018, In : Journal of Symbolic Logic. 83, 4, p. 1680-1682 3 p.

    Research output: Contribution to journalArticle

  2. Indefinite proof and inversions of syllogisms

    Dyckhoff, R., 14 Jul 2018, (Accepted/In press) In : Bulletin of Symbolic Logic. 13 p.

    Research output: Contribution to journalArticle

  3. Analyticity, balance and non-admissibility of Cut in Stoic Logic

    Bobzien, S. & Dyckhoff, R., 20 Apr 2018, In : Studia Logica. First Online, 23 p.

    Research output: Contribution to journalArticle

  4. Intuitionistic decision procedures since Gentzen

    Dyckhoff, R., 5 May 2016, Advances in Proof Theory. Kahle, R., Strahm, T. & Studer, T. (eds.). Birkhäuser Basel, p. 245-267 (Progress in Computer Science and Applied Logic; vol. 28).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

Related by journal

  1. Foundational certified code in the Twelf metalogical framework

    Crary, K. & Sarkar, S., 2008, In : ACM Transactions on Computational Logic. 9, 3, 26 p., ARTN 16.

    Research output: Contribution to journalArticle

ID: 110579706