According to Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (https://archive.org/details/constructivismin0002troe/page/718/mode/2up) it is proven in an intuitionisitc meta-theory (as well as a classical meta-theory) that Intuitionistic Predicate Logic is (semantically) complete. Acoording to Completeness and Incompleteness for Intuitionistic Logic by Charles McCarty (https://www-jstor-org.libsrv.wku.edu/stable/pdf/27590334.pdf?refreqid=excelsior%3A6a685f26e8f7160e6a8acd8600fde1e7) it is proven that IZF (intuitionstic set theory) proves that Intuitionistic Predicate Logic is (semantically) incomplete. I am unsure how to reconcile these two results. Edit: Upon further inspection I noticed that in the Semantic Completeness chapter of Troelstra there is a section Incompleteness Results which states: "The results of the previous section (which contained a completness proof) might lead us to believe that completeness for full IQC (this is the abbreviaton for intuitionistic predicate calculus in Troelstra) ... is within reach. We shall show that, nevertheless, we cannot expect to aceive this." This may be related to the claimed incompletness from the second reference. If so, my next question is: what exactly is full IQC and why does it fail to be complete?