Additional Axiom Systems from NKS
Additional Axiom Systems from NKS
In[]:=
{lab[{f[a,a]==a,f[a,b]==f[b,a],f[f[a,b],c]==f[a,f[b,c]]},"JunctionalCalculusAxioms"],lab[{f[f[a,b],f[b,c]]==a},"CentralGroupoidAxioms"],lab[{f[b,f[f[c,f[c,f[f[f[d,d],a],d]]],b]]==a},"SquagAxioms"],lab[{f[f[b,b],a]==a,f[a,b]==f[b,a],f[f[a,b],c]==f[a,f[b,c]]},"EquivalentialCalculusAxioms"],lab[{f[f[a,b],a]==a,f[a,f[b,c]]==f[b,f[a,c]],f[f[a,b],b]==f[f[b,a],a]},"ImplicationalCalculusAxioms"]}/.lab[x_,y_](yx)
In[]:=
{"JunctionalCalculusAxioms"{f[a,a]a,f[a,b]f[b,a],f[f[a,b],c]f[a,f[b,c]]},"CentralGroupoidAxioms"{f[f[a,b],f[b,c]]a},"SquagAxioms"{f[b,f[f[c,f[c,f[f[f[d,d],a],d]]],b]]a},"EquivalentialCalculusAxioms"{f[f[b,b],a]a,f[a,b]f[b,a],f[f[a,b],c]f[a,f[b,c]]},"ImplicationalCalculusAxioms"{f[f[a,b],a]a,f[a,f[b,c]]f[b,f[a,c]],f[f[a,b],b]f[f[b,a],a]}}/.{aa.,bb.,cc.,dd.,fCenterDot}
Out[]=
{JunctionalCalculusAxioms{a.·a.a.,a.·b.b.·a.,(a.·b.)·c.a.·(b.·c.)},CentralGroupoidAxioms{(a.·b.)·(b.·c.)a.},SquagAxioms{b.·((c.·(c.·(((d.·d.)·a.)·d.)))·b.)a.},EquivalentialCalculusAxioms{(b.·b.)·a.a.,a.·b.b.·a.,(a.·b.)·c.a.·(b.·c.)},ImplicationalCalculusAxioms{(a.·b.)·a.a.,a.·(b.·c.)b.·(a.·c.),(a.·b.)·b.(b.·a.)·a.}}