This question comes after the comments in the recent related question Sigma-complete Lindenbaum algebras?, 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?

EDIT: Joseph has answered affirmatively Question 1 for the case of an arbitrary Boolean algebra: there is in fact a first order theory over a language whose Lindenbaum algebra is isomorphic to it (one could considered instances of excluded middle as part of the theory).

Remarkably, his proof does use BPI, which motivates also the corresponding version of Question 2 for the Boolean case:

Question 2': Is the assertion that every Boolean algebra is the Lindenbaum algebra of a first order theory equivalent to BPI?