 In 1940 Church turned away from a type-free approach and published a version of STT that incorporated λ-abstraction (see  supplement D).  Although Church had developed what became the most useful and famous version of STT (1940), he thought that it was not enough to meet condition (1), since he thought that STT when augmented with a semantical predicate was vulnerable to the semantical paradoxes such as the Epimenides and Grelling’s paradox (cf.  section 4  above). To avoid these he thought it necessary to appeal to RTT (with reducibility).