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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Dynamic Logics (DLs) form a large family of nonclassical logics, and perhaps the one enjoying the widest range of applications. Indeed, they are designed to formalize change caused by actions of diverse nature: updates on the memory state of a computer, displacements of moving robots in an environment, measurements in models of quantum physics, belief revisions, knowledge updates, etc. In each of these areas, DL-formulas express properties of the model encoding the present state of affairs, as well as the preand post-conditions of a given action. Actions are semantically represented as transformations of one model into another, encoding the state of affairs after the action has taken place. DL-languages are expansions of classical (static) logic with dynamic operators, parametrized with actions; dynamic operators are modalities interpreted in terms of the transformation of models corresponding to their action-parameters. However, when dynamic logics feature both dynamic and ‘static’ modalities, as in the case of the Dynamic Epistemic Logics (DEL), they typically lose many desirable properties, such as the closure under uniform substitution, which facilitate a smooth algebraic and proof-theoretic treatment. This and other difficulties make their algebraic and proof-theoretic theory presently underdeveloped, and the few existing proposals seem quite ad hoc: in particular, no proposed calculus in the literature enjoys the minimal conditions enabling the specification of the meaning of a logical symbol in the sense of proof-theoretic semantics. We developed a family of display-style, cut-free sequent calculi for dynamic epistemic logics on both an intuitionistic and a classical base [7]. Like the standard display calculi, these calculi are modular: just by modifying the structural rules according to Dosen’s principle [12], these calculi are generalizable both to different Dynamic Logics (Epistemic, Deontic, etc.) and to different propositional bases (Linear, Relevant, etc.). Moreover, the rules they feature agree with the standard relational semantics for dynamic epistemic logics, while a ‘natural’ coalgebraic semantics was introduced in [7]. However, these calculi still feature a peculiar set of contextual rules, i.e. structural and operational rules involving a context (understood as the precondition for the applicability of an action), which make them non-standard as display calculi. To fix this shortcoming, in [8] we propose a new class of more general sequent calculi (which we call dynamic calculi) that overcome the need of contextual rules and enjoy other benefits, including a natural proof-theoretic semantics. In this talk we present two concrete examples of dynamic calculi for one specific dynamic epistemic logic [2], both in its classical and in its intuitionistic version, where the Intuitionistic logic for Epistemic Action and Knowledge was intoduced via duality in [10] defining dynamic algebraic semantics on intuitionistic base. These calculi can be understood as generalizations of the display calculi [4], since they feature: 1. constituents of several types (e.g. of type AG for ‘agents’ or ACT for ‘actions’), along with propositional constituents, which in their turn can be of different types (e.g. intuitionistic propositions iPROP, or classical propositions cPROP, etc.); N. Galatos, A. Kurz, C. Tsinakis (eds.), TACL 2013 (EPiC Series, vol. 25), pp. 85–87 85 Sequent calculus for dynamic epistemic logic Greco, Kurz and Palmigiano 2. non-contextual1 structural connectives (structural conjunction and disjunction, implication and disimplication — also called exclusion —, and their neutral elements) by which structures are built, where a structure can be homogeneous (e.g. α ∧ β is of type ACT ×ACT ) or heterogeneous (e.g. α ∧ A is of type ACT × PROP).2 3. structural introduction rules, which constitues a pure structural calculus because the structural and operational level are now completely separated (e.g. (X ` Y)∧ (W ` Z) / X∧W ` Y∧ Z); 4. unary translation rules, to pass from structural to operational level: the flattening rule, making it possible to transform homogeneous structures into operational formulas (e.g. A ∧ B ` X / A∧B ` X, where A∧B is a propositional formula of type PROP×PROP→ PROP), and the currying rule, making it possible to transform heterogeneous structures into ‘parametrized’ operational formulas (e.g. α ∧ A ` X / 〈α〉A ` X, where 〈α〉A is a propositional modal formula of type ACT ×PROP→ PROP). These calculi are interesting from both a methodological and an applicative viewpoint. Methodologically, the dynamic calculi achieve a unified framework simultaneously accounting for different logical behaviors: modalities (e.g. exponentials or temporal operators) and quantifiers can be seen in terms of combinations of heterogeneous components by means of operational rules at the merging-level; the behavior of a single modal operator (e.g. monotonicity) or the interaction between modalities (e.g. dynamic and epistemic operators) can be captured by means of structural rules at the merging-level. We will also discuss the categorial semantics, which seems the most ‘appropriate’ for this kind of calculi. From the point of view of the applications, dynamic calculi provide a way of generating specific display calculi for a wide array of logics — which includes but is not limited to dynamic (epistemic) logics — simply by deriving the appropriate rules; this allows to obtain meta-theorems such as cut elimination [8] uniformly for each specific calculus as a byproduct of the general theory of dynamic calculi. The dynamic calculi enjoy the strong version of Wansing’s fundamental properties of segregation, symmetricity and explicitness [12]. Therefore, they share all the benefits that come from the display calculi, but are more general: for instance they capture also dynamic poly-modal logics on substructural base.

Dynamic sequent calculus for the logic of Epistemic Actions and Knowledge