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

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)
Full Text: