The modal \(\mu \) -calculus significantly extends the expressive power of basic modal logic, by adding fixed-point operators. In this paper, we study the extension of public announcement logic with such fixed-point operators. Besides the general increased expressive power, this will in particular allow us to reason about self-referential announcements, as in “after this very announcement, \(\varphi \) will be true”. Such self-referential announcements have been of recent interest in the study of the so-called surprise exam paradox. However, a straightforward combination of the two logics would rule out formulas expressing such self-referential announcements due to the restriction of variables in fixed-point operators to be positive, which ensures that the corresponding function is monotonic which again ensures that it has a greatest fixed-point. We argue, however, that first, even without the positivity requirement the function might still be monotonic in a given model, and, second, that greatest fixed-points might exist even if the corresponding function is not monotonic. We propose an extension of public announcement logic with generalised fixed-point operators, without restricting variables to be positive, and take some first steps in analysing it. We show that the logic can be reduced to the logic without public announcement operators: to what we call “full” modal fixed-point logic. We also show that the logic is strictly more expressive than the standard modal fixed-point logic. The logic offers a simpler way of modeling self-referential announcements in the surprise exam paradox, than existing approaches.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The Surprise Exam in Full Modal Fixed-Point Logic

  • Yanjun Li,
  • Jie Ren,
  • Thomas Ågotnes

摘要

The modal \(\mu \) -calculus significantly extends the expressive power of basic modal logic, by adding fixed-point operators. In this paper, we study the extension of public announcement logic with such fixed-point operators. Besides the general increased expressive power, this will in particular allow us to reason about self-referential announcements, as in “after this very announcement, \(\varphi \) will be true”. Such self-referential announcements have been of recent interest in the study of the so-called surprise exam paradox. However, a straightforward combination of the two logics would rule out formulas expressing such self-referential announcements due to the restriction of variables in fixed-point operators to be positive, which ensures that the corresponding function is monotonic which again ensures that it has a greatest fixed-point. We argue, however, that first, even without the positivity requirement the function might still be monotonic in a given model, and, second, that greatest fixed-points might exist even if the corresponding function is not monotonic. We propose an extension of public announcement logic with generalised fixed-point operators, without restricting variables to be positive, and take some first steps in analysing it. We show that the logic can be reduced to the logic without public announcement operators: to what we call “full” modal fixed-point logic. We also show that the logic is strictly more expressive than the standard modal fixed-point logic. The logic offers a simpler way of modeling self-referential announcements in the surprise exam paradox, than existing approaches.