Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Uniform Local Tabularity in Intuitionistic Logic

Rodrigo Nicolau Almeida

TL;DR

The paper addresses uniform local tabularity in intuitionistic logic, contrasting it with classical results for $\,\mathsf{S4}$ and exploring how uniformity restricts formulas to bounded implication depth. It develops a precise algebraic and semantic framework, showing that $n$-uniform locally finite Heyting algebras always form a variety and constructing explicit axioms for the $2$-uniform case, $\mathsf{2Uni}$, which sits between $\mathsf{wPL}$ and $\mathsf{LC}$. It also demonstrates that local tabularity does not imply uniform local tabularity by presenting logics like $\mathsf{Box}$ (pre-uniform) and analyzes a spectrum of uniformities via $0$-, $1$-, $2$-, and $3$-uniform logics, including the finite-comb logic $\mathsf{LFC}$, which is $3$-uniform but not $2$-uniform. The results illuminate the structure of locally tabular logics, reveal the existence of pre-uniform phenomena, and open avenues for higher-uniformity axiomatizations and decidability questions, guiding future work in the theory of superintuitionistic logics.

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.

Uniform Local Tabularity in Intuitionistic Logic

TL;DR

The paper addresses uniform local tabularity in intuitionistic logic, contrasting it with classical results for and exploring how uniformity restricts formulas to bounded implication depth. It develops a precise algebraic and semantic framework, showing that -uniform locally finite Heyting algebras always form a variety and constructing explicit axioms for the -uniform case, , which sits between and . It also demonstrates that local tabularity does not imply uniform local tabularity by presenting logics like (pre-uniform) and analyzes a spectrum of uniformities via -, -, -, and -uniform logics, including the finite-comb logic , which is -uniform but not -uniform. The results illuminate the structure of locally tabular logics, reveal the existence of pre-uniform phenomena, and open avenues for higher-uniformity axiomatizations and decidability questions, guiding future work in the theory of superintuitionistic logics.

Abstract

By contrast wih , the analysis of local tabularity above 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, -uniformly locally finite Heyting algebras always form a variety, and an explicit axiomatization of the variety of -uniform locally finite Heyting algebras for 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.
Paper Structure (13 sections, 27 theorems, 14 equations, 8 figures)

This paper contains 13 sections, 27 theorems, 14 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Preliminaries and basic theory
  3. Superintuitionistic logics and Kripke models
  4. Local tabularity, local finiteness and their uniform versions
  5. Basic properties and criteria for uniform local tabularity
  6. The hierarchy of locally tabular logics
  7. n-uniformity in tabular logics
  8. 0-uniform, 1-uniform and 2-uniform Logics
  9. 3-uniformity and The Logic of Finite Combs
  10. A Non-Uniform Locally Tabular Logic
  11. Pre-uniform local tabularity
  12. Conclusions and Future Work
  13. Acknowledgments

Key Result

proposition 1

For each pair of models $(P,x)$ and $(Q,y)$ over $\overline{p}$ the following are equivalent:

Figures (8)

  • Figure 1: Rieger-Nishimura Ladder $\mathsf{RN}$
  • Figure 2:
  • Figure 3: $Q_{i}$ posets
  • Figure 4: 2-bisimilar models which are not bisimilar
  • Figure 5: Comb and broken comb models
  • ...and 3 more figures

Theorems & Definitions (64)

  • definition 1
  • remark 1
  • definition 2
  • proposition 1
  • proposition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • proposition 3
  • ...and 54 more