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.,ImpliesWolframCommutativeAxiomsa.·b.·a.·b.·c.a.,a.·b.b.·a.,Commutativitya.·b.b.·a.,DoubleNegation(a.·a.)·(a.·a.)a.,AndAssociativitya.·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.,andsubα_,a.,0,forallb.,subα_,a.,b.⇒subα_,a.,b.⇒insertboxes,forallb.,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.
Theorema
Theorema
Metamath
Metamath