Modal Information Logics
Søren Brinck Knudstorp
Abstract:
The present thesis studies formal properties of a family of so-called modal information logics (MILs)—modal logics first proposed in van Benthem (1996) as a way of using possible-worlds semantics to model a theory of information. They do so by extending the language of propositional logic with a binary modality defined in terms of being the supremum of two states.
First proposed in 1996, MILs have been around for some time, yet not much is known: van Benthem (2017, 2019) pose two central open problems, namely (1) axiomatizing the two basic MILs of suprema on preorders and posets, respectively, and (2) proving (un)decidability.
The main results of the first part of this thesis are solving these two problems: (1) by providing an axiomatization [with a completeness proof entailing the two logics to be the same], and (2) by proving decidability. In the proof of the latter, an emphasis is put on the method applied as a heuristic for proving decidability ‘via completeness’ for semantically introduced logics; the logics lack the FMP w.r.t. their classes of definition, but not w.r.t. a generalized class.
These results are build upon to axiomatize and prove decidable the MILs attained by endowing the language with an ‘informational implication’—in doing so a link is also made to the work of Buszkowski (2021) on the Lambek Calculus. Moreover, concluding the study of MILs on preorders and posets, it is shown that interpreting the modalities based on minimal upper bounds instead of least upper bounds does not alter the logics.
Broadening the study, the basic MIL of suprema on join-semilattices is axiomatized with an infinite scheme. This constitutes the by far most substantive part of the thesis. Accordingly—as to contribute to the toolbox of techniques for (modal) completeness proofs—an informal focus is also lend to accenting key ideas.
Finally, as an appendix, the (compactness and) decidability result(s) in Fine and Jago (2019) are significantly extended, chiefly via defining and proving a truthmaker analogue of the FMP.