According to godelian in Henkin-style completeness proofs for intuitionistic logic there are multiple intuitionstically valid proofs of the completeness of inuitionistic predicate calculus (IPC) via modified Kripke models, Category Theory, etc.

I'm inquiring whether there is a proof in terms of Heyting algebra semantics. I've found two completeness proofs using Heyting algebra semantics: the first one for the propositional calculus in Palmgren - Semantics of intuitionistic propositional logic (which I think could be extended to the predicate calculus) and the second one for the predicate calculus in Valentini - A simple proof of the completeness theorem of the intuitionistic predicate calculus with respect to the topological semantics. Both seem to be intuitionistically valid to ME, but I am suspicious of this for multiple reasons. The primary one being that Gödel and Kreisel showed that such a proof (with out modifications) entails non-constructive principles.

substantialissue is ... $\endgroup$complete. You have basically two options: (1) You define the semantics so that the Heyting algebras are not required to be complete, only that all suprema and infima actually used when computating valuations in the given model exist. Then the Lindenbaum–Tarski algebra works as is, but the semantics as a whole is quite awkward to use, as it is next to impossible to see whether a given model is actually sound (i.e., that the relevant suprema and infima exist). (2) You define the semantics so that the algebras are required to be complete. ... $\endgroup$3more comments