In[]:=
AxiomaticTheory[]
Out[]=
{AbelianGroupAxioms,AbelianHigmanNeumannAxioms,AbelianMcCuneAxioms,BooleanAxioms,GroupAxioms,HigmanNeumannAxioms,HillmanAxioms,HuntingtonAxioms,McCuneAxioms,MeredithAxioms,MonoidAxioms,RingAxioms,RobbinsAxioms,SemigroupAxioms,ShefferAxioms,WolframAlternateAxioms,WolframAxioms,WolframCommutativeAxioms}

This should give all info we know about the system:

In[]:=
AxiomaticTheory["WolframAxioms","Dataset"]
AxiomaticTheory
:Dataset is not a known property for AxiomaticTheory. Use AxiomaticTheory​[Properties] for a list of properties.
Out[]=
AxiomaticTheory[WolframAxioms,Dataset]
In[]:=
AxiomaticTheory["WolframAxioms","NotableTheorems"]
Out[]=
ImpliesShefferAxioms
∀
a.
(a.·a.)·(a.·a.)a.,
∀
{a.,b.}
a.·(b.·(b.·b.))a.·a.,
∀
{a.,b.,c.}
(a.·(b.·c.))·(a.·(b.·c.))((b.·b.)·a.)·((c.·c.)·a.),ImpliesHillmanAxioms
∀
{a.,b.}
(a.·a.)·(a.·b.)a.,
∀
{a.,b.}
a.·(a.·b.)a.·(b.·b.),
∀
{a.,b.,c.}
a.·(a.·(b.·c.))b.·(b.·(a.·c.)),ImpliesMeredithAxioms
∀
{a.,b.,c.}
a.·(b.·(a.·c.))((c.·b.)·b.)·a.,
∀
{a.,b.}
(a.·a.)·(b.·a.)a.,ImpliesWolframAlternateAxioms
∀
{a.,b.,c.}
(a.·((c.·a.)·a.))·(c.·(b.·a.))c.,ImpliesWolframCommutativeAxioms
∀
{a.,b.,c.}
(a.·b.)·(a.·(b.·c.))a.,
∀
{a.,b.}
a.·b.b.·a.,Commutativity
∀
{a.,b.}
a.·b.b.·a.,DoubleNegation
∀
a.
(a.·a.)·(a.·a.)a.,AndAssociativity
∀
{a.,b.,c.}
(a.·((b.·c.)·(b.·c.)))·(a.·((b.·c.)·(b.·c.)))(((a.·b.)·(a.·b.))·c.)·(((a.·b.)·(a.·b.))·c.),OrAssociativity
∀
{a.,b.,c.}
(a.·a.)·(((b.·b.)·(c.·c.))·((b.·b.)·(c.·c.)))(((a.·a.)·(b.·b.))·((a.·a.)·(b.·b.)))·(c.·c.)

Transfer NotableTheorems from BooleanAxioms

In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=

∀
{a.,b.}
a.⊗b.b.⊗a.,
∀
{a.,b.}
a.⊕b.b.⊕a.,
∀
{a.,b.}
a.⊗b.⊕
b.
a.,
∀
{a.,b.}
a.⊕b.⊗
b.
a.,
∀
{a.,b.,c.}
a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,
∀
{a.,b.,c.}
a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
In[]:=
AxiomaticTheory["BooleanAxioms","NotableTheorems"]
Out[]=
ImpliesHuntingtonAxioms
∀
{a.,b.}
a.⊕b.b.⊕a.,
∀
{a.,b.,c.}
a.⊕(b.⊕c.)(a.⊕b.)⊕c.,
∀
{a.,b.}
a.
⊕b.
⊕
a.
⊕
b.
a.,ImpliesRobbinsAxioms
∀
{a.,b.}
a.⊕b.b.⊕a.,
∀
{a.,b.,c.}
a.⊕(b.⊕c.)(a.⊕b.)⊕c.,
∀
{a.,b.}
a.⊕b.
⊕
a.⊕
b.
a.,DoubleNegation
∀
a.
a.
a.,DeMorgan
∀
{a.,b.}
a.⊕b.

