+[Various, slightly differing translation schemes from combinatorial logic to the lambda calculus are also possible. These generate different metatheoretical correspondences between the two calculii. Consult Hindley and Seldin for details. Also, note that the combinatorial proof theory needs to be strengthened with axioms beyond anything we've here described in order to make [M] convertible with [N] whenever the original lambda-terms M and N are convertible.]
+
+
+Let's check that the translation of the false boolean behaves as expected by feeding it two arbitrary arguments:
+
+ KIXY ~~> IY ~~> Y
+
+Throws away the first argument, returns the second argument---yep, it works.
+
+Here's a more elaborate example of the translation. The goal is to establish that combinators can reverse order, so we use the **T** combinator, where <code>T ≡ \x\y.yx</code>:
+
+ [\x\y.yx] = [\x[\y.yx]] = [\x.S[\y.y][\y.x]] = [\x.(SI)(Kx)] = S[\x.SI][\x.Kx] = S(K(SI))(S[\x.K][\x.x]) = S(K(SI))(S(KK)I)
+
+We can test this translation by seeing if it behaves like the original lambda term does.
+The orginal lambda term lifts its first argument (think of it as reversing the order of its two arguments):
+
+ S(K(SI))(S(KK)I) X Y ~~>
+ (K(SI))X ((S(KK)I) X) Y ~~>
+ SI ((KK)X (IX)) Y ~~>
+ SI (KX) Y ~~>
+ IY (KXY) ~~>
+ Y X
+
+Voilà: the combinator takes any X and Y as arguments, and returns Y applied to X.
+
+One very nice property of combinatory logic is that there is no need to worry about alphabetic variance, or
+variable collision---since there are no (bound) variables, there is no possibility of accidental variable capture,
+and so reduction can be performed without any fear of variable collision. We haven't mentioned the intricacies of
+alpha equivalence or safe variable substitution, but they are in fact quite intricate. (The best way to gain
+an appreciation of that intricacy is to write a program that performs lambda reduction.)
+
+Back to linguistic applications: one consequence of the equivalence between the lambda calculus and combinatory
+logic is that anything that can be done by binding variables can just as well be done with combinators.
+This has given rise to a style of semantic analysis called Variable Free Semantics (in addition to
+Szabolcsi's papers, see, for instance,
+Pauline Jacobson's 1999 *Linguistics and Philosophy* paper, "Towards a variable-free Semantics").
+Somewhat ironically, reading strings of combinators is so difficult that most practitioners of variable-free semantics
+express their meanings using the lambda-calculus rather than combinatory logic; perhaps they should call their
+enterprise Free Variable Free Semantics.
+
+A philosophical connection: Quine went through a phase in which he developed a variable free logic.
+
+ Quine, Willard. 1960. "Variables explained away" <cite>Proceedings of the American Philosophical Society</cite>. Volume 104: 343--347. Also in W. V. Quine. 1960. <cite>Selected Logical Papers</cite>. Random House: New
+ York. 227--235.
+
+The reason this was important to Quine is similar to the worries that Jim was talking about
+in the first class in which using non-referring expressions such as Santa Claus might commit
+one to believing in non-existant things. Quine's slogan was that "to be is to be the value of a variable."
+What this was supposed to mean is that if and only if an object could serve as the value of some variable, we
+are committed to recognizing the existence of that object in our ontology.
+Obviously, if there ARE no variables, this slogan has to be rethought.
+
+Quine did not appear to appreciate that Shoenfinkel had already invented combinatory logic, though
+he later wrote an introduction to Shoenfinkel's key paper reprinted in Jean
+van Heijenoort (ed) 1967 <cite>From Frege to Goedel, a source book in mathematical logic, 1879--1931</cite>.
+
+Cresswell has also developed a variable-free approach of some philosophical and linguistic interest
+in two books in the 1990's.
+
+A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is
+from combinatory logic (see especially his 2000 book, <cite>The Syntactic Processs</cite>). Steedman attempts to build
+a syntax/semantics interface using a small number of combinators, including T ≡ `\xy.yx`, B ≡ `\fxy.f(xy)`,
+and our friend S. Steedman used Smullyan's fanciful bird
+names for the combinators, Thrush, Bluebird, and Starling.
+
+Many of these combinatory logics, in particular, the SKI system,
+are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!