Page "Heyting algebra" Paragraph 5

Every Heyting algebra with exactly one coatom is subdirectly irreducible, whence every Heyting algebra can be made an SI by adjoining a new top.

It follows that even among the finite Heyting algebras there exist infinitely many that are subdirectly irreducible, no two of which have the same equational theory.

Hence no finite set of finite Heyting algebras can supply all the counterexamples to non-laws of Heyting algebra.

This is in sharp contrast to Boolean algebras, whose only SI is the two-element one, which on its own therefore suffices for all counterexamples to non-laws of Boolean algebra, the basis for the simple truth table decision method.

Nevertheless it is decidable whether an equation holds of all Heyting algebras.