Single Axiom for Groups

Stream: maths

[Tim Daly]

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

[David Michael Roberts]

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]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Kenny Lau]

models are required to be nonempty

[Reid Barton]

Mine aren't

[Kenny Lau]

my logic course says that they are nonempty

[Kenny Lau]

because you have the existential introduction rule

[Kenny Lau]

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

[Mario Carneiro]

could you give an example Reid?

[Kevin Buzzard]

The empty model?

[Reid Barton]

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]

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