I'm reading through Hindley and Seldin's book about the lambda calculus and combinatory logic. In the book, the authors express that, though combinatory logic can be expressed as an equational theory in first order logic, the lambda calculus cannot. I sort of understand why this is true, but I can't seem to figure out the problem with the following method. Aren't the terms of first order logic arbitrary (constructed from constants, functions, and variables, etc.) so why can't we define composition and lambda abstraction as functions on variables, and then consider an equational theory over these terms? Which systems of logic can the lambda calculus be formalized as an equationary theory over?
In particular, we consider a first order language with a single binary predicate, equality. We take a set $V$ of terms over the $\lambda$ calculus, which we will view of as constants in the enveloping first order theory and for each $x \in V$, we will add a function $f_x$, corresponding to $\lambda$ abstraction. We also add a binary function $c$ corresponding to composition. We add in the standard equality axioms, in addition to the $\beta$ and $\alpha$ conversion rules, which are a sequence of infinitely many axioms produced over the terms formed from the $\lambda$ terms from composition and $\lambda$ abstraction. I doubt this is finitely axiomatizable, but it's still a first order theory.