However, if you want one of these then you could get one by adding lambda abstraction to one of the type free combinatory logics. Some care would be needed to ensure that this is just a mere notational extension or inconsistency might result.

An alternative that I have given some attention to is a classical type free theory of functions including lambda abstraction which is modelled on the kinds of function which appear in first order set theory. In such a system the constraint on abstraction in set theory which is reflected in the principle of separation would impose a constraint on the domains over which the function could be defined.

© created 1995/12/10 modified 1995/12/10