An Optimal 14-Symbol Hybrid Basis for BCH-Algebras

TL;DR

This paper introduces a minimal two-axiom basis for BCH-algebras, replacing the standard axioms with a single 14-symbol equation verified through automated theorem proving.

Contribution

It provides the first proof of strict minimality for a 14-symbol basis in BCH-algebras using exhaustive machine-assisted methods.

Findings

The 14-symbol equation fully replaces two standard axioms.

No shorter equation (12 or fewer symbols) can define BCH-algebras with the quasi-identity.

The minimality of the basis is rigorously proven and verified.

Abstract

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.