Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.29137 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914435725000704 |
|---|---|
| author | Ramani, Mahesh Kumar, Shlok |
| author_facet | Ramani, Mahesh Kumar, Shlok |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_29137 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | An Optimal 14-Symbol Hybrid Basis for BCH-Algebras Ramani, Mahesh Kumar, Shlok Logic Logic in Computer Science 06F35, 03G25 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. |
| title | An Optimal 14-Symbol Hybrid Basis for BCH-Algebras |
| topic | Logic Logic in Computer Science 06F35, 03G25 |
| url | https://arxiv.org/abs/2603.29137 |