Lambek's lemma

Lambek's lemma

[Vaughan Pratt]

Lambek's lemma holds that every initial algebra is an isomorphism (and
dually for every final coalgebra).

With how small a diagram can you prove this?  Here's an argument with
five arrows.

TA --a--> A
  |        |
  |Tf      |f
  |        |
  v        v
TTA -Ta-> TA
.           \
.            \a
.             \
.             _\|
.
.                 A

Here f is the unique T-homomorphism from the initial T-algebra A to the
T-algebra TA, while the a arrow at lower right whiskers
(1-categorically) the square witnessing that f is a T-homomorphism.
This whisker creates another commutative square, namely afa = aTaTf =
aT(af).  The latter square therefore witnesses a homomorphism af: A -->
A. But by initiality there is only one such homomorphism, the identity,
whence af = 1.  Hence fa = TaTf (commutative diagram) = T(af) = T(1) =
1, whence f and a are mutual inverses.

I showed this argument to Peter Freyd in 1998 and his first response was
an argument with seven arrows that he felt was needed to make the
argument stick.  I suggested that his argument was simply a blow-up of
mine, which he agreed to half an hour later.

Lambek's lemma is somewhat reminiscent of Proposition 5 of Book I of
Euclid's *Elements*, that if two sides of a triangle are equal then
their opposite angles are equal.  This is the celebrated *Pons Asinorum*
or Bridge of Asses.  Applied here, the ability to prove Lambek's lemma
is a litmus test of whether you can think categorically.  (Personally I
consider the uniqueness of the free algebra on a given set as an
adequate test.)

Until recently Proposition 5 was always proved along the lines in
Euclid, cf.
http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI5.html .  Then
someone's computer program noticed that the triangles ABC and ACB (A
being the apex, with |AB| = |AC|) were congruent, from which the result
followed trivially.

Such a result would register about 2 on the New York Times' Richter
scale of earthshaking mathematical results, were it not for the fact
that it was first noticed by a computer (so the story went).

The sad thing is that even if this five-arrow proof of Lambek's lemma
had been first found by a computer, the New York Times could not have
whipped up the same enthusiasm for it as for the Pons Asinorum.  CT has
not yet acquired the visibility of geometry in the mind of the
technically literate public.

Vaughan Pratt

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Lambek's lemma

[Vaughan Pratt]

Vaughan Pratt wrote:
> Such a result [slicker proof of Euclid's Proposition 5] would register about 2 on the New York Times' Richter
> scale of earthshaking mathematical results, were it not for the fact
> that it was first noticed by a computer (so the story went).

True to form I neglected to expand on "so the story went" -- Pappus
noticed the same thing around 320 AD, cf
http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI5.html again.

Vaughan


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Lambek's lemma

[Charles Wells]

Isosceles triangles caused a bit of discussion on the mathedu mailing
list recently, starting at
http://mathforum.org/kb/message.jspa?messageID=6864271&tstart=0
(isosceles triangles only appear a couple of levels down and then the
discussion gets quite heated.) . I also wrote about it here:
http://sixwingedseraph.wordpress.com/2009/10/23/naive-proofs/ in
connection with the possibility of their being a generic triangle.

Wikipedia says the proof of the pons asinorum by mirror image was by Pappus.

Charles Wells

On Thu, Nov 12, 2009 at 1:07 AM, Vaughan Pratt <pratt@cs.stanford.edu> wrote:
> Lambek's lemma holds that every initial algebra is an isomorphism (and
> dually for every final coalgebra).
>
> With how small a diagram can you prove this?  Here's an argument with
> five arrows.
>
> TA --a--> A
>  |        |
>  |Tf      |f
>  |        |
>  v        v
> TTA -Ta-> TA
> .           \
> .            \a
> .             \
> .             _\|
> .
> .                 A
>
> Here f is the unique T-homomorphism from the initial T-algebra A to the
> T-algebra TA, while the a arrow at lower right whiskers
> (1-categorically) the square witnessing that f is a T-homomorphism.
> This whisker creates another commutative square, namely afa = aTaTf =
> aT(af).  The latter square therefore witnesses a homomorphism af: A -->
> A. But by initiality there is only one such homomorphism, the identity,
> whence af = 1.  Hence fa = TaTf (commutative diagram) = T(af) = T(1) =
> 1, whence f and a are mutual inverses.
>
> I showed this argument to Peter Freyd in 1998 and his first response was
> an argument with seven arrows that he felt was needed to make the
> argument stick.  I suggested that his argument was simply a blow-up of
> mine, which he agreed to half an hour later.
>
> Lambek's lemma is somewhat reminiscent of Proposition 5 of Book I of
> Euclid's *Elements*, that if two sides of a triangle are equal then
> their opposite angles are equal.  This is the celebrated *Pons Asinorum*
> or Bridge of Asses.  Applied here, the ability to prove Lambek's lemma
> is a litmus test of whether you can think categorically.  (Personally I
> consider the uniqueness of the free algebra on a given set as an
> adequate test.)
>
> Until recently Proposition 5 was always proved along the lines in
> Euclid, cf.
> http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI5.html .  Then
> someone's computer program noticed that the triangles ABC and ACB (A
> being the apex, with |AB| = |AC|) were congruent, from which the result
> followed trivially.
>
> Such a result would register about 2 on the New York Times' Richter
> scale of earthshaking mathematical results, were it not for the fact
> that it was first noticed by a computer (so the story went).
>
> The sad thing is that even if this five-arrow proof of Lambek's lemma
> had been first found by a computer, the New York Times could not have
> whipped up the same enthusiasm for it as for the Pons Asinorum.  CT has
> not yet acquired the visibility of geometry in the mind of the
> technically literate public.
>
> Vaughan Pratt
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>



