This question comes after the comments in the recent related question [Sigma-complete Lindenbaum algebras?](https://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?


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?


EDIT 2: François' answer and his comments underneath give a simple complete solution.


Question 1: Yes


Question 2 & 2': No. Everything is provable in ZF.



Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?
I'm not sure why you seem to disallow propositional theories. Here is a workaround... Given a Heyting algebra $H$, add a unary predicate $P\_a(x)$ for every $a \in H$ along with the axioms $$\forall x (P\_{a \land b}(x) \leftrightarrow (P\_a(x) \land P\_b(x)))$$ $$\forall x (P\_{a \lor b}(x) \leftrightarrow (P\_a(x) \lor P\_b(x)))$$ $$\forall x (P\_{a \rightarrow b}(x) \leftrightarrow (P\_a(x) \rightarrow P\_b(x)))$$ $$\forall x (P\_1(x) \land \lnot P\_0(x))$$
To trivialize the role of equality, also add a constant symbol $\*$ with the axiom $\forall x (x = \*)$. It's not hard to see that every formula is then equivalent to one of the form $P\_a(\*)$ and the map $a \in H \mapsto [P\_a(\*)]$ is an isomorphism.


