# Is it possible to check the validity of the following theorem in Group Theory automatically by a computer? If so, how?

I'm learning right now how to prove the following very basic theorem in Group Theory, which we learn in a Linear Algebra course in my university (I study Computer Science):

Let's have a group $$(M,*)$$ and $$a,b\in M$$. Then $$x=a^{-1}*b$$ is the only solution to the equation $$a*x=b$$.

I know how to proof the theorem in a "Linear Algebra style". First, I would show that $$x=a^{-1}*b$$ is a solution to the equation $$a*x=b$$, for example like this: $$a*(a^{-1}*b) = (a*a^{-1})*b = e*b = b$$ . Then I would show that it is the only solution to that equation and the proof would be done (at least my university professor would accept it).

However, in the Linear Algebra course we don't use the style of a proof that I have learnt in a Mathematical Logic course that I've just completed (e.g. we were learning to proof a particular logical consequence of a set of first order logic formulas by a method called semantic trees). I wonder, how this proof of the theorem would look like in this purely "Mathematical Logic style", e.g. by using a semantic tree method or some other method which a computer could use to check whether the theorem logically follows from the axioms of the Group Theory.

Suppose I have the following definition of a Group Theory (this definition we learnt in a Mathematical Logic course):

$$\mathscr L=\{f,e\}$$ is a language, where $$f$$ is a binary function symbol and $$e$$ is a constant called "neutral element". The theory of groups has these axioms:

1. Associativity: $$(\forall x)(\forall y)(\forall z)(f(f(x,y),z))=f(x,f(y,z))$$
2. Identity: $$(\forall x)(f(x,e)=x)$$
3. Inverse: $$(\forall x)(\exists z)(f(x,z)=e)$$

If it is possible, how do I check the validity of the theorem in a purely formal logical way (for example by a semantic tree method) so that even a computer can check the validity?

• The theory of groups does not have commutativity. Anyway, you can always rewrite your proof as a sequence of $\implies$, instantiation and modus ponens, etc. Jul 16, 2020 at 9:12
• You declare $e$ to ba a right identity, and the existence of right inverses. For groups, you also need left identity and left inverses (you don't need to state that the left inverse equals the right inverse; that one can be proven). Jul 16, 2020 at 10:11