-- 
professional website: http://www.cwru.edu/artsci/math/wells/home.html
blog: http://sixwingedseraph.wordpress.com/
abstract math website: http://www.abstractmath.org/MM//MMIntro.htm
astounding math stories: http://www.abstractmath.org/MM//MMAstoundingMath.htm
personal website:  http://www.abstractmath.org/Personal/index.html
sixwingedseraph.facebook.com


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Lambek's lemma

[Prof. Peter Johnstone]

Vaughan's argument appears in the Elephant (but with the second square,
which he has indicated by dots, drawn in, so that there are seven arrows)
as Lemma A1.1.4. Though it's not credited there, I learned it from
Peter Freyd --- I can't remember when, but that part of the Elephant
was written well before 1998.

Peter Johnstone
-----------------------
On Wed, 11 Nov 2009, Vaughan Pratt wrote:

> Lambek's lemma holds that every initial algebra is an isomorphism (and
> dually for every final coalgebra).
>
> With how small a diagram can you prove this?  Here's an argument with
> five arrows.
>
> TA --a--> A
> |        |
> |Tf      |f
> |        |
> v        v
> TTA -Ta-> TA
> .           \
> .            \a
> .             \
> .             _\|
> .
> .                 A
>
> Here f is the unique T-homomorphism from the initial T-algebra A to the
> T-algebra TA, while the a arrow at lower right whiskers
> (1-categorically) the square witnessing that f is a T-homomorphism.
> This whisker creates another commutative square, namely afa = aTaTf =
> aT(af).  The latter square therefore witnesses a homomorphism af: A -->
> A. But by initiality there is only one such homomorphism, the identity,
> whence af = 1.  Hence fa = TaTf (commutative diagram) = T(af) = T(1) =
> 1, whence f and a are mutual inverses.
>
> I showed this argument to Peter Freyd in 1998 and his first response was
> an argument with seven arrows that he felt was needed to make the
> argument stick.  I suggested that his argument was simply a blow-up of
> mine, which he agreed to half an hour later.
>
> Lambek's lemma is somewhat reminiscent of Proposition 5 of Book I of
> Euclid's *Elements*, that if two sides of a triangle are equal then
> their opposite angles are equal.  This is the celebrated *Pons Asinorum*
> or Bridge of Asses.  Applied here, the ability to prove Lambek's lemma
> is a litmus test of whether you can think categorically.  (Personally I
> consider the uniqueness of the free algebra on a given set as an
> adequate test.)
>
> Until recently Proposition 5 was always proved along the lines in
> Euclid, cf.
> http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI5.html .  Then
> someone's computer program noticed that the triangles ABC and ACB (A
> being the apex, with |AB| = |AC|) were congruent, from which the result
> followed trivially.
>
> Such a result would register about 2 on the New York Times' Richter
> scale of earthshaking mathematical results, were it not for the fact
> that it was first noticed by a computer (so the story went).
>
> The sad thing is that even if this five-arrow proof of Lambek's lemma
> had been first found by a computer, the New York Times could not have
> whipped up the same enthusiasm for it as for the Pons Asinorum.  CT has
> not yet acquired the visibility of geometry in the mind of the
> technically literate public.
>
> Vaughan Pratt
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Lambek's lemma

