From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5282 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Re: to PTJ Date: Sun, 15 Nov 2009 22:07:51 +0100 Message-ID: References: Reply-To: Andrej Bauer NNTP-Posting-Host: lo.gmane.org Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1258328508 2164 80.91.229.12 (15 Nov 2009 23:41:48 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 15 Nov 2009 23:41:48 +0000 (UTC) To: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , categories@mta.ca Original-X-From: categories@mta.ca Mon Nov 16 00:41:41 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1N9oiv-0001BH-P7 for gsmc-categories@m.gmane.org; Mon, 16 Nov 2009 00:41:37 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1N9oMy-00041g-7Q for categories-list@mta.ca; Sun, 15 Nov 2009 19:18:56 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5282 Archived-At: On Sat, Nov 14, 2009 at 8:37 PM, Joyal, Andr=C3=A9 wr= ote: > 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) =3D z where the usual group-theoretic structure is related to // by x // y =3D x^(-1) y^(-1) x^(-1) =3D x // e x y =3D (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/ ]