Bi-intermediate logics of trees and co-trees

arXiv2211.14776MaRDI QIDQ6418604FDOQ6418604

Authors: Nick Bezhanishvili, Marco A. C. Martins, Tommaso Moraschini 

Publication date: 27 November 2022

Abstract: A bi-Heyting algebra validates the G"odel-Dummett axiom $(poq)vee(qop)$ 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 $mathsfbi$-$mathsfLC$ of bi-intuitionistic logic axiomatized by the G"odel-Dummett axiom. In this paper we initiate the study of the lattice $Lambda(mathsfbi$-$mathsfLC)$ of extensions of $mathsfbi$-$mathsfLC$. We develop the methods of Jankov-style formulas for bi-G"odel algebras and use them to prove that there are exactly continuum many extensions of $mathsfbi$-$mathsfLC$. We also show that all these extensions can be uniformly axiomatized by canonical formulas. Our main result is a characterization of the locally tabular extensions of $mathsfbi$-$mathsfLC$. We introduce a sequence of co-trees, called the finite combs, and show that a logic in $mathsfbi$-$mathsfLC$ is locally tabular iff it contains at least one of the Jankov formulas associated with the finite combs. It follows that there exists the greatest non-locally tabular extension of $mathsfbi$-$mathsfLC$ and consequently, a unique pre-locally tabular extension of $mathsfbi$-$mathsfLC$. These results contrast with the case of the intermediate logic axiomatized by the G"odel-Dummett axiom, which is known to have only countably many extensions, all of which are locally tabular.

This page was built for publication: Bi-intermediate logics of trees and co-trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6418604)