Is there a completeness proof of intuitionistic predicate calculus using Heyting algebra semantics that is inuitionistically valid? 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.
 A: Harry de Swart's PhD from the University of Nijmegen (the Netherlands) was (explicitly) about this kind of topic.  He establishes the completeness of IPC using search trees, in an intuitionistic meta theory.  I do not know how search trees relate to your question.
H.C.M. de Swart: Intuitionistic logic in intuitionistic metamathematics, Dissertation, 1976, University of Nijmegen. https://core.ac.uk/reader/43594080
de Swart has since left this field, so I do not know if he will answers questions via email.
A: It's going to depend on exactly what you mean by Heyting algebra semantics, but there is a proof in Troelstra and Van Dalen, Constructivism in Mathematics, Vol 2, for what they call $\Theta$-models, where $\Theta$ is a Heyting algebra. The completeness theorem appears as Theorem 6.12.
A: I have a completeness proof based on Abstraction Logic, but it is a classical proof: https://doi.org/10.47757/abstraction.logic.1
Also, it is for intuitionistic abstraction logic and all logics extending it.