a.
⊗
b.
,
∀
{a.,b.}
a.⊗b.

a.
⊕
b.

In[]:=
AxiomaticTheory["BooleanAxioms","Operators"]
Out[]=
AndCircleTimes,OrCirclePlus,NotOverBar
In[]:=
InputForm[%24]
Out[]//InputForm=
<|And -> CircleTimes, Or -> CirclePlus, Not -> OverBar|>

Presburger arithmetic

(from Documentation)
In[]:=
a⊖b
Out[]=
a⊖b
In[]:=
¬a
Out[]=
!a
In[]:=
CircleTimes[a,b]
Out[]=
a⊗b
In[]:=
Square[p]
Out[]=
p
In[]:=
AxiomaticTheory["BooleanAxioms","OperatorArities"]
Out[]=
{CircleTimes2,CirclePlus2,OverBar1}
In[]:=
<|"PresburgerArithmeticAxioms"<|"Operators"<|"Plus"CirclePlus,"Negation"Square|>,"OperatorArities"<|CirclePlus2,Square1|>,"Axioms"->
∀
a.
a.⊕0a.,
∀
a.
a.⊕a.0,
∀
{a.,b.,c.}
(a.⊕b.)⊕c.a.⊕(b.⊕c.)|>|>
Out[]=
PresburgerArithmeticAxiomsOperatorsPlusCirclePlus,NegationSquare,OperatorAritiesCirclePlus2,Square1,Axioms
∀
a.
a.⊕0a.,
∀
a.
a.⊕a.0,
∀
{a.,b.,c.}
(a.⊕b.)⊕c.a.⊕(b.⊕c.)
"Axioms"
"Operators"
"OperatorArities"
"NotableTheorems"
"EquivalentTheories"
"Subtheories"
"Supertheories"
In[]:=
{ForAll[x,plus[x,0]x],ForAll[x,plus[x,neg[x]]0],ForAll[{x,y,z},plus[plus[x,y],z]plus[x,plus[y,z]]]}/.{plusCirclePlus,negSquare,xa.,yb.,zc.}
Out[]=

∀
a.
a.⊕0a.,
∀
a.
a.⊕a.0,
∀
{a.,b.,c.}
(a.⊕b.)⊕c.a.⊕(b.⊕c.)

Should add Description

"Fragment of Presburger arithmetic"

Adding in axioms (AKA relations) for specific groups

In[]:=
AxiomaticTheory["GroupAxioms"]
Out[]=

∀
{a.,b.,c.}
a.⊗(b.⊗c.)(a.⊗b.)⊗c.,
∀
a.
a.⊗

1
a.,
∀
a.
a.⊗
a.


1

We should be able to get group relations from FiniteGroupData
In[]:=
AlternatingGroup[5]
Out[]=
AlternatingGroup[5]
In[]:=
FiniteGroupData["Quaternion","DefiningRelations"]
Out[]=
2∘3∘2∘
∘-1
3
3∘2∘3∘
∘-1
2
1
In[]:=
FiniteGroupData["Quaternion","DefiningRelations"]/.{2a.,3b.}
Out[]=
a.∘b.∘a.∘
∘-1
b.
b.∘a.∘b.∘
∘-1
a.
1
AxiomaticTheory[{"GroupAxioms","Quaternion"}]
In FiniteGroupData ... ? “AxiomaticRelations”

Logic puzzles

Conclude, following Lewis Carroll, that babies cannot manage crocodiles:
In[]:=
FindEquationalProof[Not[Exists[x,And[baby[x],manageCrocodile[x]]]],{ForAll[x,Implies[baby[x],Not[logical[x]]]],ForAll[x,Implies[manageCrocodile[x],Not[despised[x]]]],ForAll[x,Implies[Not[logical[x]],despised[x]]]}]

NKS book

