A ring is an algebraic structure defined by a long-standing set of seven axioms. Given that it is often desirable to find the smallest possible set of axioms for different algebraic theories, this project aims to find the smallest possible axiomatic system for the theory of rings through the computational power of Wolfram Language. It was determined by A. Tarski that ring theory may be reduced to a single axiom. A candidate for this axiom has been found, establishing an upper bound for the maximum equational length. A lower bound has also been found through brute force, though future work includes strengthening this lower bound.

Introduction

History and Purpose of the Project

Fermat’s Last Theorem, conjectured in the 1600s, famously remained unproven until Andrew Wiles completed a proof of the theorem in 1995. However, during the span of the hundreds of years prior to this proof’s finalization, it became apparent that there was a need to generalize integer arithmetic. In the 1890s, Richard Dedekind and David Hilbert defined the concept of rings, modules, and ideals in their respective
research
in an attempt to do so
(1)
.
In 1921, Emmy Noether defined a rigid set of axioms for rings in her publication “Idealtheorie in
Ringbereichen,"
(2)
​
and these axioms, besides the axiom of commutative multiplication, have been accepted ever
since.
​​ Inspired by the study of single-axiom generalizations of group theory and Boolean algebra, notably studied by William McCune, Alfred Tarski, Graham Higman, Bernhard Hermann Neumann, and Stephen Wolfram, the purpose of this project is to similarly minimize the standard axioms for ring theory by utilizing the computational functionality of Wolfram Language.

Notations and Definitions

An axiom is defined as a statement that is accepted as true without proof, from which other statements are logically derived. Let  be a set. A binary operation is a function ⊙ :  ×  ⟶  such that (, ) ⊙(, ). ⊙(, ) is most commonly denoted  ⊙ . A ring is a set ℛ equipped with two binary operations, ⊕ : ℛ × ℛ ⟶ ℛ and ⊗ : ℛ × ℛ ⟶ ℛ such that the following axioms hold:
In[3]:=
AxiomaticTheory[{"RingAxioms",<|"Identity"->e|>}];​​ringAxiomsDataset=AxiomaticTheory[{"RingAxioms",<|"Identity"->e|>},"Dataset"]["AxiomsAssociation"]
Out[4]=
These axioms were produced by the AxiomaticTheory function. Note that in in some texts, these axioms are the axioms for “Rngs,” or rings lacking unity. For this project, we call rings the algebraic structure satisfying the axioms above, and rings having a multiplicative identity element “rings with unity” or “rings with identity.”
For the sake of computational simplicity, we denote variableNameNQ as the same set of axioms as variableName, minus the quantifier(s) and the formal variables:
In[35]:=
ringAxiomsNQ={a⊕(b⊕c)(a⊕b)⊕c,a⊕bb⊕a,a⊕0a,a⊕
a
0,a⊗(b⊕c)a⊗b⊕a⊗c,a⊗(b⊗c)(a⊗b)⊗c,(a⊕b)⊗ca⊗c⊕b⊗c};
In the previous axioms, “e” and “0” denote the additive identity element of ℛ, while “
a.
” and “
a
” denote the additive inverse of a. ∈ ℛ and a ∈ ℛ respectively. For the duration of this notebook, we will be referring to the size of an axiomatic equation as an ordered pair (ℓ,), where ℓ denotes the “length” of the equation and  denotes the number of variables it contains. For the purposes of this project, the additive identity element will be considered a variable. The length of an equation is defined by the number of occurrences of variables and operations. (Note: This includes “=” and OverBar but does not include parentheses or quantifiers such as “
∀
{x,y,z}
.”)​ This notation is borrowed from William McCune in his various papers on single axiom systems for group theory. Let Λ denote the set of variables used in an axiomatic system. We will define the total length of an axiomatic system as the ordered pair containing the componentwise sum of the lengths of axioms and the total number of variables used in the axiomatic system. That is, the total length of an axiomatic system is
(
ℓ
k
,

max
), where
ℓ
k
=
∑
i=0
ℓ
i
and

max
= |Λ|
.

The Standard Ring Axioms

For the purposes of convenience, to determine the size of an axiomatic system, we may consider a tree whose vertices are defined by the symbols in an axiomatic equation. The order of the tree is conveniently equal to the length of its corresponding axiomatic equation.
The following code serves to construct graphical representations of the ring axioms, determine their orders and corresponding axiom lengths, then find the total length of the standard set of ring axioms:
In[210]:=
Map[ExpressionTree[#,"HeadTrees",HeadsFalse]&,ringAxiomsNQ]​​ringAxiomsNQLength=Total[TreeSize/@ExpressionTree/@ringAxiomsNQ];​​Style[" = Total Length "ringAxiomsNQLength,FontSize20]
Out[210]=
Out[212]=
66 = Total Length
Since |{a, b, c, 0}| = 4, we can see that the size of the standard system of axioms for ring theory has size (66,4). Visually, we may consider the first degree entailment cones of these axiomatic systems to get a general sense of how complicated and reduced the axiomatic system in question is. For scope, the first degree entailment cones for various standardized forms of ring theory are displayed below. This idea and its implementation is inspired by Stephen Wolfram’s “The Physicalization of Metamathematics and Its Implications for the Foundations of
Mathematics."
(5)
​
Below are the radial entailment cones of ring theory, commutative ring theory, and commutative unital ring theory:
In[27]:=
Grid@(List/@Map[Labeled[
[◼]
TwoWayRuleTokenEventGraph
[
[◼]
AxiomaticTheoryTWP
[#[[1]]],1,"TokenLabeling"->False,GraphLayout"RadialEmbedding",ImageSizeMedium,VertexSize->Larger],Text[Style[#[[2]],Bold,GrayLevel[.5],Medium]]]&,{{"RingAxioms","Ring Theory"},{"CommutativeRingAxioms","Commutative Ring Theory"},{"CommutativeRingWithIdentityAxioms","Commutative Unital Ring Theory"}}])
Out[27]=

The Abelian Group Axioms

The Tarskian Axiom

The following sequence of inputs follows the method in McNulty’s paper to explicitly state a single axiom for rings with unity:

The Proof

“⟹”

“⟸”

Subsequent Theory

Establishing a Lower Bound

Concluding Remarks

Future Work

Acknowledgments

References

1
.
J. J. O’Connor, E. M. Robertson (2004), “The development of Ring Theory,” https://mathshistory.st-andrews.ac.uk/HistTopics/Ring_theory/
2
.
E. Noether (1921), “Idealtheorie in Ringbereichen,” Mathematische Annalen. https://doi.org/10.1007/BF01464225
3
.
M. F. Atiyah and I. G. MacDonald (1969), Introduction to Commutative Algebra. Addison-Wesley.
4
.
W. McCune (1993), “Single axioms for groups and Abelian groups with various operations,” J. Automated Reasoning. https://link.springer.com/article/10.1007/BF0088186
5
.
S. Wolfram (2022), “The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics,” Wolfram Media, Inc. https://www.wolframscience.com/metamathematics/axiom-systems-of-present-day-mathematics/
6
.
G. McNulty (2004), “Minimum Bases for Equational Theories of
Groups and Rings, the Work of Alfred Tarski and Thomas C. Green,” Annals of Pure and Applied Logic. https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=7a4ae268f89b83ec915ea49d6befc1ec0e135e98
7
.
W. McCune, M Kinyon (2004), “Yet Another Paper on Group Theory Single Axioms,” https://www.cs.unm.edu/~mccune/projects/gtsax/#:~:text=First%20posted%20in%20June%202004%2C%20updated%20several%20times%20since.&text=This%20work%20(in%20progress)%20is,in%20terms%20of%20%7Bdivision%7D.
8
.
G. GrSatzer, R. Padmanabhan (1978),” Symmetric difference in abelian groups,” Paci/c J. Math. https://www.researchgate.net/publication/38343412_Symmetric_difference_in_abelian_groups
9
.
A. Tarski (1938), “Ein Beitrag zur Axiomatik der Abelschen Gruppen,” Fund. Math. 30 https://www.ams.org/books/pspum/025/pspum025-endmatter.pdf

Cite This Notebook

“[WSS24] Finding Minimal Axioms for Ring Theory”
by Tate Allen
​https://community.wolfram.com/groups/-/m/t/3209590