Locally finite reducts of Heyting algebras and canonical formulas. (English) Zbl 1417.03198

Bezhanishvili, Guram; Bezhanishvili, Nick

Notre Dame J. Formal Logic 58, No. 1, 21-45 (2017).

Summary: The variety of Heyting algebras has two well-behaved locally finite reducts, the variety of bounded distributive lattices and the variety of implicative semilattices. The variety of bounded distributive lattices is generated by the \(\to\)-free reducts of Heyting algebras, while the variety of implicative semilattices is generated by the \(\vee\)-free reducts. Each of these reducts gives rise to canonical formulas that generalize Jankov formulas and provide an axiomatization of all superintuitionistic logics (si-logics for short).
The \(\vee\)-free reducts of Heyting algebras give rise to the \((\wedge,\to)\)-canonical formulas that we studied in an earlier work. Here we introduce the \((\wedge,\vee)\)-canonical formulas, which are obtained from the study of the \(\to\)-free reducts of Heyting algebras. We prove that every si-logic is axiomatizable by \((\wedge,\vee)\)-canonical formulas. We also discuss the similarities and differences between these two kinds of canonical formulas.
One of the main ingredients of these formulas is a designated subset \(D\) of pairs of elements of a finite subdirectly irreducible Heyting algebra \(A\). When \(D=A^2\), we show that the \((\wedge,\vee)\)-canonical formula of \(A\) is equivalent to the Jankov formula of \(A\). On the other hand, when \(D=\emptyset\), the \((\wedge,\vee)\)-canonical formulas produce a new class of si-logics we term stable si-logics. We prove that there are continuum many stable si-logics and that all stable si-logics have the finite model property. We also compare stable si-logics to splitting and subframe si-logics.

MSC:

03B55	Intermediate logics
06D20	Heyting algebras (lattice-theoretic aspects)

Keywords:

superintuitionistic logic; axiomatization; filtration; finite model property; Heyting algebra; duality theory