Making a quantifier-free type finitary

Question

Consider the theory of Heyting algebras. I have a model $L$ and a tuple $a$ in $L$. The quantifier-free type $p(x)$ of $a$ in $L$ is not generally equivalent to a single finitary formula. But suppose that $a$ generates a finite substructure in $L$. Is there a single formula $\phi(x)$ such that $\phi(x)$ is realized by $a'$ in $L'$ iff $a' \models p$?

On one hand, only finitely many terms occurring in $p$ are really necessary. On the other hand, I believe I need to say that certain terms refer to the same element in $\phi$, too, and I'm not sure if this is always possible. I'm aware that Heyting algebras are not locally finite, and I'm not sure if every finite Heyting algebra is the quotient of the free Heyting algebra by a finite number of equations (I'm not even sure if the last point is relevant here, either).

Answer 1

Yes, such a formula exists, and there's nothing deep here. Let $y_1,\dots,y_n$ be a list of all the elements of the substructure generated by $a=(a_1,\dots,a_m)$. For each $i$, choose a term $t_i(x_1,\dots,x_m)$ such that $t(a_1,\dots,a_m)=y_i$. Now let $\varphi(x_1,\dots,x_m)$ be the conjunction of the following:

• for each pair $(i,j)$ such that $a_i=y_j$, the formula $x_i=t_j(x_1,\dots,x_m)$
• for each pair $(i,j)$ such that $i\neq j$, the formula $t_i(x_1,\dots,x_m)\neq t_j(x_1,\dots,x_m)$
• the full description of how all the Heyting algebra operations act on the set $\{y_1,\dots,y_n\}$ (that is, the full "table" for each operation), representing each $y_i$ with the term $t_i(x_1,\dots,x_m)$.

If $a'$ is a tuple in any structure $L'$ such that $L'\models \varphi(a')$, then it is clear that the substructure generated by $a$ is isomorphic to the substructure generated by $a'$ (just map $y_i$ to $t_i(a')$ for each $i$, and $\varphi$ says this is an injection which preserves all the operations and whose image is the substructure generated by $a'$). It follows that $a'\models p$.

(Of course, none of this is special to Heyting algebras; a similar construction would work for structures over any finite language.)