Todd asked “Why [did Church choose] lambda and not some other Greek letter?”. Here are three answers: 1 Matthias: The story is that in the 10s and 20s, mathematicians and logicians used ^ as a notation for set abstraction, as in ^i : i is prime. Church used ^` (i.e., a primed version of this symbol) for function abstraction, because functions are just sets with extra properties. The first type set