Why is lambda calculus named after that specific Greek letter? Why not “rho calculus”, for example?

The symbol “λ” is used for one of two basic constructions in the system introduced by Alonzo Church, specifically abstraction. The notation did not just happen to be chosen but was to distinguish it from another construction by Whitehead and Russell represented as “xˆ.” For his new system, Church initially used “∧x,” then replaced it to “λx” to ease printing, obviously, interpreting the former logical symbol as the capital Greek letter “Λ.”

See “History of λ-calculus and Combinatory Logic” by J. R. Hindley, F. Cardone (Handbook of the History of Logic, 5: 723–817, Elsevier, 2009).

I heard that Church originally used the hat symbol above the bounded variable, like $\hat x.x$, in handwritten papers. Then, the notation became ^x.x because of old-fashioned typewriters. I think it first became $\Lambda x.x$ when more recent text processors appeared, and $\lambda x.x$ after that (for aesthetics reasons probably).

Thanks to the silent downvoter, I did some googling and found Barendregt version in “The Impact of the Lambda Calculus in Logic and Computer Science”:

We end this introduction by telling what seems to be the story how the letter 'λ' was chosen to denote function abstraction. In [100] Principia Mathematica the notation for the function $f$ with $f(x) = 2x + 1$ is $2 \hat x + 1$. Church originally intended to use the notation $\hat x.2x + 1$. The typesetter could not position the hat on top of the $x$ and placed it in front of it, resulting in $\wedge x.2x + 1$. Then another typesetter changed it into $\lambda x.2x + 1$.

Dana Scott, who was a PhD student of Church, addressed this question. He said that, in Church's words, the reasoning was "eeny, meeny, miny, moe" — in other words, an arbitrary choice for no reason. He specifically debunked Barendregt's version in a recent talk at the University of Birmingham.

• Source
• Video