[FOM] identities

Sat Jan 20 10:14:54 EST 2007

```Quoting martin at eipye.com Thu, 18 Jan 2007:

> An "identity" is a sentence that can be expressed as the
> universal quaqntification of an ideintity. A friend has
> asked whether there is an algorithm for determining
> whether a given identity is implied by a given finite set
> of identities. Surely this is known to be unsolvable.
> References?

I think this may be any textbook on lambda/combinatory calculus (say,
by Barendregt).

One version of the theory of combinators (Schönfinkel and Curry)
consists of two equations for two constants S and K and binary
operation of "application" x,y |--> xy satisfying the identities:

((Sx)y)z = (xz)(yz).

(Kx)y = x.

Combinatory terms can define arbitrary partial recursive function under
special representation of natural numbers as "iteratots" Z_n:

|- (Z_n f)x = f^n x (f applied n times to x)

with Z_n definable as a combinatory term consisting of S and K.

Thus, the undecidability of this theory follows.

Combinators were also used by Statman to show non-elementary complexity
of cut-elimination (or something close to that related with Herbrand
theorem).

P.S. It seems Kleene witnessed that he has found how to subtract one
(Z_n |--> Z_{n-1} -- an essential step necessary to define any PRF by
combinators or lambda terms) while sitting in the dentist's chair.

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

```