[Vaughan Pratt]

Prof. Peter Johnstone wrote:
> Vaughan's argument appears in the Elephant

Oops, I keep forgetting to check there for these things, sorry Peter!

> (but with the second square,
> which he has indicated by dots, drawn in, so that there are seven arrows)

Actually my dots were not to indicate the second square but merely to
prevent mail forwarding programs from deleting initial spaces on lines.
  I don't know why they do so, but it screws up formatting of ASCII
diagrams.

 > Though it's not credited there, I learned it from
> Peter Freyd --- I can't remember when, but that part of the Elephant
> was written well before 1998.

The reason it came up in 1998 is that I was preparing a lecture then for
my algebraic logic class and was trying to reconstruct the proof I'd
seen Peter F. give some years earlier (for all I know PTJ and I heard
PJF give it at the same talk).  I came up with the five-arrow diagram
and sent it to PJF asking if that was his proof.  He replied "I don't
see where you proved that fa = 1. Here's the way I'd present it," and
sent me the seven-arrow diagram as per the Elephant's Lemma A1.1.4.
Some discussion ensued, the outcome of which was that he agreed I'd
proved fa = 1 after all.

I thought no more of this until a couple of days ago when I suggested to
Mikael Vejdemo-Johansson, who is teaching a CT course here at Stanford
this quarter, that he present Lambek's lemma.  Reviewing my
correspondence with PJF, it occurred to me that people ought to know
that the second square could be suppressed for the sake of two fewer
arrows in the diagram, FWIW as they say, whence my message.

Mathematically speaking this observation is a triviality (which is why
PTJ is comfortable calling the 5-arrow and 7-arrow diagrams "the same").

But by the same token the Reidemeister moves are a triviality inasmuch
as they relate "the same" knots.  (As a meta-Reidemeister move let me
remark that the first time I saw the Reidemeister moves was when I was
writing my fourth year honours thesis in Pure Maths at Sydney in 1965,
in a class of 14 that included Ross Street and Brian Day, for which I'd
chosen knot theory after grinding to a halt trying to write about
Riemannian manifolds without any supervision--I found I could at least
read the knot theory literature without supervision!  My knee-jerk
reaction to the Reidemeister moves was "how is this mathematics?" and I
moved on to the Alexander polynomial and other algebraic techniques,
about which I wrote some ninety pages of typical undergraduate
misunderstandings, none of which mentioned the Reidemeister moves.  This
was well before either Conway's reworking of the Alexander polynomial
(when I was just starting Berkeley's CS PhD program) or, 14 years after
Conway, Vaughan Jones' polynomial (when I was working at Sun
Microsystems).  My real interest in 1965 was theoretical physics, for
which I hoped honours math would be good preparation for honours
physics.  But then in 1967 computers happened along as yet another
career option.)

Getting back to whether 5 is any smaller than 7, there is something
disconcerting about the righthand square in A1.1.4 (page 6 of the
Elephant), since it asserts that aTa = aTa.  Why should the equation x=x
have to take up fully 50% of the diagram proving Lambek's lemma?  My
reconstruction of PJF's proof did not deem x=x worthy of such a large
share of the proof.

This is the sort of argument only a proof theorist could love.  PTJ is
quite right when he says these are the same proof.  Being no less a
Platonist than anyone on this list, I said as much in my reply to PJF in
1998.

On the other hand, what sort of Platonist would reject 5 < 7?

Vaughan Pratt

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Lambek's lemma

[Steve Vickers]

Dear Vaughan,

I used the same argument in "Topical Categories of Domains" Propn 2.3.7
(published 1999, though long in the gestation). I remarked "We briefly
recall the usual argument", so I'm not claiming any priority. As I
recall I had little trouble working out the proof for myself, but I knew
the result as folklore and assumed any simple proofs would be part of
the same folklore.

