 Church’s work was dogged by what he termed “antinomies”, which he distinguished from paradoxes in that the former result in outright contradiction whereas the latter give rise only to unacceptable conclusions. (Quine’s paradox discussed in  supplement C  is an example of a paradox that is not an antinomy.) His early attempt at providing foundations for mathematics turned out to be susceptible to Russell’s antinomy (Church 1932) and Richard’s antinomy (Church 1933). (Hereafter we use “paradox” rather than “antinomy” since that is the current usage; but bear in mind that there are then two kinds of paradox.) His later attempts to formulate LSD gave rise to the Russell-Myhill paradox and Anderson’s (1987) paradox, which drove Church to turn to Ramified Type Theory (or “RTT”) as a solution (see below  §4.4  and  §5).  In addition Church was convinced that Simple Type Theory (or “STT”, see  supplement D)  supplemented with a semantical predicate is threatened by the semantical paradoxes and in particular by the Grelling-Nelson paradox (the “heterological” paradox), hereafter “Grelling’s paradox” or GP. Church had an intense desire to show first how GP may be derived in STT so supplemented, secondly, how RTT resolves the problem, third, that adding the axioms of reducibility does not restore the paradox and in fact leads to an important definability result concerning RTT with reducibility, and finally, fourth, that the resolution of GP by means of RTT does not differ significantly from a Tarskian resolution in terms of the distinction between object and metalanguage.