## Stream: maths

### Topic: Single Axiom for Groups

#### Tim Daly (Oct 25 2019 at 03:19):

http://ftp.mcs.anl.gov/pub/tech_reports/reports/P270.pdf

#### David Michael Roberts (Oct 27 2019 at 22:22):

When I was a student I vainly tried to prove (on paper) the usual axioms from that single axiom (the first one given, in terms of division), without looking at the existing proof. I didn't get very far.

#### Kevin Buzzard (Oct 28 2019 at 00:09):

That looks like a job for...automatic theorem provers!

#### Kevin Buzzard (Oct 28 2019 at 00:17):

Where do you even start? I guess proving that x/x is independent of x would be a nice beginning, because then you can define inverse and then, finally, multiplication [assuming you just start with a division]

#### Reid Barton (Oct 28 2019 at 00:29):

IMO all of these equational theories have an obvious model which is not a group

#### Reid Barton (Oct 28 2019 at 00:30):

except (2.2) I think (and obviously the standard one)

#### Kenny Lau (Oct 28 2019 at 00:31):

models are required to be nonempty

Mine aren't

#### Kenny Lau (Oct 28 2019 at 00:33):

my logic course says that they are nonempty

#### Kenny Lau (Oct 28 2019 at 00:33):

because you have the existential introduction rule

#### Kenny Lau (Oct 28 2019 at 00:33):

$Q(a)\to \ \exists {x}\,Q(x)$

#### Mario Carneiro (Oct 28 2019 at 00:34):

could you give an example Reid?

The empty model?

#### Reid Barton (Oct 28 2019 at 00:44):

Traditionally models are assumed to be nonempty. But that doesn't work in categorical logic, for example. The category of models of any algebraic theory has an initial object, and if the theory has no constant symbols then that initial object is empty. (There's no initial object in the category of nonempty sets for example.)

#### Reid Barton (Oct 28 2019 at 00:45):

Yes, the traditional assumption has something to do with the funny semantics of formulas with free variables

Last updated: May 06 2021 at 19:30 UTC