It is known that any Heyting algebra is the Lindenbaum algebra of some theory in the second order intuitionistic propositional calculus. I believe this gives affirmative answer to your question although I do not know enough to be sure.

In the paper "On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic" (draft version freely available) Andy Pitts constructed quantifiers out of any Heyting algebra $H$. There are operators $A_p,E_p:H[p]\to H$ such that for any Heyting algebra polynomial $\phi(p)$ with coefficients in $H$ and any $h\in H$, one has $\phi(p)\leqslant h$ in $H[p]$ (with $h$ regarded as a constant polynomial) iff $E_p(\phi(p))\leqslant h$ in $H$, and $h\leqslant\phi(p)$ iff $h\leqslant A_p(\phi(p))$.

It follows that the generic model of the theory of $H$-algebras (i. e. Heyting algebras together with a homomorphism from $H$ to them) produces a model of soipc. For details see the last page of the paper.

Pitts also asked whether this can be extended to higher orders. Because of the correspondence between higher order intuitionistic type theories and elementary toposes, a variant of his question is whether for any Heyting algebra $H$ there exists a topos with $H$ as the lattice of all subobjects of the terminal object.

Dito Pataraia has an amazing construction of such a topos, although more than two years after his death we (his closest friends and colleagues) still have not managed to turn his work into a publication. This is mostly my fault I have to admit.

For complete $H$ a solution is given by the topos of sheaves on $H$.

For a (not necessarily complete) Boolean algebra $B$ there is a construction by Freyd which goes as follows. Present $B$ as a filtered colimit of a diagram of finite algebras $(B_i, \iota_{ij}:B_i\to B_j)$ (for example, union of all finite subalgebras of $B$). Each finite $B_i$ is the algebra of subobjects of 1 in the topos $\mathbf T_i=\mathbf{Sets}^{\textrm{atoms of $B_i$}}$ (or if you prefer you can take only finite sets), and each $\iota_{ij}$ induces a logical functor $\mathbf T_i\to\mathbf T_j$ (reindexing along the dual map between atoms in the opposite direction). The colimit of this diagram of logical functors gives a topos $\mathbf T$ whose algebra of subobjects of 1 is $B$. (This is an exercise in the first topos book of Johnstone.)

Perhaps more explicitly one may view this $\mathbf T$ as follows. Let $X_B$ be the dual space of $B$ (any zero-dimensional compact Hausdorff space). Then objects of $\mathbf T$ are given by local homeomorphisms $Y\to X_B$ which can be realized as pullbacks along a continuous map $X_B\to X$ of a map $Y'\to X$ of finite sets (with discrete topology). Thus such objects are represented by finite strict $B$-valued sets: finite sets $S$ equipped with an equality predicate $\mathrm{eq}_S:S\times S\to B$ such that for any $s,s'\in S$, either $\mathrm{eq}_S(s,s')=0$ or $\mathrm{eq}_S(s,s')=\mathrm{eq}_S(s,s)=\mathrm{eq}_S(s',s')$. Morphisms $(S,\mathrm{eq}_S)\to(T,\mathrm{eq}_T)$ are then defined as usual with $B$-valued sets, i. e. as certain predicates $S\times T\to B$ serving as graphs of maps.

All this however heavily uses Booleanness of $B$. At least Dito's construction is completely different and much more involved.

It is known that any Heyting algebra is the Lindenbaum algebra of some theory in the second order intuitionistic propositional calculus. I believe this gives affirmative answer to your question although I do not know enough to be sure.

In the 1992 JSL paper "On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic" (JSTOR; draft version freely available) Andy Pitts constructed quantifiers out of any Heyting algebra $H$. There are operators $A_p,E_p:H[p]\to H$ such that for any Heyting algebra polynomial $\phi(p)$ with coefficients in $H$ and any $h\in H$, one has $\phi(p)\leqslant h$ in $H[p]$ (with $h$ regarded as a constant polynomial) iff $E_p(\phi(p))\leqslant h$ in $H$, and $h\leqslant\phi(p)$ iff $h\leqslant A_p(\phi(p))$.

It follows that the generic model of the theory of $H$-algebras (i. e. Heyting algebras together with a homomorphism from $H$ to them) produces a model of soipc. For details see the last page of the paper.

Pitts also asked whether this can be extended to higher orders. Because of the correspondence between higher order intuitionistic type theories and elementary toposes, a variant of his question is whether for any Heyting algebra $H$ there exists a topos with $H$ as the lattice of all subobjects of the terminal object.

