An Optimal 14-Symbol Hybrid Basis for BCH-Algebras
This work provides a foundational simplification for mathematicians and logicians working on algebraic structures, though it is incremental in refining axiomatic systems.
The authors tackled the problem of finding a minimal axiomatic basis for BCH-algebras by replacing two standard equations with a single 14-symbol equation, proving its optimality through automated theorem proving and exhaustive search, with no prior proof of this result known.
We present an optimally minimal two-axiom basis for BCH-algebras. The standard presentation of a BCH-algebra relies on three axioms: two equations and one quasi-identity. Using automated theorem proving, we prove that the two standard equations can be entirely replaced by a 14-symbol equation, ((xy)z)((x(z0))y) = 0, while retaining the standard quasi-identity. We then provide a rigorous proof of strict minimality for this new equational companion. By employing an exhaustive, machine-assisted search space generation coupled with finite countermodel building, we demonstrate that no equation of 12 or fewer symbols can define the class of BCH-algebras when paired with the standard quasi-identity. Our literature searches have revealed no prior proof of this result, to the extent of our knowledge. All equivalence derivations were verified using Prover9, and all minimality countermodels were generated using Mace4.