This problem asks for a result analogous to a theorem of Shavrukov describing the (r.e.) subalgebras of the provability algebra of PA.

De Jongh and Visser showed that the r.e. subalgebras of the theory HA^* are exactly the positive Heyting algebras satisfying the disjunction property. (The theory HA^* has been introduced by Visser earlier. It is somewhat artificially defined by a fixed point construction as the extention of HA by the schema expressing the completeness of HA^* itself.)

For HA the question of r.e. subalgebras remains open. De Jongh and Visser conjecture that these can be characterized as the Lindenbaum Heyting algebras of propositional r.e. theories P (over intuitionistic logic) satisfying the following condition.

Whatever a finite Kripke model satisfying P (possibly without a unique minimal element), there is an extension of this model to a model of P by adding a new root below all nodes.

The usual disjunction property corresponds to a more relaxed condition, where one allows to add additional nodes above the common root.

D. de Jongh, A. Visser. Embeddings of Heyting algebras. In: W. Hodges et al., eds., Logic: from foundations to applications. Clarendon Press, Oxford, 1996. Pages 187-213.