(Actually, my result is slightly more general. I was working in a
2-category (of Toposes) that, unlike Cat, is not well-pointed. Given the
endo-1-cell T, I assumed that the 0-cell A of T-algebras (the inserter
from T to the identity) had a global point - a 1-cell from 1 to A - that
was strongly initial in the sense that it was left adjoint to the unique
1-cell A -> 1. In my context the simple argument still worked.)

Regards,

Steve.

Vaughan Pratt wrote:
> Lambek's lemma holds that every initial algebra is an isomorphism (and
> dually for every final coalgebra).
>
> With how small a diagram can you prove this?  Here's an argument with
> five arrows.
>
> TA --a--> A
>  |        |
>  |Tf      |f
>  |        |
>  v        v
> TTA -Ta-> TA
> .           \
> .            \a
> .             \
> .             _\|
> .
> .                 A
>
> Here f is the unique T-homomorphism from the initial T-algebra A to the
> T-algebra TA, while the a arrow at lower right whiskers
> (1-categorically) the square witnessing that f is a T-homomorphism.
> This whisker creates another commutative square, namely afa = aTaTf =
> aT(af).  The latter square therefore witnesses a homomorphism af: A -->
> A. But by initiality there is only one such homomorphism, the identity,
> whence af = 1.  Hence fa = TaTf (commutative diagram) = T(af) = T(1) =
> 1, whence f and a are mutual inverses.
>
> I showed this argument to Peter Freyd in 1998 and his first response was
> an argument with seven arrows that he felt was needed to make the
> argument stick.  I suggested that his argument was simply a blow-up of
> mine, which he agreed to half an hour later.
>
> Lambek's lemma is somewhat reminiscent of Proposition 5 of Book I of
> Euclid's *Elements*, that if two sides of a triangle are equal then
> their opposite angles are equal.  This is the celebrated *Pons Asinorum*
> or Bridge of Asses.  Applied here, the ability to prove Lambek's lemma
> is a litmus test of whether you can think categorically.  (Personally I
> consider the uniqueness of the free algebra on a given set as an
> adequate test.)
>
> Until recently Proposition 5 was always proved along the lines in
> Euclid, cf.
> http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI5.html .  Then
> someone's computer program noticed that the triangles ABC and ACB (A
> being the apex, with |AB| = |AC|) were congruent, from which the result
> followed trivially.
>
> Such a result would register about 2 on the New York Times' Richter
> scale of earthshaking mathematical results, were it not for the fact
> that it was first noticed by a computer (so the story went).
>
> The sad thing is that even if this five-arrow proof of Lambek's lemma
> had been first found by a computer, the New York Times could not have
> whipped up the same enthusiasm for it as for the Pons Asinorum.  CT has
> not yet acquired the visibility of geometry in the mind of the
> technically literate public.
>
> Vaughan Pratt



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Lambek's lemma

[Prof. Peter Johnstone]

Dear Vaughan,

Of course I agree with you that, logically, there is no point in
drawing a commutative square to prove that x = x. I also agree that
5 < 7. But I think there is still some point in drawing the second
square in A1.1.4, at least in pedagogical terms: until you've seen
(or at least visualized) the second square, it's hard for the mind
to accept the argument that says af = 1. (I feel strongly about this,
having spent two hours this afternoon in an examples class for the
students attending my first-year graduate course on category theory.)
And, as someone (I forget who, but it may have been Mike Barr) pointed
out long ago, one can (well, almost) define the variety of groups
as the variety defined by a single binary operation satisfying a
single equation; 1 < 3, but no sane group-theorist would do it
that way.

Peter
-------------------
On Fri, 13 Nov 2009, Vaughan Pratt wrote:

