Local properties in modal logic

AbstractIn modal logic, when adding a syntactic property to an axiomatisation, this property will semantically become true in all models, in all situations, under all circumstances. For instance, adding a property like Kap→Kbp (agent b knows at least what agent a knows) to an axiomatisation of some epistemic logic has as an effect that such a property becomes globally true, i.e., it will hold in all states, at all time points (in a temporal setting), after every action (in a dynamic setting) and after any communication (in an update setting), and every agent will know that it holds, it will even be common knowledge. We propose a way to express that a property like the above only needs to hold locally: it may hold in the actual state, but not in all states, and not all agents may know that it holds. We achieve this by adding relational atoms to the language that represent (implicitly) quantification over all formulas, as in ∀p(Kap→Kbp). We show how this can be done for a rich class of modal logics and a variety of syntactic properties. We then study the epistemic logic enriched with the syntactic property ‘knowing at least as much as’ in more detail. We show that the enriched language is not preserved under bisimulations. We also demonstrate that adding public announcements to this enriched epistemic logic makes it more expressive, which is for instance not true for the ‘standard’ epistemic logic S5