I've read that initially Church proposed the $\lambda$-calculus as part of his Postulates of Logic paper (which is a dense read). But Kleene proved his "system" inconsistent after which, Church extracted relevant things for his work on "effective computability" and abandoned his prior work on logic.
So as I understand it, the $\lambda$-system and its notations took form as part of something to do with logic. What was Church initially trying to achieve that he forked off from later? What were the initial reasons for creating $\lambda$-calculus?