> Prof. Peter Johnstone wrote:
>> Vaughan's argument appears in the Elephant
>
> Oops, I keep forgetting to check there for these things, sorry Peter!
>
>> (but with the second square,
>> which he has indicated by dots, drawn in, so that there are seven arrows)
>
> Actually my dots were not to indicate the second square but merely to
> prevent mail forwarding programs from deleting initial spaces on lines.
> I don't know why they do so, but it screws up formatting of ASCII
> diagrams.
>
>> Though it's not credited there, I learned it from
>> Peter Freyd --- I can't remember when, but that part of the Elephant
>> was written well before 1998.
>
> The reason it came up in 1998 is that I was preparing a lecture then for
> my algebraic logic class and was trying to reconstruct the proof I'd
> seen Peter F. give some years earlier (for all I know PTJ and I heard
> PJF give it at the same talk).  I came up with the five-arrow diagram
> and sent it to PJF asking if that was his proof.  He replied "I don't
> see where you proved that fa = 1. Here's the way I'd present it," and
> sent me the seven-arrow diagram as per the Elephant's Lemma A1.1.4.
> Some discussion ensued, the outcome of which was that he agreed I'd
> proved fa = 1 after all.
>
> I thought no more of this until a couple of days ago when I suggested to
> Mikael Vejdemo-Johansson, who is teaching a CT course here at Stanford
> this quarter, that he present Lambek's lemma.  Reviewing my
> correspondence with PJF, it occurred to me that people ought to know
> that the second square could be suppressed for the sake of two fewer
> arrows in the diagram, FWIW as they say, whence my message.
>
> Mathematically speaking this observation is a triviality (which is why
> PTJ is comfortable calling the 5-arrow and 7-arrow diagrams "the same").
>
> But by the same token the Reidemeister moves are a triviality inasmuch
> as they relate "the same" knots.  (As a meta-Reidemeister move let me
> remark that the first time I saw the Reidemeister moves was when I was
> writing my fourth year honours thesis in Pure Maths at Sydney in 1965,
> in a class of 14 that included Ross Street and Brian Day, for which I'd
> chosen knot theory after grinding to a halt trying to write about
> Riemannian manifolds without any supervision--I found I could at least
> read the knot theory literature without supervision!  My knee-jerk
> reaction to the Reidemeister moves was "how is this mathematics?" and I
> moved on to the Alexander polynomial and other algebraic techniques,
> about which I wrote some ninety pages of typical undergraduate
> misunderstandings, none of which mentioned the Reidemeister moves.  This
> was well before either Conway's reworking of the Alexander polynomial
> (when I was just starting Berkeley's CS PhD program) or, 14 years after
> Conway, Vaughan Jones' polynomial (when I was working at Sun
> Microsystems).  My real interest in 1965 was theoretical physics, for
> which I hoped honours math would be good preparation for honours
> physics.  But then in 1967 computers happened along as yet another
> career option.)
>
> Getting back to whether 5 is any smaller than 7, there is something
> disconcerting about the righthand square in A1.1.4 (page 6 of the
> Elephant), since it asserts that aTa = aTa.  Why should the equation x=x
> have to take up fully 50% of the diagram proving Lambek's lemma?  My
> reconstruction of PJF's proof did not deem x=x worthy of such a large
> share of the proof.
>
> This is the sort of argument only a proof theorist could love.  PTJ is
> quite right when he says these are the same proof.  Being no less a
> Platonist than anyone on this list, I said as much in my reply to PJF in
> 1998.
>
> On the other hand, what sort of Platonist would reject 5 < 7?
>
> Vaughan Pratt
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

to PTJ

[Joyal, André]

Hi Peter,

>And, as someone (I forget who, but it may have been Mike Barr) pointed
>out long ago, one can (well, almost) define the variety of groups
>as the variety defined by a single binary operation satisfying a
>single equation; 1 < 3, but no sane group-theorist would do it
>that way.

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. 

Best,
André



-------- Message d'origine--------
De: categories@mta.ca de la part de Prof. Peter Johnstone
Date: ven. 13/11/2009 16:49
À: Vaughan Pratt; categories@mta.ca
Objet : categories: Re: Lambek's lemma
 
Dear Vaughan,

Of course I agree with you that, logically, there is no point in
drawing a commutative square to prove that x = x. I also agree that
5 < 7. But I think there is still some point in drawing the second
square in A1.1.4, at least in pedagogical terms: until you've seen
(or at least visualized) the second square, it's hard for the mind
to accept the argument that says af = 1. (I feel strongly about this,
having spent two hours this afternoon in an examples class for the
students attending my first-year graduate course on category theory.)
And, as someone (I forget who, but it may have been Mike Barr) pointed
out long ago, one can (well, almost) define the variety of groups
as the variety defined by a single binary operation satisfying a
single equation; 1 < 3, but no sane group-theorist would do it
that way.

