Dynamic Proof Theory for Dynamic Epistemic Logic

1. Introduction

• DEL models public, private, and other epistemic actions as events that transform models and agents’ information states.Its unified representation of knowledge-changing processes is a source of its expressive power.Source: §1 · p. 1
• Prior proof-theoretic approaches include tableaux, labelled calculi, and display calculi; Liu and Sano (2026) provide an S5-based treatment.In their S5 case, full cut elimination fails and cuts are restricted to an extended subformula closure.Source: §1 · p. 1
• The paper aims to capture DEL’s expressive strength over S5, internalize event-driven transformations syntactically, and establish full cut elimination.The approach avoids auxiliary semantic devices and reduction axioms.Source: §1 · p. 1
• The calculus extends a structural S5 hypersequent system, encoding reflexivity, transitivity, and symmetry in hypersequent structure rather than additional logical rules.This structural simplicity makes it a suitable basis for the dynamic extension.Source: §1 · p. 2
• Agent indices and an event store enrich dynamic hypersequents to represent epistemic transformations structurally; the calculus has invertible logical rules and admissible structural rules, including cut.The authors describe it as the first non-labelled sequent calculus that is both S5-based and inherently dynamic.Source: §1 · p. 2

2. Dynamic Epistemic Logic

• DEL formulas combine atomic propositions, negation, conjunction, agent-specific knowledge modalities, and event modalities.A pointed event model is also part of the language’s inductive construction.Source: §2 · p. 2
• The dynamic modality [eM]A requires A to hold after an executable event in the corresponding updated model and world.An event is executable when its precondition holds at the original world.Source: §2 · pp. 2–3
• An epistemic model consists of possible worlds, agents’ equivalence relations, and a valuation; an event model supplies event points, indistinguishability relations, and preconditions.The semantic definition simultaneously specifies truth and the updated model formed by the restricted modal product.Source: §2 · p. 3
• In the Mayread example, Anne may leave the letter unopened or read it; Bob cannot distinguish the three events, while Anne can.The event preconditions determine which events can occur in each original state.Source: §2 · pp. 3–4
• Event composition represents consecutive events, while [α]A denotes the successive application of the event modalities in sequence α.The section also defines prefixes and notation for the model obtained after successive updates.Source: §2 · pp. 4–5
• The Hilbert-style DEL system is presented through axioms and inference rules, and its derivability coincides with validity.The stated rules include modus ponens and necessitation.Source: §2 · p. 4

• Dynamic sequents distinguish a world across event-updated models with event-sequence labels, while vertical bars in dynamic hypersequents aggregate dynamic sequents as model worlds.Source: §3 · p. 5
• Agent-specific indices attach each world-component to its cell in each agent’s S5 partition and remain unchanged through updates while the world survives.Source: §3 · p. 7
• The event store records finite agent-indexed indistinguishability links among pointed event models and event variables, and requires every stored variable to be bound.Source: §3 · p. 9
• Because an index graph alone lacks an evaluation root, interpretation roots a disconnected unfolding at each world-component and conjoins the resulting interpretations.Source: §3 · pp. 9–10

3. Indexed Dynamic Hypersequents for DEL

• An assignment maps each event variable to a pointed event model while preserving the event store’s agent relations, then replaces variables in the hypersequent with their assigned models.The event models assigned to related variables must themselves satisfy the corresponding agent relation.Source: §3 · p. 11
• Interpretation quantifies over assignments to the event store; because the store has finitely many variables and event models are finite, there are finitely many assignments and their interpretations can be conjoined.Event variables are bound by pointed event models.Source: §3 · p. 11
• An indexed dynamic hypersequent with an event store is valid exactly when its instantiated hypersequent is valid for every assignment of pointed event models to the event variables.Each assignment specifies which pointed event models the event letters denote.Source: §3 · p. 11

4. The calculus 𝐈𝐃𝐇𝐒DEL

• Rule (eRK), read bottom-up, represents a false K_aA by an indistinguishable world that falsifies A in the updated model.The worlds share the agent’s information cell, and their event sequences are indistinguishable from that agent’s perspective.Source: §4 · p. 13
• Rules (eLK1)′ and (eLK2)′ connect knowledge to epistemic events by handling indistinguishable worlds across updates.For (eLK2)′, premises cover either failed preconditions at successive event stages or satisfaction of A at the resulting world.Source: §4 · p. 13
• Event rules introduce [⋅] on both sides of the sequent, while dynamic rules encode atomic permanence, event introduction, and precondition recall.Atomic permanence preserves an atom’s truth value across updates; New and Recall connect updated world-sequents to prior models and event preconditions.Source: §4 · p. 14
• The calculus includes propositional-event rules, and the paper demonstrates derivability of an atomic-permanence instance for a pointed event model.The propositional-event rules connect conjunction, events, and variables.Source: §4 · p. 14

