Product closure of some second-order modal logics

TL;DR

This paper proves that certain second-order modal logics, including monadic second order logic, are unaffected in expressive power by product update operations, using an intermediate language with action nominals.

Contribution

It establishes the closure of monadic second order logic and related logics under product update, introducing the use of action nominals as a key technique.

Findings

Monadic second order logic is closed for product update.

Propositionally quantified modal logic is closed for product update.

Modal mu-calculus is closed for product update.

Abstract

Product update is an operation on models introduced into epistemic logic in order to represent a broad class of informational events. If adding modalities representing product update to a language does not alter its expressive power then we say that the language is "closed for product update." The basic modal language is known to be closed for product update. We establish that monadic second order logic is closed for product update (Theorem 5). Our technique is to pass via an intermediate language with what we call "action nominals." We obtain as corollaries that propositionally quantified modal logic is closed for product update, as is the modal mu-calculus.