Dito Pataraia has an amazing construction of such a topos, although more than two years after his death we (his closest friends and colleagues) still have not managed to turn his work into a publication. This is mostly my fault I have to admit.

For complete $H$ a solution is given by the topos of sheaves on $H$.

For a (not necessarily complete) Boolean algebra $B$ there is a construction by Freyd which goes as follows. Present $B$ as a filtered colimit of a diagram of finite algebras $(B_i, \iota_{ij}:B_i\to B_j)$ (for example, union of all finite subalgebras of $B$). Each finite $B_i$ is the algebra of subobjects of 1 in the topos $\mathbf T_i=\mathbf{Sets}^{\textrm{atoms of $B_i$}}$ (or if you prefer you can take only finite sets), and each $\iota_{ij}$ induces a logical functor $\mathbf T_i\to\mathbf T_j$ (reindexing along the dual map between atoms in the opposite direction). The colimit of this diagram of logical functors gives a topos $\mathbf T$ whose algebra of subobjects of 1 is $B$. (This is an exercise in the first topos book of Johnstone.)

Perhaps more explicitly one may view this $\mathbf T$ as follows. Let $X_B$ be the dual space of $B$ (any zero-dimensional compact Hausdorff space). Then objects of $\mathbf T$ are given by local homeomorphisms $Y\to X_B$ which can be realized as pullbacks along a continuous map $X_B\to X$ of a map $Y'\to X$ of finite sets (with discrete topology). Thus such objects are represented by finite strict $B$-valued sets: finite sets $S$ equipped with an equality predicate $\mathrm{eq}_S:S\times S\to B$ such that for any $s,s'\in S$, either $\mathrm{eq}_S(s,s')=0$ or $\mathrm{eq}_S(s,s')=\mathrm{eq}_S(s,s)=\mathrm{eq}_S(s',s')$. Morphisms $(S,\mathrm{eq}_S)\to(T,\mathrm{eq}_T)$ are then defined as usual with $B$-valued sets, i. e. as certain predicates $S\times T\to B$ serving as graphs of maps.

All this however heavily uses Booleanness of $B$. At least Dito's construction is completely different and much more involved.

It is known that any Heyting algebra is the Lindenbaum algebra of some theory in the second order intuitionistic propositional calculus. I believe this gives affirmative answer to your question although I do not know enough to be sure.

In the paper "On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic" (draft version freely available) Andy Pitts constructed quantifiers out of any Heyting algebra $H$. There are operators $A_p,E_p:H[p]\to H$ such that for any Heyting algebra polynomial $\phi(p)$ with coefficients in $H$ and any $h\in H$, one has $\phi(p)\leqslant h$ in $H[p]$ (with $h$ regarded as a constant polynomial) iff $E_p(\phi(p))\leqslant h$ in $H$, and $h\leqslant\phi(p)$ iff $h\leqslant A_p(\phi(p))$.

It follows that the generic model of the theory of $H$-algebras (i. e. Heyting algebras together with a homomorphism from $H$ to them) produces a model of soipc. For details see the last page of the paper.

Pitts also asked whether this can be extended to higher orders. Because of the correspondence between higher order intuitionistic type theories and elementary toposes, a variant of his question is whether for any Heyting algebra $H$ there exists a topos with $H$ as the lattice of all subobjects of the terminal object.

Dito Pataraia has an amazing construction of such a topos, although more than two years after his death we (his closest friends and colleagues) still have not managed to turn his work into a publication. This is mostly my fault I have to admit.

For complete $H$ a solution is given by the topos of sheaves on $H$.

For a (not necessarily complete) Boolean algebra $B$ there is a construction by Freyd which goes as follows. Present $B$ as a filtered colimit of a diagram of finite algebras $(B_i, \iota_{ij}:B_i\to B_j)$ (for example, union of all finite subalgebras of $B$). Each finite $B_i$ is the algebra of subobjects of 1 in the topos $\mathbf T_i=\mathbf{Sets}^{\textrm{atoms of $B_i$}}$ (or if you prefer you can take only finite sets), and each $\iota_{ij}$ induces a logical functor $\mathbf T_i\to\mathbf T_j$ (reindexing along the dual map between atoms in the opposite direction). The colimit of this diagram of logical functors gives a topos $\mathbf T$ whose algebra of subobjects of 1 is $B$.

Perhaps more explicitly one may view this $\mathbf T$ as follows. Let $X_B$ be the dual space of $B$ (any zero-dimensional compact Hausdorff space). Then objects of $\mathbf T$ are given by local homeomorphisms $Y\to X_B$ which can be realized as pullbacks along a continuous map $X_B\to X$ of a map $Y'\to X$ of finite sets (with discrete topology). Thus such objects are represented by finite strict $B$-valued sets: finite sets $S$ equipped with an equality predicate $\mathrm{eq}_S:S\times S\to B$ such that for any $s,s'\in S$, either $\mathrm{eq}_S(s,s')=0$ or $\mathrm{eq}_S(s,s')=\mathrm{eq}_S(s,s)=\mathrm{eq}_S(s',s')$. Morphisms $(S,\mathrm{eq}_S)\to(T,\mathrm{eq}_T)$ are then defined as usual with $B$-valued sets, i. e. as certain predicates $S\times T\to B$ serving as graphs of maps.

All this however heavily uses Booleanness of $B$. At least Dito's construction is completely different and much more involved.

It is known that any Heyting algebra is the Lindenbaum algebra of some theory in the second order intuitionistic propositional calculus. I believe this gives affirmative answer to your question although I do not know enough to be sure.

In the paper "On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic" (draft version freely available) Andy Pitts constructed quantifiers out of any Heyting algebra $H$. There are operators $A_p,E_p:H[p]\to H$ such that for any Heyting algebra polynomial $\phi(p)$ with coefficients in $H$ and any $h\in H$, one has $\phi(p)\leqslant h$ in $H[p]$ (with $h$ regarded as a constant polynomial) iff $E_p(\phi(p))\leqslant h$ in $H$, and $h\leqslant\phi(p)$ iff $h\leqslant A_p(\phi(p))$.

It follows that the generic model of the theory of $H$-algebras (i. e. Heyting algebras together with a homomorphism from $H$ to them) produces a model of soipc. For details see the last page of the paper.

Pitts also asked whether this can be extended to higher orders. Because of the correspondence between higher order intuitionistic type theories and elementary toposes, a variant of his question is whether for any Heyting algebra $H$ there exists a topos with $H$ as the lattice of all subobjects of the terminal object.

Dito Pataraia has an amazing construction of such a topos, although more than two years after his death we (his closest friends and colleagues) still have not managed to turn his work into a publication. This is mostly my fault I have to admit.

For complete $H$ a solution is given by the topos of sheaves on $H$.

For a (not necessarily complete) Boolean algebra $B$ there is a construction by Freyd which goes as follows. Present $B$ as a filtered colimit of a diagram of finite algebras $(B_i, \iota_{ij}:B_i\to B_j)$ (for example, union of all finite subalgebras of $B$). Each finite $B_i$ is the algebra of subobjects of 1 in the topos $\mathbf T_i=\mathbf{Sets}^{\textrm{atoms of $B_i$}}$ (or if you prefer you can take only finite sets), and each $\iota_{ij}$ induces a logical functor $\mathbf T_i\to\mathbf T_j$ (reindexing along the dual map between atoms in the opposite direction). The colimit of this diagram of logical functors gives a topos $\mathbf T$ whose algebra of subobjects of 1 is $B$. (This is an exercise in the first topos book of Johnstone.)

Perhaps more explicitly one may view this $\mathbf T$ as follows. Let $X_B$ be the dual space of $B$ (any zero-dimensional compact Hausdorff space). Then objects of $\mathbf T$ are given by local homeomorphisms $Y\to X_B$ which can be realized as pullbacks along a continuous map $X_B\to X$ of a map $Y'\to X$ of finite sets (with discrete topology). Thus such objects are represented by finite strict $B$-valued sets: finite sets $S$ equipped with an equality predicate $\mathrm{eq}_S:S\times S\to B$ such that for any $s,s'\in S$, either $\mathrm{eq}_S(s,s')=0$ or $\mathrm{eq}_S(s,s')=\mathrm{eq}_S(s,s)=\mathrm{eq}_S(s',s')$. Morphisms $(S,\mathrm{eq}_S)\to(T,\mathrm{eq}_T)$ are then defined as usual with $B$-valued sets, i. e. as certain predicates $S\times T\to B$ serving as graphs of maps.

All this however heavily uses Booleanness of $B$. At least Dito's construction is completely different and much more involved.