5. Admissibility results

• Hypersequents containing the same formula on both sides of a dynamic sequent are derivable.Source: §5 · p. 14
• Internal, external, and dynamic weakening are height-preserving admissible, with introduced variables restricted to those already in the event store.Source: §5 · p. 15
• Merge is height-preserving admissible; semantically, it identifies indistinguishable worlds and corresponding event sequences, including their intermediate updated worlds.The event sequences are merged componentwise, with corresponding prefixes identified in intermediate updated models.Source: §5 · pp. 15–16
• The world-only and event-only Merge rules are height-preserving admissible, and the Newe rule is admissible.Source: §5 · p. 17
• All logical rules are height-preserving invertible in the calculus.The section also establishes height-preserving admissibility for weakening, contraction, and merge.Source: §5 · pp. 14, 18
• The contraction rules are height-preserving admissible.Source: §5 · p. 19

6. Soundness and Completeness

• Every formula derivable in the calculus is valid in DEL.Source: §6 · p. 20
• Soundness is proved by showing that the axioms are valid and the rules preserve validity.The proof uses the indexed hypersequent conditions to establish the required semantic relationships.Source: §6 · pp. 20–21
• Every DEL-valid formula is derivable in the calculus.Source: §6 · p. 23
• Completeness proceeds by deriving DEL axioms and showing modus ponens and necessitation admissible; event composition uses a derivability lemma.The proof uses Cut admissibility for modus ponens and external weakening for necessitation.Source: §6 · pp. 21, 23, 24

7. Cut admissibility

• Propositional, modal, event, and specified structural rules permute down across repeated (Rat) or (Lat) applications under the stated activity condition.An occurrence of (Rat) or (Lat) also permutes down across repeated applications of the same rule when the removed atom is inactive in those applications.Source: §7 · p. 24
• The Cut rule is admissible in the calculus.The proof uses induction on DHS-complexity of the cut formula, with a secondary induction on the sum of premise derivation heights.Source: §7 · p. 24
• When the cut formula is not principal in the last rule, the rule is reapplied after an admissible cut on its premise.For principal formulas, the proof separates propositional, modal, event, and dynamic rules; it treats modal and event cases in detail.Source: §7 · p. 25
• For dynamic-rule cases, the proof handles axioms, nonprincipal rules, and atoms principal in different dynamic sequents through contraction admissibility and inductive cuts.The final different-sequent case uses height-preserving contraction before cutting the atom.Source: §7 · p. 27

8. Conclusions

• Indexed dynamic hypersequents with an event store represent epistemic events directly in the proof system, capturing DEL dynamics without labels or relational atoms.The framework starts from the proof-theoretic treatment of multi-agent S5.Source: §8 · p. 28
• The calculus has admissible weakening, contraction, and merge rules, is sound and complete for DEL, and has an admissible cut rule.The authors describe it as the first proof-theoretic calculus for DEL over a classical S5 base with all structural rules, including contraction and cut, admissible.Source: §8 · p. 28
• Future work includes extending the approach to common or distributed knowledge and studying decidability, counter-model construction, proof-search optimisations, and complexity bounds.The authors also propose exploring the structural methodology in other dynamic modal logics with model transformations.Source: §8 · p. 28

A. Appendix

• In the three-premise (eLK2)′ case, the proof reduces cut admissibility through successive cuts on event-prefix formulas, using induction on formula complexity.The derivation repeatedly applies (DW) and (Newe) as it proceeds through the prefixes.Source: A. Appendix · pp. 28–29
• When an atom is principal in different dynamic components, the proof uses height-preserving contraction and an inductively admissible cut.The appendix gives the general case after describing the relevant (Rat) and (Lat) applications.Source: A. Appendix · p. 30
• In the example with k = 2 and l = 1, a novel cut on formula A follows an earlier cut, with admissible cuts justified by induction on the sum of heights.The derivation also applies (DW) and (Merge) to the premise of (eRK), then uses admissibility of (DW) and (Newe).Source: A. Appendix · pp. 29–30