Abstract
Suppose the ri-placed relation symbols Pi, 1 ≦ ik, 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 ;