English

Local Tabularity is Decidable for Bi-Intermediate Logics of Trees and of Co-Trees

Logic 2024-09-24 v1

Abstract

A bi-Heyting algebra validates the G\"odel-Dummett axiom (pq)(qp)(p\to q)\vee (q\to p) iff the poset of its prime filters is a disjoint union of co-trees (i.e., order duals of trees). Bi-Heyting algebras of this kind are called bi-G\"odel algebras and form a variety that algebraizes the extension biGD\operatorname{\mathsf{bi-GD}} of bi-intuitionistic logic axiomatized by the G\"odel-Dummett axiom. In this paper we establish the decidability of the problem of determining if a finitely axiomatizable extension of biGD\operatorname{\mathsf{bi-GD}} is locally tabular. Notably, if LL is an extension of biGD\operatorname{\mathsf{bi-GD}}, then LL is locally tabular iff LL is not contained in Log(FC)Log(FC), the logic of a particular family of finite co-trees, called the finite combs. We prove that Log(FC)Log(FC) is finitely axiomatizable. Since this logic also has the finite model property, it is therefore decidable. Thus, the above characterization of local tabularity ensures the decidability of the aforementioned problem.

Keywords

Cite

@article{arxiv.2409.14998,
  title  = {Local Tabularity is Decidable for Bi-Intermediate Logics of Trees and of Co-Trees},
  author = {Miguel Martins and Tommaso Moraschini},
  journal= {arXiv preprint arXiv:2409.14998},
  year   = {2024}
}