This is the external website for the ESSLLI 2019 course "Quantifying over Information Change". For now, this page contains a summary of the material that will be treated in the course and a list of references. The slides for the course have not been finalized yet, but will be posted here before ESSLLI starts.

In dynamic epistemic logics a modality that is interpreted as a model transformer represents information change. Examples are public announcement logic, action model logic, and arrow update logic. Such logics can be expanded with operators describing quantification over information change to represent, for example, 'there is an announcement after which formula phi is true' (where phi is some postcondition in the resulting structure), or 'there is an action model after which phi is true'. Over the past 10 to 15 years several such logics have been proposed. They are indispensable in describing epistemic planning problems. We will present various such logics in depth, and also sketch some general themes around update logics involving expressivity, axiomatization, decidability, quantifying over world/relation/factual change, and related logics such as sabotage logic.

Students taking this course are expected to know modal logic and to have at least some familiarity with dynamic epistemic logic.

Note that this is only a tentative outline. Expect the final outline to deviate at least somewhat from this one.

Epistemic logic, the logic of knowledge, can be used to describe the information state of one or more agents, and the knowledge that the agents possess in that situation. Basic epistemic logic by itself cannot, however, represent information change. So it cannot be used to reason about situations where agents learn new things, or forget things they already knew. Dynamic epistemic logic (DEL) is an extension of epistemic logic that does allow us to represent information change.

In DEL, information change is represented by so-called updates. An update is of the form <E>, where E is some kind of event that changes what information the agents possess. A formula <E>phi then means “after the event E has happened, phi will be true”. There are many different kinds of updates, representing different kinds of information changing events. The simplest type of update is the public announcement (Plaza, 1989, Baltag et al., 1998). A public announcement is of the form <psi>, and indicates that all agents are made aware of the truth of psi in a public fashion, for example by an announcement when all of them are present. As a simple example, suppose that a teacher announces to their class that the test will be on Friday. After such an announcement, it will be common knowledge between the teacher and the class that the test is indeed on Friday. In DEL, this can be represented as <p>Cp, where p is an atomic proposition meaning “the test is on Friday”.

Public announcements can only represent relatively simple events, in order to represent more complex events we can use different types of updates, such as action model logic (Baltag et al., 1998) or arrow update logic (Kooi & Renne, 2011). Arrow updates, like public announcements, represent events that are essentially public. Action models are a generalization of public announcements to events that are non-public. Similarly, arrow updates can be generalized to arrow update models (Kooi & Renne, 2011, Van Ditmarsch et al., 2018) that allow for non-public events.

One particular strand of further development in DEL is towards quantification over updates. Dynamic epistemic logic allows us to reason about the effects of a particular event that is specified in advance. Using quantified updates, we can reason about the effect of every possible update. A root of such investigations is Fine's work on propositional quantification (1970), and later work on bisimulation quantifiers (French, 2006). The first dynamic epistemic logic to explicitly use a quantified update was APAL: arbitrary public announcement logic (2008). The language op APAL contains an operator <>phi standing for 'there is psi such that after public announcement of psi, phi (is true)', subject to certain conditions on psi to avoid a circular definition. Such a logic is useful for analyzing knowability (if phi is true, is there an update after which the agent knows that phi?), and also in epistemic planning (given epistemic goal phi, is there an update/program realizing phi?). A number of variations of this logic have appeared since, with quantification over certain subsets of all public announcements. A well-established version is one where <G>phi stands for 'there are psi_1, ..., psi_n (one for each agent in G) such that after simultaneous public announcement by the agents in G of psi_1, ..., psi_n, phi (is true)'. This logic formalizes certain notions of agency and ability (Agotnes et al., 2010). Another version, with relations to game logics, has a similar operator but then expressing that the agents in G can realize phi no matter what the agents not in G do to prevent it (by simultaneous announcements).

Quantification over updates other than public announcements is also possible. Arbitrary action model logic (Hales, 2013) and arbitrary arrow update logic (Van Ditmarsch et al, 2017) quantify over action models and arrow updates, respectively, as their names suggest. Most, but not all, of these quantified update logics are undecidable. Whether they are axiomatizable is currently an open question, although the slightly more powerful arbitrary arrow update logic with common knowledge has been shown to be unaxiomatizable (Kuijer, 2017). Additionally, even for the decision problems that are decidable, the computational complexity tends to be rather high.

Another related logic is Refinement modal logic (Bozelli et al., 2014), which has a modality representing quantification over updates, but does not have (deterministic/concrete) update modalities in the object language to quantify over. The refinement modality can be nicely mapped to combinations of relativization and bisimulation quantifiers, and therefore is a decidable (but highly complex) logic. The meaning of the refinement operator is hard to describe informally, so it is difficult to find real-life examples that are well represented using refinements. Still, its technical properties make it very useful in theoretical computer science, for issues such as synthesis and simulation.

A number of other logics exist that are conceptually similar to quantified update logics, but that operate very differently from a technical point of view. These logics have very expressive quantifiers over information change (the reason they are expressive is that they are state-based, not model-based), and include sabotage logic (Van Benthem, 2005) as well as various works by Areces and Fervari on relation-changing modalities. Yet further developments envisage update logics with quantification over purely factual change, both public and private, reminiscent of the original Fine (1970) publication on propositional quantification.

In this ESSLLI course, we will discuss all types of quantified information change. We will explain the applications of the different logics, but also their downsides with respect to computational complexity. Additionally, we will compare the logics to one another, with emphasis on their expressivity and update expressivity.