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

TL;DR

This paper proves that determining local tabularity for finitely axiomatizable extensions of bi-G"odel logic, characterized by co-tree structures, is a decidable problem, advancing understanding of bi-Heyting algebra logics.

Contribution

It establishes the decidability of local tabularity for extensions of bi-G"odel logic using co-tree structures, and shows that the logic of finite co-trees is finitely axiomatizable and decidable.

Findings

Local tabularity is decidable for extensions of bi-G"odel logic.

The logic of finite co-trees, called Log(FC), is finitely axiomatizable.

Log(FC) has the finite model property, ensuring decidability.

Abstract

A bi-Heyting algebra validates the G\"odel-Dummett axiom $(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 $\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 $\operatorname{\mathsf{bi-GD}}$ is locally tabular. Notably, if $L$ is an extension of $\operatorname{\mathsf{bi-GD}}$, then $L$ is locally tabular iff $L$ is not contained in $Log(FC)$, the logic of a particular family of finite co-trees, called the finite combs. We prove that $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.