 When instead the alternative definitions of  Section 1.4  are employed, then this requirement is obviously met due to the presence of the logical constants \(\sfQ_{{o}\alpha \alpha}\) in the signature, which by definition denote the respective identity relations on the objects of type α and therefore trivially ensure their existence in each general model \(\cM\). It is therefore a natural option to always assume primitive equality constants (for each type α) in a concrete choice of base system for Church’s type theory, just as realized in Andrews’ system \(\cQ_0\).