[FOM] identities

Vladimir Sazonov V.Sazonov at csc.liv.ac.uk
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 

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.

More information about the FOM mailing list