This question comes after the comments in the recent related question http://mathoverflow.net/q/161978/12976, but in its current form is sufficiently different in my opinion, and so I decided to follow Joel's suggestion. It is also something I had asked myself before but never seriously considered. 

Question 1: Is every Heyting algebra the intuitionistic Lindenbaum-Tarski algebra of some first-order theory over some language? 

There are two possible motivations for this. First, the assertion would be true should one consider propositional theories instead. Second, an analogous result for categories is known to hold, and could be considered a generalization: every Heyting category is equivalent to the syntactic category of an intuitionistic first order theory (namely, the theory of the category itself).

In the case of an affirmative answer for Question 1, I would be also interested in an answer to

Question 2: Does the assertion in Question 1 (if true) requires some amount of choice? How much exactly? Is it, e.g., equivalent to BPI?