This is a natural follow-up to my previous question, here: [A question regarding equational bases of the theory of the commutative and associative properties](https://mathoverflow.net/questions/409080/a-question-regarding-equational-bases-of-the-theory-of-the-commutative-and-assoc). As before, suppose we are working in the signature of a single binary operation $+$. Also as before, let $S$ be a set of equations which generate precisely the same equational theory generated by the set containing the commutative and associative equations: $\{x+y=y+x,x+(y+z)=(x+y)+z\}$. Now, suppose that the cardinality of $S$ is finite and greater than or equal to $3$. Must $S$ have at least $|S| - 2$ redundant axioms, where $|S|$ is the cardinality of $S$? I conjecture that it must, and moreover I make the stronger conjecture that there exists a subset $T$ of $S$ which has cardinality $|S|-2$, such that the set difference $S - T$ generates the same equational theory as the set of commutativity and associativity. In other words, not only are there $|S|-2$ redundant axioms, but the redundant axioms are "set-wise" redundant, not merely individually redundant. Is my stronger conjecture true? If not, is at least my weaker conjecture true?



Follow up to a question on equational bases of the theory of the commutative and associative properties
In more simple terms, you want to show that if $S$ is any set of equations equivalent to $\def\ac{\mathrm{AC}}\ac=\{x+y=y+x,x+(y+z)=(x+y)+z\}$, then there exists $T\subseteq S$ of size $2$ such that $T$ is already equivalent to $\ac$.


This follows from the answer to the linked question: since $\ac$ is finite, $S$ is equivalent to a finite subtheory; then if $T\subseteq S$ is a minimal finite subset equivalent to $\ac$, we cannot have $|T|\ge3$ by the linked answer, hence $|T|\le2$.


In fact, let me give a simpler argument that shows more: $S$ must “essentially” contain $\ac$ as a subset. More precisely, up to renaming of variables, it contains the commutative law $x+y=y+x$, and it contains an equation equivalent to the associative law $x+(y+z)=(x+y)+z$ modulo commutativity:



> 
> **Proposition:** If $S$ is equivalent to $\ac$, then up to renaming of variables, $S$ contains the equation $x+y=y+x$, and an equation $t=s$ where $t\in\{x+(y+z),x+(z+y),(y+z)+x,(z+y)+x\}$ and $s\in\{(x+y)+z,(y+x)+z,z+(x+y),z+(y+x)\}$.
> 
> 
> 


**Proof:**


Recall that an equation $t=s$ follows from $S$ iff it has an equational $S$-proof: a sequence of terms $t\_0,\dots,t\_n$ such that $t\_0$ is $t$, $t\_n$ is $s$, and each $t\_i=t\_{i+1}$ is an instance of an equation $e\in S$ (i.e., $t\_{i+1}$ results from $t\_i$ by replacing a subterm $u$ with a term $v$ where one of $u=v$ or $v=u$ is a substitution instance of $e$).


An equation $t=s$ is provable in $S\equiv\ac$ iff each variable has the same number of occurrences in $t$ and $s$. It follows that if $t\_0,\dots,t\_n$ is an $S$-proof, then all the terms $t\_i$ have the same number of occurrences of each variable.


Since $S\equiv\ac$, there is an $S$-proof of $x+y=y+x$. By the property above, the only terms that can occur in such a proof are $x+y$ and $y+x$, thus the only possibility is that $x+y=y+x$ is an instance of an equation $e\in S$. Since this equation is not an instance of any strictly shorter equation valid in $\ac$, it follows that $e$ is $x+y=y+x$ itself up to renaming of variables.


Likewise, there is an $S$-proof of $x+(y+z)=(x+y)+z$. The only terms that can occur in the proof are the $12$ terms with one occurrence of each of $x$, $y$, and $z$. We can partition the set of these terms as $T\_x\cup T\_y\cup T\_z$, where $T\_x=\{x+(y+z),x+(z+y),(y+z)+x,(z+y)+x\}$ consists of the terms whose “outermost variable” is $x$, and similarly for $T\_y$ and $T\_z$. The $4$ terms in $T\_x$ are equal modulo commutativity, and likewise for $T\_y$ and $T\_z$.


Now, since $x+(y+z)\in T\_x$ and $(x+y)+z\in T\_z$, an $S$-proof $t\_0,\dots,t\_n$ of $x+(y+z)=(x+y)+z$ must contain terms $t\_i,t\_{i+1}$ that belong to different $T\_{\dots}$ sets. By renaming variables if necessary, we may assume that $t\_i\in T\_x$ and $t\_{i+1}\in T\_z$. Again, the equation $t\_i=t\_{i+1}$ is an instance of an equation $e\in S$, but it is not an instance of any strictly shorter equation valid in $\ac$ (because $t\_i$ and $t\_{i+1}$ have no common subterms other than variables), hence $e$ is $t\_i=t\_{i+1}$ itself up to renaming of variables.


