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? Martin