On Sat, Nov 14, 2009 at 8:37 PM, Joyal, André <joyal.andre@uqam.ca> wrote:
I recall that Tarski is responsible for describing the theory of groups with a single binary operation satisfying a single equation. But dont have a reference with me.
A small point: the algebraic theory described by Tarski admits the empty set as a model. Strictly speaking, it is not equivalent to the theory of group.
The axiomatization of groups (excluding non-empty group) that is known to me from Borceux's handbook has a constant "e" for the unit and "double division" x // y governed by the axiom: x // (((x // y) // z) // (y // e))) // (e // e) = z where the usual group-theoretic structure is related to // by x // y = x^(-1) y^(-1) x^(-1) = x // e x y = (x // e) // (y // e) I usually use this example when I teach Lawvere's algebraic theories to explain that we might want a formulation of an (algebraic) theory that is "canonical" with respect to a choice of operations and axioms. The relevant reference is: W. McCune: Single axioms for groups and Abelian groups with various operations, Journal of Automated Reasoning, 1993, vol. 10, no. 1, p. 1--13. A non-evil link to this paper: ftp://info.mcs.anl.gov/pub/tech_reports/reports/P270.ps.Z (Never ever click on the first hit on Google when it points to Springer. This just increases their page rank but takes you to a stupid general page, not the paper itself. And even if it does, they'll try to sell it to you for some obscene amount of money.) Tarski's result is cited. The paper contains many other axiomatizations. The author used the Otter theorem prover extensively to find the axiomatizations. With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]