Peter

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Lambek's lemma

[Vaughan Pratt]

Prof. Peter Johnstone wrote:
> But I think there is still some point in drawing the second
> square in A1.1.4, at least in pedagogical terms: until you've seen
> (or at least visualized) the second square, it's hard for the mind
> to accept the argument that says af = 1.

Agreed 1000% (UK: 100%).  In fact it could serve as a real-world example
of the difference an extra square can make in a diagrammatic argument
whose verbal counterpart gains nothing from it.  As such it would be
interesting grist for the mill currently being ground more finely lately
by those interested in diagrammatic reasoning, represented here by Sol
Feferman who's been taking quite an active interest in it lately.

(Even though I'm more of a visual thinker, quite the opposite of Gordon
Plotkin for example who considers himself as verbal as I am visual, for
some reason I tend to view commutative diagrams as more verbal than
visual, perhaps because my ability to visualize makes it clearer to me
that they are depicting equations between words and are therefore really
verbal entities, appearances notwithstanding.  This would help explain
my lack of enthusiasm for the second square.  But I would still draw it
explicitly if teaching the lemma, just like you.)

> And, as someone (I forget who, but it may have been Mike Barr) pointed
> out long ago, one can (well, almost) define the variety of groups
> as the variety defined by a single binary operation satisfying a
> single equation; 1 < 3, but no sane group-theorist would do it
> that way.

Substitute "Boolean algebra" for "group" and one finds in Stephen
Wolfram's ANKS the same claim: one binary operation, satisfying one
equation; in this case 1 < 12 or thereabouts when defining a Boolean
algebra as a complemented distributive lattice.  I'm sure Stephen is
under no delusions as to the pedagogical benefits of his definition.

Unfortunately neither definition is correct because both varieties so
defined have as their initial object the "empty group," resp. "empty
Boolean algebra," one, resp. two, elements too few.  Or did you not
count e when you said "one binary operation?"

Vaughan


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: to PTJ

[burroni]

Hi,
You can find this equation (and ref to Higman and Neumann) in the GTM  
springer no 26 page 7 : E.G. manes "Algebraic Theory.
      xxxdydzdxxdxdzddd=y
(polish notations and d is the binary operation.)

Best,
Albert

"Joyal, André" <joyal.andre@uqam.ca> a écrit :

> Hi Peter,
>
>> And, as someone (I forget who, but it may have been Mike Barr) pointed
>> out long ago, one can (well, almost) define the variety of groups
>> as the variety defined by a single binary operation satisfying a
>> single equation; 1 < 3, but no sane group-theorist would do it
>> that way.
>
> 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.
>
> Best,
> André
>
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: to PTJ

[Andrej Bauer]

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/ ]

Re: to PTJ

[Ronnie Brown]

I am curious to know how all this fits with partial algebraic 
operations. The axioms for a groupoid allow for the empty groupoid. That 
reminds me that Philip Higgins wrote about partial algebraic structures in

@article {Higgins-algebrawithoperators,
    AUTHOR = {Higgins, Philip J.},
     TITLE = {Algebras with a scheme of operators},
   JOURNAL = {Math. Nachr.},
  FJOURNAL = {Mathematische Nachrichten},
    VOLUME = {27},
      YEAR = {1963},
     PAGES = {115--132},
      ISSN = {0025-584X},
   MRCLASS = {18.10},
  MRNUMBER = {MR0163940 (29 \#1239)},
MRREVIEWER = {A. Heller},
}

and he told me that years later he got a paper from a computer scientist 
saying `Higgins' theorem is true as stated' , which apparently concerned 
the empty structure!

Does anyone on this list know a reference for axioms for group theory 
which are related to Dakin's axioms for a simplicial T-complex;
1) degenerate implies thin;
2) every horn has a unique thin filler;
3) if all faces but one of a thin element are thin, then so also is the 
remaining face.

The last axiom is related to associativity. I am sure I had a reference 
at one time, but have lost it.

Ronnie Brown

burroni@math.jussieu.fr wrote:
> Hi,
> You can find this equation (and ref to Higman and Neumann) in the GTM 
> springer no 26 page 7 : E.G. manes "Algebraic Theory.
>      xxxdydzdxxdxdzddd=y
> (polish notations and d is the binary operation.)
>
> Best,
> Albert
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]