Bi-intermediate logics of trees and co-trees

A bi-Heyting algebra validates the Gödel-Dummett axiom (p→q)∨(q→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ödel algebras and form a variety that algebraizes the extension bi-GD of bi-intuitionistic logic axiomatized by the Gödel-Dummett axiom. In this paper we initiate the study of the lattice Λ(bi-GD) of extensions of bi-GD.

We develop the methods of Jankov-style formulas for bi-Gödel algebras and use them to prove that there are exactly continuum many extensions of bi-GD. 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 bi-GD. We introduce a sequence of co-trees, called the finite combs, and show that a logic in Λ(bi-GD) 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 nonlocally tabular extension of bi-GD and consequently, a unique pre-locally tabular extension of bi-GD. These results contrast with the case of the intermediate logic axiomatized by the Gödel-Dummett axiom, which is known to have only countably many extensions, all of which are locally tabular.