[FOM] identities

[Vladimir Sazonov]

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).


Vladimir Sazonov

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.