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. 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?
1 Answer
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.
