English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The present paper provides an analysis of the existing proof systems fordynamic epistemic logic from the viewpoint of proof-theoretic semantics.Dynamic epistemic logic is one of the best known members of a family of logicalsystems which have been successfully applied to diverse scientific disciplines,but the proof theoretic treatment of which presents many difficulties. After anillustration of the proof-theoretic semantic principles most relevant to thetreatment of logical connectives, we turn to illustrating the main features ofdisplay calculi, a proof-theoretic paradigm which has been successfullyemployed to give a proof-theoretic semantic account of modal and substructurallogics. Then, we review some of the most significant proposals of proof systemsfor dynamic epistemic logics, and we critically reflect on them in the light ofthe previously introduced proof-theoretic semantic principles. Thecontributions of the present paper include a generalisation of Belnap's cutelimination metatheorem for display calculi, and a revised version of thedisplay-style calculus D.EAK. We verify that the revised version satisfies thepreviously mentioned proof-theoretic semantic principles, and show that itenjoys cut elimination as a consequence of the generalised metatheorem.

A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic