Essays, Posts & Presentations

Finding Minimal Axioms for Ring Theory

Tate Allen

Author

Tate Allen

Title

Finding Minimal Axioms for Ring Theory

Description

This is a Wolfram Summer School notebook that explores finding the smallest possible systems of Axioms for Ring Theory

Finding Minimal Axioms for Ring Theory

TATE ALLEN

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. Tarksi that ring theory may be reduced to a single axiom. A notable candidate for this axiom has been found, but remains unverified. Future work includes verifying the single-axiom system for rings through proof and establishing upper and lower bounds on the lengths.

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, and Bernhard Hermann Neumann, 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[69]:=

AxiomaticTheory[{"RingAxioms",<|"Identity"->e|>}];ringAxiomsDataset=AxiomaticTheory[{"RingAxioms",<|"Identity"->e|>},"Dataset"]["AxiomsAssociation"]

Out[70]=

AdditionAssociativity	∀ {a.,b.,c.} a.⊕(b.⊕c.)(a.⊕b.)⊕c.
AdditionCommutativity	∀ {a.,b.} a.⊕b.b.⊕a.
AdditionIdentity	∀ a. a.⊕ea.
AdditionInverse	∀ a. a.⊕ a. e
LeftDistributivity	∀ {a.,b.,c.} a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.
MultiplicationAssociativity	∀ {a.,b.,c.} a.⊗(b.⊗c.)(a.⊗b.)⊗c.
RightDistributivity	∀ {a.,b.,c.} (a.⊕b.)⊗c.a.⊗c.⊕b.⊗c.

These axioms were roduced 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[131]:=

ringAxiomsNQ={a⊕(b⊕c)(a⊕b)⊕c,a⊕bb⊕a,a⊕0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 “

” and “

” 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 “=” 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

(

ℓ



max

), where

ℓ

∑

i=0

ℓ

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)

Entailment cones of Ring Theory, Commutative Ring Theory, and Commutative Unital Ring Theory:

In[525]:=

