Dynamic measure logic (Q714709)

The axiom system \(\mathsf{S4C}\) for the bimodal dynamic measure logic combines the modal logic \(\mathsf{S4}\) for the \(\square\) operator with the modal logic \(\mathsf{KD.alt}\) for the temporal `next' operator \(\bigcirc\), with the interaction axiom \({\bigcirc} \square \phi \rightarrow \square {\bigcirc} \phi\). It has a standard semantics in terms of Kripke models and accessibility relations, where the relation \(R\) for \(\square\) is reflexive and transitive, the relation \(G\) for \(\bigcirc\) is a total function and where \(u R v\) implies that \(G(u) R G(v)\); then \(\square\) is interpreted by \(R\) and \(\bigcirc\) by \(G^{-1}\). The paper investigates a semantics for \(\mathsf{S4C}\) which replaces Kripke frames by the Lebesgue measure algebra \(\mathcal{M}_{[0,1]}^\lambda\), where \([0,1]\) is the real interval (which is viewed as a topological space). The latter is defined to be the quotient algebra \(\mathrm{Borel}([0,1]) / \mathrm{Null}_\lambda\), where \(\mathrm{Borel}([0,1])\), is the collection of Borel subsets of \([0,1]\) (which is the smallest \(\sigma\)-algebra containing all open subsets of \([0,1]\)), \(\mathrm{Null}_\lambda\) is a \(\sigma\)-ideal in \(\mathrm{Borel}([0,1])\) and where \(\lambda\) is the Lebesgue measure restricted to the real interval \([0,1]\). The completeness proof transforms a Kripke model into the Lebesgue measure algebra.