Unsolvable problems for equational theories.
Peter G. Perkins · Notre Dame Journal of Formal Logic · 1967
In 1954 R. Lyndon [7] gave an example of a sevenelement groupoid whose identities cannot be deduced from any finite subset.That is, they are not "finitely based."In this paper we present some by-products of an unsuccessful attempt to find, or prove the non-existence of, an effective procedure which would determine of an arbitrary finite groupoid whether or not its identities have a finite basis.Included are the undecidability of certain questions of provability, equational completeness, consistency, and being the basis of the identities of some finite groupoid when asked of finite as well as recursive sets of equations.*2. Preliminaries.We consider, for the most part, algebras of the type .21 = (Λ o , Θ) with one binary operation θ on a set A o and commonly called groupoids.The generalizations of the notions and definitions that follow to any number of finitary operations, including specified constants, are the obvious ones.Associated with 21 is the language and deductive structure described below.Language. 1) The set of variables is {w, x, y, z, w ly x^ . . .} .2) The set of terms is the smallest set containing the variables and such that if s and t are terms then (s + t) is a term, the set of subterms of a variable υ is {v}.The set of subterms of (s + t) is the set consisting of (s + t) together with the subterms of s and the subterms of t.3) The set of equations is the set {s = t : s, t are terms}.Rules of deduction.Let r, s, t, u be terms.The following deductions may be made.E1 s = t from r = u if s = t is the result of substituting a term for a variable throughout r ~ u.