Uniform Local Tabularity in Intuitionistic Logic

By contrast with S4, the analysis of local tabularity above IPC has provided a difficult challenge. This paper studies a strengthening of local tabularity - 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 below 3 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, which is shown to be the unique pre-uniformly locally tabular extension of the system KG.