On weak completeness of intuitionistic predicate logic
Georg Kreisel · Journal of Symbolic Logic · 1962
Suppose the ri-placed relation symbols Pi, 1 ≦ i ≦ k, are all the non-logical constants occurring in the closed formula , also written as , of Heyting's predicate calculus (HPC). Then HPC is called complete for provided , i.e. Here D ranges over arbitrary species, and over arbitrary (possibly incompletely defined) subspecies of ;