ringEntailmentCone=Grid@(List/@Map[Labeled[

[◼]	TwoWayRuleTokenEventGraph

[

[◼]	AxiomaticTheoryTWP

[#[[1]]],1,"TokenLabeling"->False,GraphLayout"RadialEmbedding",ImageSizeLarge,VertexSize->Larger],Text[Style[#[[2]],Bold,GrayLevel[.5],Medium]]]&,{{"RingAxioms","Ring Theory"},{"CommutativeRingAxioms","Commutative Ring Theory"},{"CommutativeRingWithIdentityAxioms","Commutative Unital Ring Theory"}}])

Out[525]=

Ring Theory

Commutative Ring Theory

Commutative Unital Ring Theory

The Abelian Group Axioms

In M. F. Atiyah and I. G. MacDonald’s “Introduction to Commutative

Algebra,"

(3)

rings are described by two axioms: 1. ℛ is an abelian group with respect to ⊕. 2. ⊗ is associative and distributive over ⊕.Of course, these “axioms” are not axiomatic at all, but they do serve to motivate the first steps in minimizing the standard set of axioms. William McCune reduced the axioms for abelian groups into a single axiom of size

(4)

(12,3)

, given by:

In[242]:=

AxiomaticTheory["AbelianMcCuneAxioms","Dataset"]["AxiomsAssociation"]multiplicativeAbelianMccuneAxiomsNQ=((a⊗b)⊗c)⊗

a⊗c

b;

Out[242]=

AbelianMcCuneAxiom

∀

{a.,b.,c.}

((a.⊗b.)⊗c.)⊗

a.⊗c.

b.

As before, we may construct an expression tree to verify the length of McCune’s axiom for abelian groups:

In[244]:=

ExpressionTree@multiplicativeAbelianMccuneAxiomsNQmultiplicativeAbelianMccuneAxiomsNQLength=ExpressionTree@multiplicativeAbelianMccuneAxiomsNQ//TreeSize;Style[" = Total Length "multiplicativeAbelianMccuneAxiomsNQLength,FontSize20]

Out[244]=

Out[246]=

12 = Total Length

As ℛ is an abelian group with respect to ⊕, the first 4 ring axioms may be replaced with McCune’s single abelian group axiom, written additively, forming a reduced axiom system:

In[1330]:=

abelianMccuneAxioms=AxiomaticTheory[{"AbelianMcCuneAxioms",<|Identity->e,"Multiplication"->CirclePlus|>}];abelianMccuneAxiomsDataset=(AxiomaticTheory[{"AbelianMcCuneAxioms",<|"Identity"->e,"Multiplication"->CirclePlus|>},"Dataset"]["AxiomsAssociation"]);reducedAxioms1=Join[abelianMccuneAxioms,Take[ringAxioms,-3]];reducedAxioms1NQ={((a⊕b)⊕c)⊕

a⊕c

b,a⊗(b⊕c)a⊗b⊕a⊗c,a⊗(b⊗c)(a⊗b)⊗c,(a⊕b)⊗ca⊗c⊕b⊗c};reducedAxioms1Dataset=Join[abelianMccuneAxiomsDataset,Take[AxiomaticTheory[{"RingAxioms",<|"Identity"->e|>},"Dataset"]["AxiomsAssociation"],-3]]

Out[1334]=

AbelianMcCuneAxiom	∀ {a.,b.,c.} ((a.⊕b.)⊕c.)⊕ a.⊕c. b.
LeftDistributivity	∀ {a.,b.,c.} a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.
MultiplicationAssociativity	∀ {a.,b.,c.} a.⊗(b.⊗c.)(a.⊗b.)⊗c.
RightDistributivity	∀ {a.,b.,c.} (a.⊕b.)⊗c.a.⊗c.⊕b.⊗c.

This should work in theory, but it may be checked by utilizing the FindFiniteModels resource function from the Wolfram Function Repository.

The following finite models and their corresponding operation tables represent every possible definition of the two operations that satisfy the set of standard ring axioms, having a cardinality of 2 and 3 respectively:

In[238]:=

ringSize2=ResourceFunction["FindFiniteModels"][AxiomaticTheory["RingAxioms"]/.OverTilde[x_]:>x[]]

Out[238]=

{0,6,0,1}00,CirclePlus{{0,1},{1,0}},CircleTimes{{0,0},{0,0}},OverBar{0,1},{0,6,1,1}00,CirclePlus{{0,1},{1,0}},CircleTimes{{0,0},{0,1}},OverBar{0,1},{1,9,7,1}01,CirclePlus{{1,0},{0,1}},CircleTimes{{0,1},{1,1}},OverBar{0,1},{1,9,15,1}01,CirclePlus{{1,0},{0,1}},CircleTimes{{1,1},{1,1}},OverBar{0,1}

Out[747]=



\[CirclePlus[CirclePlus]	0	1
0	0	1
1	1	0

\[CirclePlus[CirclePlus]	0	1
0	0	1
1	1	0

\[CirclePlus[CirclePlus]	0	1
0	1	0
1	0	1

\[CirclePlus[CirclePlus]	0	1
0	1	0
1	0	1



Out[760]=



⊗	0	1
0	0	0
1	0	0

⊗	0	1
0	0	0
1	0	1

⊗	0	1
0	0	1
1	1	1

⊗	0	1
0	1	1
1	1	1



In[354]:=

ringSize3=ResourceFunction["FindFiniteModels"][AxiomaticTheory["RingAxioms"]/.OverTilde[x_]:>x[],3]

Out[354]=

{0,4069,0,7}00,CirclePlus{{0,1,2},{1,2,0},{2,0,1}},CircleTimes{{0,0,0},{0,0,0},{0,0,0}},OverBar{0,2,1},{0,4069,142,7}00,CirclePlus{{0,1,2},{1,2,0},{2,0,1}},CircleTimes{{0,0,0},{0,1,2},{0,2,1}},OverBar{0,2,1},{0,4069,194,7}00,CirclePlus{{0,1,2},{1,2,0},{2,0,1}},CircleTimes{{0,0,0},{0,2,1},{0,1,2}},OverBar{0,2,1},{1,14001,4017,21}01,CirclePlus{{2,0,1},{0,1,2},{1,2,0}},CircleTimes{{0,1,2},{1,1,1},{2,1,0}},OverBar{2,1,0},{1,14001,9841,21}01,CirclePlus{{2,0,1},{0,1,2},{1,2,0}},CircleTimes{{1,1,1},{1,1,1},{1,1,1}},OverBar{2,1,0},{1,14001,15665,21}01,CirclePlus{{2,0,1},{0,1,2},{1,2,0}},CircleTimes{{2,1,0},{1,1,1},{0,1,2}},OverBar{2,1,0},{2,11453,3968,11}02,CirclePlus{{1,2,0},{2,0,1},{0,1,2}},CircleTimes{{0,1,2},{1,0,2},{2,2,2}},OverBar{1,0,2},{2,11453,8180,11}02,CirclePlus{{1,2,0},{2,0,1},{0,1,2}},CircleTimes{{1,0,2},{0,1,2},{2,2,2}},OverBar{1,0,2},{2,11453,19682,11}02,CirclePlus{{1,2,0},{2,0,1},{0,1,2}},CircleTimes{{2,2,2},{2,2,2},{2,2,2}},OverBar{1,0,2}

Out[748]=



⊕	0	1	2
0	0	1	2
1	1	2	0
2	2	0	1

⊕	0	1	2
0	0	1	2
1	1	2	0
2	2	0	1

⊕	0	1	2
0	0	1	2
1	1	2	0
2	2	0	1

⊕	0	1	2
0	2	0	1
1	0	1	2
2	1	2	0

⊕	0	1	2
0	2	0	1
1	0	1	2
2	1	2	0

⊕	0	1	2
0	2	0	1
1	0	1	2
2	1	2	0

⊕	0	1	2
0	1	2	0
1	2	0	1
2	0	1	2

⊕	0	1	2
0	1	2	0
1	2	0	1
2	0	1	2

⊕	0	1	2
0	1	2	0
1	2	0	1
2	0	1	2



Out[749]=



⊗	1	2
0	0	0
1	0	0
2	0	0

⊗	1	2
0	0	0
1	1	2
2	2	1

⊗	1	2
0	0	0
1	2	1
2	1	2

⊗	0	1	2
0	0	1	2
1	1	1	1
2	2	1	0

⊗	0	1	2
0	1	1	1
1	1	1	1
2	1	1	1

⊗	0	1	2
0	2	1	0
1	1	1	1
2	0	1	2

⊗	0	1	2
0	0	1	2
1	1	0	2
2	2	2	2

⊗	0	1	2
0	1	0	2
1	0	1	2
2	2	2	2

⊗	0	1	2
0	2	2	2
1	2	2	2
2	2	2	2



The next four outputs are the models of rings of cardinality 2 and 3 and their respective ring operation tables generated by the reduced axioms using McCune’s single axiom group theory system.

In[346]:=

ResourceFunction["FindFiniteModels"][Join[abelianMccuneAxioms,Take[ringAxioms,-3]]]

Out[346]=

{6,0,1}CirclePlus{{0,1},{1,0}},CircleTimes{{0,0},{0,0}},OverBar{0,1},{6,1,1}CirclePlus{{0,1},{1,0}},CircleTimes{{0,0},{0,1}},OverBar{0,1},{9,7,1}CirclePlus{{1,0},{0,1}},CircleTimes{{0,1},{1,1}},OverBar{0,1},{9,15,1}CirclePlus{{1,0},{0,1}},CircleTimes{{1,1},{1,1}},OverBar{0,1}

Out[585]=



\[CirclePlus[CirclePlus]	0	1
0	0	1
1	1	0

\[CirclePlus[CirclePlus]	0	1
0	0	1
1	1	0

\[CirclePlus[CirclePlus]	0	1
0	1	0
1	0	1

\[CirclePlus[CirclePlus]	0	1
0	1	0
1	0	1



Out[761]=



⊗	0	1
0	0	0
1	0	0

⊗	0	1
0	0	0
1	0	1

⊗	0	1
0	0	1
1	1	1

⊗	0	1
0	1	1
1	1	1



In[54]:=

ResourceFunction["FindFiniteModels"][Join[abelianMccuneAxioms,Take[ringAxioms,-3]],3]

Out[54]=

{4069,0,7}CirclePlus{{0,1,2},{1,2,0},{2,0,1}},CircleTimes{{0,0,0},{0,0,0},{0,0,0}},OverBar{0,2,1},{4069,142,7}CirclePlus{{0,1,2},{1,2,0},{2,0,1}},CircleTimes{{0,0,0},{0,1,2},{0,2,1}},OverBar{0,2,1},{4069,194,7}CirclePlus{{0,1,2},{1,2,0},{2,0,1}},CircleTimes{{0,0,0},{0,2,1},{0,1,2}},OverBar{0,2,1},{11453,3968,11}CirclePlus{{1,2,0},{2,0,1},{0,1,2}},CircleTimes{{0,1,2},{1,0,2},{2,2,2}},OverBar{1,0,2},{11453,8180,11}CirclePlus{{1,2,0},{2,0,1},{0,1,2}},CircleTimes{{1,0,2},{0,1,2},{2,2,2}},OverBar{1,0,2},{11453,19682,11}CirclePlus{{1,2,0},{2,0,1},{0,1,2}},CircleTimes{{2,2,2},{2,2,2},{2,2,2}},OverBar{1,0,2},{14001,4017,21}CirclePlus{{2,0,1},{0,1,2},{1,2,0}},CircleTimes{{0,1,2},{1,1,1},{2,1,0}},OverBar{2,1,0},{14001,9841,21}CirclePlus{{2,0,1},{0,1,2},{1,2,0}},CircleTimes{{1,1,1},{1,1,1},{1,1,1}},OverBar{2,1,0},{14001,15665,21}CirclePlus{{2,0,1},{0,1,2},{1,2,0}},CircleTimes{{2,1,0},{1,1,1},{0,1,2}},OverBar{2,1,0}

Out[586]=



\[CirclePlus[CirclePlus]	0	1	2
0	0	1	2
1	1	2	0
2	2	0	1

\[CirclePlus[CirclePlus]	0	1	2
0	0	1	2
1	1	2	0
2	2	0	1

\[CirclePlus[CirclePlus]	0	1	2
0	0	1	2
1	1	2	0
2	2	0	1

\[CirclePlus[CirclePlus]	0	1	2
0	2	0	1
1	0	1	2
2	1	2	0

\[CirclePlus[CirclePlus]	0	1	2
0	2	0	1
1	0	1	2
2	1	2	0

\[CirclePlus[CirclePlus]	0	1	2
0	2	0	1
1	0	1	2
2	1	2	0

\[CirclePlus[CirclePlus]	0	1	2
0	1	2	0
1	2	0	1
2	0	1	2

\[CirclePlus[CirclePlus]	0	1	2
0	1	2	0
1	2	0	1
2	0	1	2

\[CirclePlus[CirclePlus]	0	1	2
0	1	2	0
1	2	0	1
2	0	1	2



Out[750]=



⊗	1	2
0	0	0
1	0	0
2	0	0

⊗	1	2
0	0	0
1	1	2
2	2	1

⊗	1	2
0	0	0
1	2	1
2	1	2

⊗	0	1	2
0	0	1	2
1	1	1	1
2	2	1	0

⊗	0	1	2
0	1	1	1
1	1	1	1
2	1	1	1

⊗	0	1	2
0	2	1	0
1	1	1	1
2	0	1	2

⊗	0	1	2
0	0	1	2
1	1	0	2
2	2	2	2

⊗	0	1	2
0	1	0	2
1	0	1	2
2	2	2	2

⊗	0	1	2
0	2	2	2
1	2	2	2
2	2	2	2



The next outputs are the result of taking the same set of reduced axioms as before and removing the quantifiers and formal variables.

In[347]:=

ResourceFunction["FindFiniteModels"][Join[abelianMccuneAxioms,Take[ringAxiomsNQ,-3]]]

Out[347]=

In[55]:=

ResourceFunction["FindFiniteModels"][Join[abelianMccuneAxioms,Take[ringAxiomsNQ,-3]],3]

Notice that the models generated by the reduced set of axioms are the same as the models generated by the reduced set of axioms without quantifiers or formal variables, and all three of them share the same set of possible operation tables. For the sake of simplicity, we will only be considering the models generated by axiom systems without quantifiers from now on.

Now, with a slightly reduced axiomatic system, we may check its length to visualize how much smaller this system is:

In[817]:=

ExpressionTree/@reducedAxioms1NQreducedAxioms1NQLength=Total[TreeSize/@ExpressionTree/@reducedAxioms1NQ];Style[" = Total Length "reducedAxioms1NQLength,FontSize20]

Thus this way of expressing the theory of rings is smaller than the standard set of axioms, but it is still possible to make a smaller system.

The Tarskian Axiom

Alfred Tarski and his doctoral students did large amounts of work in the field of finitely axiomatizable equational theories. In one paper covering his work, it was proven that there exists a single-equation axiomatic system that encapsulates the theory of rings having two imposed binary

operations

(6)

First, however, we will suppose that ℛ is a ring with identity, as the process of determining its single axiom is much simpler. In the formulation of the Tarskian axiom below, we denote a ⊕ (-b) as a ⊖ b. Additionally, it is important to note that the statementy = ((z ⊖ z) ⊖ (x ⊖ y)) ⊖ ((w ⊖ w) ⊖ x) must be true. This is true in all rings and may be easily derived using the standard ring axioms, so it poses no issue here.

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

In[1171]:=

p0=(x.⊕y.)⊕z.;q0=x.⊕(y.⊕z.);p1=x.⊕y.;q1=y.⊕x.;p2=x.⊕



;q2=x.;p3=x.⊕

;q3=



;p4=(x.⊗y.)⊗z.;q4=x.⊗(y.⊗z.);p5=x.⊗



;q5=x.;p6=



⊗x.;q6=x.;p7=x.⊗(y.⊕z.);q7=(x.⊗y.)⊕(x.⊗z.);p8=(y.⊕z.)⊗x.;q8=(y.⊗x.)⊕(z.⊗x.);u0=p0.

;r0=q0.

;u1=p1.

;r1=q1.

;u2=p2.

;r2=q2.

;u3=p3.

;r3=q3.

;u4=p4.

;r4=q4.

;u5=p5.

;r5=q5.

;u6=p6.

;r6=q6.

;u7=p7.

;r7=q7.

;u8=p8.

;r8=q8.

;u9=x.⊗



;r9=x.;u10=((z.⊖z.)⊖(x.⊖y.))⊖((w.⊖w.)⊖x.);r10=y.;

=p0.(

⊖

);

=q0.(

⊖

);

=p1.(

⊖

);

=q1.(

⊖

);

=p2.(

⊖

);

=q2.(

⊖

);

=p3.(

⊖

);

=q3.(

⊖

);

=p4.(

⊖

);

=q4.(

⊖

);

=p5.(

⊖

);

=q5.(

⊖

);

=p6.(

⊖

);

=q6.(

⊖

);

=p7.(

⊖

);

=q7.(

⊖

);

=p8.(

⊖

);

=q8.(

⊖

);

=x.⊗



;

=x.;

u10

=((z.⊖z.)⊖(x.⊖y.))⊖((w.⊖w.)⊖x.);

r10

=y.;p=(x.⊗



)⊖x.;q=(y.⊗(w.⊖w.))⊖(z.⊗(w.⊖w.));s=p⊖((u0⊖(u1⊖(u2⊖(u3⊖(u4⊖(u5⊖(u6⊖(u7⊖(u8⊖(u9⊖u10))))))))))⊖(

⊖(

⊖

u10

)))))))))));t=q⊖((r0⊖(r1⊖(r2⊖(r3⊖(r4⊖(r5⊖(r6⊖(r7⊖(r8⊖(r9⊖r10))))))))))⊖(

⊖(

⊖

r10

)))))))))));

=((z.⊖z.)⊖(x.⊖y.))⊖((s⊖t)⊖x.)y./.DotCircleTimes

Out[1237]=

z.⊖z.⊖(x.⊖y.)⊖x.⊗



⊖x.⊖((x.⊕y.)⊕z.)⊗

⊖(x.⊕y.)⊗

⊖(x.⊕



)⊗

⊖(x.⊕

)⊗

⊖((x.⊗y.)⊗z.)⊗

⊖(x.⊗



)⊗

⊖(



⊗x.)⊗

⊖(x.⊗(y.⊕z.))⊗

⊖((y.⊕z.)⊗x.)⊗

⊖x.⊗



⊖(z.⊖z.⊖(x.⊖y.)⊖(w.⊖w.⊖x.))⊖((x.⊕y.)⊕z.)⊗(

⊖

)⊖(x.⊕y.)⊗(

⊖

)⊖(x.⊕



)⊗(

⊖

)⊖(x.⊕

)⊗(

⊖

)⊖((x.⊗y.)⊗z.)⊗(

⊖

)⊖(x.⊗



)⊗(

⊖

)⊖(



⊗x.)⊗(

⊖

)⊖(x.⊗(y.⊕z.))⊗(

⊖

)⊖((y.⊕z.)⊗x.)⊗(

⊖

)⊖x.⊗



⊖(z.⊖z.⊖(x.⊖y.)⊖(w.⊖w.⊖x.))⊖y.⊗(w.⊖w.)⊖z.⊗(w.⊖w.)⊖(x.⊕(y.⊕z.))⊗

⊖(y.⊕x.)⊗

⊖x.⊗

⊖



⊗

⊖((x.⊗(y.⊗z.))⊗

⊖(x.⊗

⊖((x.⊗y.⊕x.⊗z.)⊗

⊖((y.⊗x.⊕z.⊗x.)⊗

⊖(x.⊖y.))))))⊖(x.⊕(y.⊕z.))⊗(

⊖

)⊖(y.⊕x.)⊗(

⊖

)⊖x.⊗(

⊖

)⊖



⊗(

⊖

)⊖((x.⊗(y.⊗z.))⊗(

⊖

)⊖(x.⊗(

⊖

)⊖(x.⊗(

⊖

)⊖((x.⊗y.⊕x.⊗z.)⊗(

⊖

)⊖((y.⊗x.⊕z.⊗x.)⊗(

⊖

)⊖(x.⊖y.))))))⊖x.y.

The output is presumably a single axiom for unital ring theory. This axiom, while notably longer than the standard axioms for unital ring theory, lines up with both McCune’s findings that every single-axiom satisfies that one side of the equation is a single

(7)

variable

and Tarski’s research into equational theories of groups and rings. However, that alone is not enough to verify the validity of this axiom. Assuming it is true, though, we proceed to find its length using the same method as before.

The tree representing this single axiom is displayed below. In an attempt to make the image easier on the eyes, labels have been removed:

In[1305]:=

deltaTree=ExpressionTree[

,ImageSizeFull,TreeElementLabel->All->None]deltaTreeLength=ExpressionTree@

//TreeSize;Style[" = Total Length "deltaTreeLength,FontSize20]

Out[1305]=

Out[1307]=

470 = Total Length

It is unlikely that this axiom is the smallest single-axiom system for unital rings that exists, but at the very least, this axiom establishes an upper bound for the length of a single-axiom system for rings having a multiplicative identity.

Concluding Remarks

Indeed, it is possible to reduce the set of axioms for rings with identity to a single axiom having a length of at most 470. In theory, it is possible to do this for rings without identity as well, though the specific axiom that satisfies the equational theory of non-unital rings is still unknown. A convenient and short reduction of ring axioms was found by utilizing McCune’s abelian group axiom, though it far from minimal. While the enumeration of axioms to find finite models that matched the distributive and associative axioms was attempted, no results were found.

Future Work

Firstly, it is imperative that this single axiom be verified so that we may know with proof that it is indeed logically equivalent to the equational theory of unital rings. This may be done by hand or by utilizing FindEquationalProof. Additionally, this axiom only covers unital rings, which was not the intended path of the project. Thus future work will include finding and proving single axioms for rings without identity, as well as extending to commutative rings and commutative rings with unity. On a different note, this projects does not take full advantage of the visual charm of entailment cones, so generating new entailment cones to assist the reader visually is another future goal of this project. Lastly, the axiom found, if proven, only serves as an upper bound to the minimal length of the axiomatic theory for rings. A key detail that is missing is concrete proof of minimality. Utilizing enumerative techniques and the FindFiniteModels function to eliminate all single axiom candidates having a certain length may serve as a way to establish a lower bound on the minimal length of a single-axiom system for rings.

Acknowledgments

I would like to express my gratitude to my mentors Eric Parfitt and Daniel Sanchez for their constant support. Without their contributions to both ideas and programmatic execution, this project would not have been possible. I would also like to thank Sotiris Michos for putting incredible amounts of work into this project, even without obligation. You truly turned the tides of the project and were pivotal to its success. My thanks also extend to the rest of the Wolfram Staff for the amazing lectures, their guidance, and for providing this wonderful opportunity to their students.

References

J. J. O’Connor, E. M. Robertson (2004), “The development of Ring Theory,” https://mathshistory.st-andrews.ac.uk/HistTopics/Ring_theory/

E. Noether (1921), “Idealtheorie in Ringbereichen,” Mathematische Annalen. https://doi.org/10.1007/BF01464225

M. F. Atiyah and I. G. MacDonald (1969), Introduction to Commutative Algebra. Addison-Wesley.

W. McCune (1993), “Single axioms for groups and Abelian groups with various operations,” J. Automated Reasoning. https://link.springer.com/article/10.1007/BF0088186

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/

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

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.

Cite This Notebook

“[WSS24] Finding Minimal Axioms for Ring Theory”
by Tate Allen
Community Post Link

Cite this as: Tate Allen, "Finding Minimal Axioms for Ring Theory" from the Notebook Archive (2024), https://notebookarchive.org/2024-07-4n28ynr