Cluster expansion and the boxdot conjecture

TL;DR

This paper proves the boxdot conjecture, showing that certain modal logics faithfully interpreted via the boxdot translation are included in the original logic, with broader implications for various modal systems.

Contribution

It confirms the boxdot conjecture and introduces a semantic condition ensuring the maximal logic embedding via the boxdot translation.

Findings

The boxdot conjecture is true for T.

The natural generalization holds for S4, S5, and KTB.

A semantic condition characterizes maximal logic embeddings.

Abstract

The boxdot conjecture asserts that every normal modal logic that faithfully interprets T by the well-known boxdot translation is in fact included in T. We confirm that the conjecture is true. More generally, we present a simple semantic condition on modal logics $L_0$ which ensures that the largest logic where $L_0$ embeds faithfully by the boxdot translation is $L_0$ itself. In particular, this natural generalization of the boxdot conjecture holds for S4, S5, and KTB in place of T.