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:
This should give all info we know about the system:
In[]:=
AxiomaticTheory["WolframAxioms","Dataset"]
Out[]=
AxiomaticTheory[WolframAxioms,Dataset]
In[]:=
AxiomaticTheory["WolframAxioms","NotableTheorems"]
Out[]=
ImpliesShefferAxioms(a.·a.)·(a.·a.)a.,a.·(b.·(b.·b.))a.·a.,(a.·(b.·c.))·(a.·(b.·c.))((b.·b.)·a.)·((c.·c.)·a.),ImpliesHillmanAxioms(a.·a.)·(a.·b.)a.,a.·(a.·b.)a.·(b.·b.),a.·(a.·(b.·c.))b.·(b.·(a.·c.)),ImpliesMeredithAxiomsa.·(b.·(a.·c.))((c.·b.)·b.)·a.,(a.·a.)·(b.·a.)a.,ImpliesWolframAlternateAxioms(a.·((c.·a.)·a.))·(c.·(b.·a.))c.,ImpliesWolframCommutativeAxioms(a.·b.)·(a.·(b.·c.))a.,a.·b.b.·a.,Commutativitya.·b.b.·a.,DoubleNegation(a.·a.)·(a.·a.)a.,AndAssociativity(a.·((b.·c.)·(b.·c.)))·(a.·((b.·c.)·(b.·c.)))(((a.·b.)·(a.·b.))·c.)·(((a.·b.)·(a.·b.))·c.),OrAssociativity(a.·a.)·(((b.·b.)·(c.·c.))·((b.·b.)·(c.·c.)))(((a.·a.)·(b.·b.))·((a.·a.)·(b.·b.)))·(c.·c.)
∀
a.
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.,c.}
∀
{a.,b.}
∀
{a.,b.}
∀
a.
∀
{a.,b.,c.}
∀
{a.,b.,c.}
Transfer NotableTheorems from BooleanAxioms
Transfer NotableTheorems from BooleanAxioms
In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=
a.⊗b.b.⊗a.,a.⊕b.b.⊕a.,a.⊗b.⊕a.,a.⊕b.⊗a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
∀
{a.,b.}
∀
{a.,b.}
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.,c.}
∀
{a.,b.,c.}
In[]:=
AxiomaticTheory["BooleanAxioms","NotableTheorems"]
Out[]=
ImpliesHuntingtonAxiomsa.⊕b.b.⊕a.,a.⊕(b.⊕c.)(a.⊕b.)⊕c.,⊕b.⊕⊕a.,ImpliesRobbinsAxiomsa.⊕b.b.⊕a.,a.⊕(b.⊕c.)(a.⊕b.)⊕c.,⊕a.,DoubleNegationa.,DeMorgan⊗,⊕
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
a.
a.
b.
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
a.⊕b.
a.⊕
b.
∀
a.
a.
∀
{a.,b.}
a.⊕b.
a.
b.
∀
{a.,b.}
a.⊗b.
a.
b.
In[]:=
AxiomaticTheory["BooleanAxioms","Operators"]
Out[]=
AndCircleTimes,OrCirclePlus,NotOverBar
In[]:=
InputForm[%24]
Out[]//InputForm=
<|And -> CircleTimes, Or -> CirclePlus, Not -> OverBar|>
Presburger arithmetic
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[]=
{CircleTimes2,CirclePlus2,OverBar1}
In[]:=
<|"PresburgerArithmeticAxioms"<|"Operators"<|"Plus"CirclePlus,"Negation"Square|>,"OperatorArities"<|CirclePlus2,Square1|>,"Axioms"->a.⊕0a.,a.⊕a.0,(a.⊕b.)⊕c.a.⊕(b.⊕c.)|>|>
∀
a.
∀
a.
∀
{a.,b.,c.}
Out[]=
PresburgerArithmeticAxiomsOperatorsPlusCirclePlus,NegationSquare,OperatorAritiesCirclePlus2,Square1,Axiomsa.⊕0a.,a.⊕a.0,(a.⊕b.)⊕c.a.⊕(b.⊕c.)
∀
a.
∀
a.
∀
{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]]]}/.{plusCirclePlus,negSquare,xa.,yb.,zc.}
Out[]=
a.⊕0a.,a.⊕a.0,(a.⊕b.)⊕c.a.⊕(b.⊕c.)
∀
a.
∀
a.
∀
{a.,b.,c.}
Should add Description
Should add Description
"Fragment of Presburger arithmetic"
Adding in axioms (AKA relations) for specific groups
Adding in axioms (AKA relations) for specific groups
In[]:=
AxiomaticTheory["GroupAxioms"]
Out[]=
a.⊗(b.⊗c.)(a.⊗b.)⊗c.,a.⊗a.,a.⊗
∀
{a.,b.,c.}
∀
a.
1
∀
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∘3∘2∘3∘1
∘-1
3
∘-1
2
In[]:=
FiniteGroupData["Quaternion","DefiningRelations"]/.{2a.,3b.}
Out[]=
a.∘b.∘a.∘b.∘a.∘b.∘1
∘-1
b.
∘-1
a.
AxiomaticTheory[{"GroupAxioms","Quaternion"}]
In FiniteGroupData ... ? “AxiomaticRelations”
Logic puzzles
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
NKS book
{x[1]a.,x[2]b.,x[3]c.,x[4]d.}
Peano arithmetic
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,equalHumpEqual,impliesDoubleRightArrow,unequalNotHumpEqual,plusCirclePlus,timesCircleTimes,sSquare})
Out[]=
{0a.,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
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]]]]],""}};
Real algebra
Real algebra
Additional Elements
Additional Elements
“Description”
“Description”
“Reference”
“Reference”
“FormulationDate”
“FormulationDate”
“AxiomNames”
“AxiomNames”
Axiom Systems from the Web, etc.
Axiom Systems from the Web, etc.
https://en.wikipedia.org/wiki/List_of_Hilbert_systems
https://en.wikipedia.org/wiki/List_of_Hilbert_systems
https://en.wikipedia.org/wiki/Relation_algebra
https://en.wikipedia.org/wiki/Relation_algebra
https://www.wolframscience.com/nks/p773--implications-for-mathematics-and-its-foundations/
https://www.wolframscience.com/nks/p773--implications-for-mathematics-and-its-foundations/
http://us.metamath.org/mpeuni/mmset.html#axioms
http://us.metamath.org/mpeuni/mmset.html#axioms
http://us.metamath.org/metamath/nf.mm
http://us.metamath.org/metamath/nf.mm
https://github.com/leanprover/lean
https://github.com/leanprover/lean
http://us.metamath.org/mpeuni/mmtheorems.html
http://us.metamath.org/mpeuni/mmtheorems.html
Theorema
Theorema
https://github.com/windsteiger/Theorema
https://github.com/windsteiger/Theorema
Metamath
Metamath
http://us.metamath.org/metamath/set.mm
http://us.metamath.org/metamath/set.mm
https://www.wolframfoundation.org/programs/SemanticWorkshopWhitePaper.pdf
https://www.wolframfoundation.org/programs/SemanticWorkshopWhitePaper.pdf
https://writings.stephenwolfram.com/2014/08/computational-knowledge-and-the-future-of-pure-mathematics/
https://writings.stephenwolfram.com/2014/08/computational-knowledge-and-the-future-of-pure-mathematics/