Uniform Local Tabularity in Intuitionistic Logic

By contrast wih $\mathsf{S}\mathsf{4}$, the analysis of local tabularity above $\mathsf{I}\mathsf{P}\mathsf{C}$ has provided a difficult challenge. This paper studies a strengthening of local tabularity – $\mathit{\text{uniform}}\mathit{\text{local}}\mathit{\text{tabularity}}$ – where one demands that all formulas be equivalent to formulas of a given implication depth. Algebraically, this amounts to considering Heyting algebras generated by finitely many iterations of the implication operation. It is shown that in contrast with locally finite Heyting algebras, $n$-uniformly locally finite Heyting algebras always form a variety, and an explicit axiomatization of the variety of $n$-uniform locally finite Heyting algebras for $n\le 2$ is given. In connection with this analysis, it is shown that there exist locally tabular logics which are not uniformly locally tabular, answering a question of Shehtman – an example of a pre-uniformly locally tabular logic is presented.