Published online by Cambridge University Press: 12 March 2014
In [3] Myhill has constructed a complete system K which allows in it the development of a large and important section of classical mathematics. Completeness is achieved essentially by sacrificing universal quantification and introducing instead the proper ancestral as a primitive idea.
In the following we are presenting a system K0 which will be shown to be equivalent to K (i.e. the primitive operators of both systems are mutually definable in terms of one another). K0 is also complete and covers the same ground as K. K0, however, differs from K by the introduction of the limited universal quantifier instead of the proper ancestral and of concatenation instead of the ordered-pair function as primitive operators. By a further reduction K0 will be shown to be equivalent to the system K1 not containing the abstraction-operator and the class-membership relation.