Locally tabular products of modal logics
Ilya B. Shapirovsky, Vladislav Sliusarev
TL;DR
This paper tackles when the product of two Kripke-complete modal logics, L1 × L2, is locally tabular. It proves that local tabularity of the factors is necessary but not sufficient, and then develops semantic (bounded cluster property, reducible path property) and axiomatic (product RP formulas, 1-finiteness) criteria that guarantee local tabularity of the product, with explicit applicability to new families and extensions such as S4.1[2] × S5 and a prelocally tabular Tack × S5 extension. The authors show that local tabularity does not imply the product finite model property, and analyze how the height of the factors influences product fmp, including open cases for height 2. They also introduce a product RP criterion for extensions above S4 × S5 and construct two-dimensional tack-type logics to illustrate prelocal tabularity in higher-dimensional products. The work provides a comprehensive framework to identify locally tabular products and open problems about extending these results to broader logics and symmetric cases, with potential impact on understanding the finite-model behavior and structure of bimodal products.
Abstract
In the product $L_1\times L_2$ of two Kripke complete consistent logics, local tabularity of $L_1$ and $L_2$ is necessary for local tabularity of $L_1\times L_2$. However, it is not sufficient: the product of two locally tabular logics may not be locally tabular. We provide extra semantic and axiomatic conditions that give criteria of local tabularity of the product of two locally tabular logics, and apply them to identify new families of locally tabular products. We show that the product of two locally tabular logics may lack the product finite model property. We give an axiomatic criterion of local tabularity for all extensions of $S4.1 [ 2 ]\times S5$. Finally, we describe a new prelocally tabular extension of $S{4}\times S{5}$.