Solution (source code)

= Solution

No such first-order theory exists. Suppose $T$ axiomatized the Heyting algebras having only finitely many <regular element of a Heyting algebra>[regular elements]. Expand the language by constants $c_n$ and add
$$
\neg\neg c_n=c_n,\qquad c_n\neq c_m\quad(n\neq m).
$$
Every finite subset has a model: take a sufficiently large finite Boolean algebra, in which every element is regular. By the <compactness theorem>, the entire expanded theory has a model. Its reduct is a model of $T$ with infinitely many distinct regular elements, contradicting the proposed axiomatization.