# Type-free lambda logics (L)

## Type-free lambda logics (L)

I don't know that these have ever been studied.
I think its just a historical accident that the people who were interested in type-free systems worked with combinators
rather than lambda abstraction.
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