KNOCKING DOWN BOXES: THE FMP FOR <mml:math xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mnf="http://cambridge.org/core/manifest" xmlns:cup="http://contentservices.cambridge.org" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:m="http://cambridge.org/core/metadata" xmlns:core="http://cambridge.org/core" xmlns:c="http://cambridge.org/core/content" display="inline"> <mml:mrow> <mml:mi mathvariant="bold">K</mml:mi> </mml:mrow> <mml:mo>⊕</mml:mo> <mml:msup> <mml:mi>◻</mml:mi> <mml:mrow> <mml:mi>m</mml:mi> <mml:mo>+</mml:mo> <mml:mi>k</mml:mi> </mml:mrow> </mml:msup> <mml:mi>p</mml:mi> <mml:mo stretchy="false" accent="false">→</mml:mo> <mml:msup> <mml:mi>◻</mml:mi> <mml:mi>m</mml:mi> </mml:msup> <mml:mi>p</mml:mi> </mml:math> $\mathbf {K}\oplus \Box ^{m+k} p\to \Box ^m p$ bold upper K circled plus white medium square Superscript m plus k Baseline p right arrow white medium square Superscript m Baseline p

Abstract It is a long-standing open problem whether modal logics of the form K ⊕ ◻ n p → ◻ m p $\mathbf {K}\oplus \Box ^np\to \Box ^mp$ bold upper K circled plus white medium square Superscript n Baseline p right arrow white medium square Superscript m Baseline p for n > m > 1 $n>m>1$ n greater than m greater than 1 have the finite model property (FMP). We solve this by showing that any modal logic axiomatized by formulas of the form ◻ n p → ◻ m p $\Box ^np\to \Box ^mp$ white medium square Superscript n Baseline p right arrow white medium square Superscript m Baseline p where n > m > 1 $n>m>1$ n greater than m greater than 1 has the FMP.