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.

  • 1
    $\begingroup$ Since lambda calculus and combinatory logic are trivially the same thing written 2 different ways, it is likely that the author is making a statement more about the grammar of the logic moreso than the inherent expressibility of the logic. Without having the book, I'd speculate that they may be pointing out that combinatory logic's grammar is a subgrammar of FOL, and lambda calculus is not because $\lambda x$ is a different kind of quantifier than $\exists x$ or $\forall x$. $\endgroup$ – DanielV Feb 24 '17 at 17:04
  • $\begingroup$ the book later discusses models of combinatory logic, and mentions that because combinatory logic can be expressed as a first order theory (a system of first order logic with extra axioms of some form), we essentially already have a definition of models for combinatory logic, whereas for the lambda calculus we don't, because it cannot be formalized as a first order theory. what I'm arguing is why doesn't my method above express the lambda caculus as a first order theory. $\endgroup$ – Jacob Denson Feb 25 '17 at 10:14
  • $\begingroup$ How exactly do you intent to convert $\lambda x . yx = y$ into first order logic without first converting it into combinatory logic? $\endgroup$ – DanielV Feb 25 '17 at 12:59
  • $\begingroup$ The equality is a predicate of the logic, and the $\lambda x.yx$ and $y$ are terms of the logic. The $\eta$ conversion rule then becomes an axiom of the logic. $\endgroup$ – Jacob Denson Feb 26 '17 at 0:54
  • $\begingroup$ I've updated the question to elaborate more on my formalization of the calculus as a first order theory. $\endgroup$ – Jacob Denson Feb 26 '17 at 1:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.