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 ≤ 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.