##
**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.

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.