{x[1]a.,x[2]b.,x[3]c.,x[4]d.}

Peano arithmetic

"PeanoArithmeticAxioms"
<|"Implies"DoubleRightArrow,"Equal"HumpEqual,"Unequal"NotHumpEqual,"Plus"CirclePlus,"Times"CircleTimes,"Successor"Square|>
{zero[]0}
In[]:=
peano={{unequal[zero[],s[x[1]]],""},{implies[equal[s[x[1]],s[x[2]]],equal[x[1],x[2]]],""},{equal[plus[x[1],zero[]],x[1]],""},{equal[plus[x[1],s[x[2]]],s[plus[x[1],x[2]]]],""},{equal[times[x[1],zero[]],zero[]],""},{equal[times[x[1],s[x[2]]],plus[times[x[1],x[2]],x[1]]],""},{implies[and[sub[α_,x[1],zero[]],forall[x[2],implies[sub[α_,x[1],x[2]],sub[α_,x[1],s[x[2]]]]]],insertboxes["",forall[x[2],sub[α_,x[1],x[2]]]]]/;FreeQ[α,x[2]],"[Mathematical Induction]"}};
In[]:=
First/@(peano/.{x[1]a.,x[2]b.,x[3]c.,x[4]d.}/.{zero[]0,equalHumpEqual,impliesDoubleRightArrow,unequalNotHumpEqual,plusCirclePlus,timesCircleTimes,sSquare})
Out[]=
{0a.,a.≏b.⇒a.≏b.,a.⊕0≏a.,a.⊕b.≏(a.⊕b.),a.⊗0≏0,a.⊗b.≏a.⊗b.⊕a.,and[sub[α_,a.,0],forall[b.,sub[α_,a.,b.]⇒sub[α_,a.,b.]]]⇒insertboxes[,forall[b.,sub[α_,a.,b.]]]/;FreeQ[α,b.]}
"Peano arithmetic with the induction axiom schema"

Robinson arithmetic

In[]:=
robinson={{unequal[zero[],s[x[1]]],""},{implies[equal[s[x[1]],s[x[2]]],equal[x[1],x[2]]],""},{equal[plus[x[1],zero[]],x[1]],""},{equal[plus[x[1],s[x[2]]],s[plus[x[1],x[2]]]],""},{equal[times[x[1],zero[]],zero[]],""},{equal[times[x[1],s[x[2]]],plus[times[x[1],x[2]],x[1]]],""},{implies[unequal[x[1],zero[]],exists[x[2],equal[x[1],s[x[2]]]]],""}};
In[]:=
First/@(robinson/.{x[1]a.,x[2]b.,x[3]c.,x[4]d.}/.{zero[]0,equalHumpEqual,impliesDoubleRightArrow,unequalNotHumpEqual,plusCirclePlus,timesCircleTimes,sSquare})
Out[]=
{0a.,a.≏b.⇒a.≏b.,a.⊕0≏a.,a.⊕b.≏(a.⊕b.),a.⊗0≏0,a.⊗b.≏a.⊗b.⊕a.,a.0⇒exists[b.,a.≏b.]}

Real algebra

Additional Elements

“Description”

“Reference”

“FormulationDate”

“AxiomNames”

Axiom Systems from the Web, etc.

https://en.wikipedia.org/wiki/List_of_Hilbert_systems

https://en.wikipedia.org/wiki/Relation_algebra

https://www.wolframscience.com/nks/p773--implications-for-mathematics-and-its-foundations/

http://us.metamath.org/mpeuni/mmset.html#axioms

http://us.metamath.org/metamath/nf.mm

https://github.com/leanprover/lean

http://us.metamath.org/mpeuni/mmtheorems.html

Theorema

https://github.com/windsteiger/Theorema

Metamath

http://us.metamath.org/metamath/set.mm

https://www.wolframfoundation.org/programs/SemanticWorkshopWhitePaper.pdf

https://writings.stephenwolfram.com/2014/08/computational-knowledge-and-the-future-of-pure-mathematics/