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 with respect to Heyting Algebra semantics.

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 shown that IZF (intuitionstic set theory) proves that Intuitionistic Predicate Logic is (semantically) incomplete.

I understand that the two results are NOT contradictory because they are with respect to different semantics. But I'm curious if anyone has analyzed the differences between these semantics too any further depth and can offer any insight on this curious situation.

Additionally, 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."

What exactly is full IQC and why does it fail to be complete? Does Heyting Algebra Semantics prove completeness for full IQC while Kripke or beth semantics do not?

Edit: Increasing the clarity of the question in light of the comment section of this post and Henkin-style completeness proofs for intuitionistic logic.

fewerentailments. $\endgroup$5more comments