Some extensional term models for combinatory logics and Lambda-Calculi
Henk Barendregt

Abstract:
This thesis is concerned with combinatorial logic, not as a basis for the rest of mathematics, but as a formal system for the study of computational procedures. Chapter I provides an overview and extension of already known material.
In Chapter II, the ω-rule is introduced and, using transfinite induction, it is proven that the extension of combinatorial logic with the ω-rule is consistent. Furthermore, the existence of universal generators is proven. For terms that are not universal generators, the ω rule is a derivative rule.
In Chapter III, a number of other consistency results are proven, yielding several non-elementary equivalent models of combinatorial logic.
Proofs of the above results usually use conservative extensions of combinatorial logic. A new proof technique plays an important role here, namely the underlining method. This method formalizes the concept of residue and thus avoids the otherwise rather cumbersome arguments.