Uniform Local Tabularity in Intuitionistic Logic

TL;DR

This paper introduces the concept of uniform local tabularity in intuitionistic logic, analyzing algebraic structures called Heyting algebras, and provides axiomatizations and examples distinguishing it from local tabularity.

Contribution

It defines uniform local tabularity, proves that certain classes form a variety, and offers explicit axiomatizations for specific cases, advancing understanding of algebraic properties in intuitionistic logic.

Findings

n-uniformly locally finite Heyting algebras form a variety

Explicit axiomatization for n ≤ 2 cases

Existence of locally tabular logics not uniformly locally tabular

Abstract

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.