 Church (1962b) distinguished sharply between which systems provide foundations for “the whole of presently extant mathematics” and which ones provide “an economical basis” for particular branches such as arithmetic. Church’s view was that while the study of logicism had led to the discovery of type theory and so to the discovery of adequate foundations for the whole of extant mathematics (see  §5.2),  it did not succeed in putting arithmetic on the most economical basis possible (for reasons explained, in  supplement D  on TT). Moreover: