In a set $X$ we define a binary operation $*$ such that
$\forall x, y \in X,\ (x*y)*y=y*(y*x)=x.$
Is $*$ commutative and why?
In a set $X$ we define a binary operation $*$ such that
$\forall x, y \in X,\ (x*y)*y=y*(y*x)=x.$
Is $*$ commutative and why?
Yes, it is commutative. Here is why : $ x * y = y*(y*(x*y)) = y * ((x * (x*y))*(x*y)) = y *x. $ I first use the identity to multiply by $y$ on the left twice, and then I replace the second $y$ by $x*(x*y)$. Then we use the fact that $ (x * (x * y))*(x*y) = x $ to remove the bigger chunk.
Hope that helps,
Ah, I think I got a counterexample:
Consider the free monoid $F_2$ on 2 letters $a,b$ (with empty word '$1$'), and consider its quotient $X:=F_2/(w^2\sim 1) $ for all words $w\in F_2$. Then, basically $X$ contains those words which doesn't have any substring of the form $ww$, and if such appears at a concatenation, they get just cancelled. For example $aba\cdot ab= a$.
Update: not good, as it is going to be a group, $xy=yx$ will follow from all $x^2=1$...
Here's a proof that uses the automated theorem prover Prover9.
As a human, I find the output of these things difficult to read, but I find they can help by (a) suggesting an important in-between step, and (b) give a proof (even if it is unreadable), which means the result we're trying to prove is actually true, and it is possible there is a proof with a number of steps that could be understood by humans. (Also, there is a "coolness factor" to automated proofs.)
Here's the input:
formulas(assumptions). (x * y) * y = x. y * (y * x) = x. end_of_list. formulas(goals). x * y = y * x. end_of_list.
and a trimmed version of the output:
============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 7. % Level of proof is 3. % Maximum clause weight is 7. % Given clauses 4. 1 x * y = y * x # label(non_clause) # label(goal). [goal]. 2 (x * y) * y = x. [assumption]. 3 x * (x * y) = y. [assumption]. 4 c2 * c1 != c1 * c2. [deny(1)]. 5 x * (y * x) = y. [para(3(a,1),2(a,1,1))]. 7 x * y = y * x. [para(2(a,1),5(a,1,2))]. 8 $F. [resolve(7,a,4,a)]. ============================== end of proof ==========================