Miguel MARTINS (University of Barcelona) will give a talk on
Counting/determining locally tabular bi-intuitionistic logics of co-trees: a denumerable/decidable problem
Abstract:
The bi-intuitionistic propositional calculus bIPC is the natural symmetric extension of the intuitionistic propositional calculus IPC, obtained by enriching the language with the co-implication \gets, a binary connective that behaves dually to the intuitionistic implication. This yields a logical system equipped with far greater expressive power than that of IPC, which is algebraized by the variety of bi-Heyting algebras (i.e., Heyting algebras whose order duals are also Heyting algebras).
A notable extension of bIPC is the bi-Gödel-Dummett logic bGD (aka the bi-intuitionistic logic of co-trees), axiomatized by the Gödel-Dummett prelinearity axiom (p \to q) \lor (q \to p). Over IPC, the same formula axiomatizes the widely studied intuitionistic linear calculus LC (aka the intuitionistic logic of chains). It is well known that the lattice of extensions of LC forms a chain of order type (\omega + 1)^\partial, and that all of its elements are locally tabular. However, this is far from the bi-intuitionistic case: the lattice of extensions of bGD is not a chain, has the size of the continuum, but contains only denumerably many locally tabular logics. This was proved by developing the theory of Jankov and subframe formulas of bi-Gödel algebras (i.e., the algebras which algebraize bGD), and subsequently deriving a criterion for local tabularity in extensions of bGD. We also use this criterion to ensure the decidability of the problem of determining if a finitely axiomatizable extension of bGD is locally tabular.