Zulip Chat Archive

Stream: maths

Topic: Single Axiom for Groups


view this post on Zulip Tim Daly (Oct 25 2019 at 03:19):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 28 2019 at 00:09):

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

view this post on Zulip 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]

view this post on Zulip Reid Barton (Oct 28 2019 at 00:29):

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

view this post on Zulip Reid Barton (Oct 28 2019 at 00:30):

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

view this post on Zulip Kenny Lau (Oct 28 2019 at 00:31):

models are required to be nonempty

view this post on Zulip Reid Barton (Oct 28 2019 at 00:32):

Mine aren't

view this post on Zulip Kenny Lau (Oct 28 2019 at 00:33):

my logic course says that they are nonempty

view this post on Zulip Kenny Lau (Oct 28 2019 at 00:33):

because you have the existential introduction rule

view this post on Zulip Kenny Lau (Oct 28 2019 at 00:33):

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

view this post on Zulip Mario Carneiro (Oct 28 2019 at 00:34):

could you give an example Reid?

view this post on Zulip Kevin Buzzard (Oct 28 2019 at 00:38):

The empty model?

view this post on Zulip 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.)

view this post on Zulip 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