Estoy leyendo el libro de Hindley y Seldin sobre el cálculo lambda y la lógica combinatoria. En el libro, los autores expresan que, aunque la lógica combinatoria se puede expresar como una teoría equacional en lógica de primer orden, el cálculo lambda no puede. Entiendo un poco por qué esto es cierto, pero no logro descubrir el problema con el siguiente método. ¿Acaso los términos de la lógica de primer orden son arbitrarios (construidos a partir de constantes, funciones y variables, etc.)? ¿Por qué no podemos definir la composición y la abstracción lambda como funciones sobre variables, y luego considerar una teoría equacional sobre estos términos? ¿En qué sistemas lógicos se puede formalizar el cálculo lambda como una teoría equacional?
En particular, consideramos un lenguaje de primer orden con un solo predicado binario, la igualdad. Tomamos un conjunto $V$ de términos sobre el cálculo $\lambda$, que veremos como constantes en la teoría de primer orden envolvente y, para cada $x \in V$, agregaremos una función $f_x$, correspondiente a la abstracción $\lambda$. También agregamos una función binaria $c$ correspondiente a la composición. Añadimos los axiomas estándar de igualdad, además de las reglas de conversión $\beta$ y $\alpha$, que son una secuencia de infinitos axiomas producidos sobre los términos formados a partir de los términos $\lambda$ de composición y abstracción $\lambda$. Dudo que esto sea finitamente axiomatizable, pero sigue siendo una teoría de primer orden.
