1:56 PM
@Threnody No. It's exactly as you wrote. And it's good that you wrote it exactly in that way. Sorry I didn't notice you finished posting it.
You're missing some "·" in (4), though.
Your version is not quite right.
If you want to have the symbol "e", you cannot just axiomatize (G,·), but rather (G,e,·). Otherwise, your (4) even with the "·"s added is meaningless (because e is not defined).
To save time, I'll give you the correct version, but you must make sure you can subsequently produce it correctly by yourself:
(1) e∈G. ·∈func(G,G).
(2) ∀x,y,z∈G ( x·(y·z) = (x·y)·z ).
(3) ∀x∈G ( x·e = e·x = x ).
(4) ∀x∈G ∃y∈G ( x·y = y·x = e ).
Well I decided to change (1) to include the axiomatization of e as an element as well as properly define the meaning of ·.
In conventional FOL, (1) will be captured by the language of the theory, and only (2) to (4) are axioms of the theory of groups.
But I want to use my variant of FOL, as it is more practical and also it is pedagogically better.
So... The proof that the identity is unique is simply the proof (over FOL) that those axioms imply ∀x∈G ∃!y∈G ( x·y=y·x = e ).
In other words, using nothing but the rules in my deductive system for FOL, you can literally prove that statement.
Oops! Sorry I don't know what I was writing for (1).
It's a binary function, so of course input is from G^2.
Also we need to stipulate that · is syntactically written as an infix operation, so that those syntax like "x·(y·z)" make sense.
So with these details down, we have truly set up the axiomatization of the theory of groups.
Although this axiomatization is in the meta-system, all the quantifiers are over G, and we can ensure that you (essentially) cannot prove more than the theory of groups by replacing (1) with:
(1') e∈G. ∀x,y∈G ( x·y∈G ).
So why do I want the meta-system version? Because we can directly start doing group theory, which is outside the theory of groups, without needing to talk about models of the theory of groups.
For example, a group (G,e,·) is called cyclic iff ∃u∈G ∀x∈G ( ... ). What is filled in the blank? @Threnody