Uniform Local Tabularity in Intuitionistic Logic

By contrast wih $\mathsf{S4}$, the analysis of local tabularity above $\mathsf{IPC}$ has provided a difficult challenge. This paper studies a strengthening of local tabularity -- \textit{uniform local 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\leq 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.