WOLFRAM NOTEBOOK

Rearranging variables

In[]:=
Union[Level[((a.·b.)·c.)·(a.·((a.·c.)·a.)),{-1}]]
Out[]=
{a.,b.,c.}
In[]:=
varperms=Thread[{a.,b.,c.}->#]&/@Permutations[{a.,b.,c.}]
Out[]=
{{a.a.,b.b.,c.c.},{a.a.,b.c.,c.b.},{a.b.,b.a.,c.c.},{a.b.,b.c.,c.a.},{a.c.,b.a.,c.b.},{a.c.,b.b.,c.a.}}
In[]:=
Last[First[AxiomaticTheory["WolframAxioms"]]]/.#&/@varperms
Out[]=
{((a.·b.)·c.)·(a.·((a.·c.)·a.))c.,((a.·c.)·b.)·(a.·((a.·b.)·a.))b.,((b.·a.)·c.)·(b.·((b.·c.)·b.))c.,((b.·c.)·a.)·(b.·((b.·a.)·b.))a.,((c.·a.)·b.)·(c.·((c.·b.)·c.))b.,((c.·b.)·a.)·(c.·((c.·a.)·c.))a.}
In[]:=
ParallelMapFindEquationalProof[p·q==q·p,ForAll[{a.,b.,c.},#]]&,
Out[]=
ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·p
,ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·p
,ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·p
,ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·p
,ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·p
,ProofObject
Logic: EquationalLogic
Steps: 102
Theorem: p·qq·p
In[]:=
Take[#["ProofDataset"],4]&/@%
Out[]=
Statement
Proof
Axiom
1
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
Hypothesis
1
p·qq·p
CriticalPairLemma
1
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
11 total ›
CriticalPairLemma
2
a.(b.·a.)·(((c.·α.)·b.)·((((c.·α.)·b.)·a.)·((c.·α.)·b.)))
11 total ›
,
Statement
Proof
Axiom
1
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
Hypothesis
1
p·qq·p
CriticalPairLemma
1
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
11 total ›
CriticalPairLemma
2
a.(b.·a.)·(((c.·α.)·b.)·((((c.·α.)·b.)·a.)·((c.·α.)·b.)))
11 total ›
,
Statement
Proof
Axiom
1
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
Hypothesis
1
p·qq·p
CriticalPairLemma
1
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
11 total ›
CriticalPairLemma
2
a.(b.·a.)·(((c.·α.)·b.)·((((c.·α.)·b.)·a.)·((c.·α.)·b.)))
11 total ›
,
Statement
Proof
Axiom
1
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
Hypothesis
1
p·qq·p
CriticalPairLemma
1
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
11 total ›
CriticalPairLemma
2
a.(b.·a.)·(((c.·α.)·b.)·((((c.·α.)·b.)·a.)·((c.·α.)·b.)))
11 total ›
,
Statement
Proof
Axiom
1
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
Hypothesis
1
p·qq·p
CriticalPairLemma
1
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
11 total ›
CriticalPairLemma
2
a.(b.·a.)·(((c.·α.)·b.)·((((c.·α.)·b.)·a.)·((c.·α.)·b.)))
11 total ›
,
Statement
Proof
Axiom
1
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
Hypothesis
1
p·qq·p
CriticalPairLemma
1
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
11 total ›
CriticalPairLemma
2
a.(b.·a.)·(((c.·α.)·b.)·((((c.·α.)·b.)·a.)·((c.·α.)·b.)))
11 total ›
I.e. variables got arranged before going into FEP
ResourceFunction[""]
In[]:=
AxiomaticTheory["WolframAxioms"]/.Thread[{a.,b.,c.}->{a,b,c}]
Out[]=
∀
{a,b,c}
((a·b)·c)·(a·((a·c)·a))c
In[]:=
%[[1,-1]]
Out[]=
((a·b)·c)·(a·((a·c)·a))c

External Provers

From the equational logic axiom ((a·b)·c)·(a·((a·c)·a)) == c prove that p·q == q·p. Assume nothing about Center other than what can be deduced from the axiom

Enumerate Nand Truths

Note: p·q == q·p is the simplest theorem true of Nand
In[]:=
canonize[expr_]:=With[{s=Union[Flatten[Level[expr,{-1}]]]},First[Sort[expr/.#&/@(Thread[s->#]&/@Permutations[s])]]]
In[]:=
nandtest[expr_,vars_]:=TautologyQ[expr/.f->Nand,vars]
In[]:=
sources[nsym_,ct_]:=Flatten[Groupings[#,f->2]&/@Catenate[Table[Tuples[Symbol/@Take[Alphabet[],nsym],n],{n,ct}]]]
In[]:=
sources[2,3]
Out[]=
{a,b,f[a,a],f[a,b],f[b,a],f[b,b],f[f[a,a],a],f[a,f[a,a]],f[f[a,a],b],f[a,f[a,b]],f[f[a,b],a],f[a,f[b,a]],f[f[a,b],b],f[a,f[b,b]],f[f[b,a],a],f[b,f[a,a]],f[f[b,a],b],f[b,f[a,b]],f[f[b,b],a],f[b,f[b,a]],f[f[b,b],b],f[b,f[b,b]]}
In[]:=
sources[1,3]
Out[]=
{a,f[a,a],f[f[a,a],a],f[a,f[a,a]]}
In[]:=
With[{e=Join[sources[1,3],sources[2,3]]},Union[canonize/@Select[DeleteCases[Flatten[Outer[Equal,e,e]],True],nandtest[#,{a,b}]&]]]
Out[]=
{f[a,b]f[b,a],f[a,f[a,a]]f[b,f[b,b]],f[a,f[a,a]]f[f[a,a],a],f[a,f[a,a]]f[f[b,b],b],f[a,f[a,b]]f[a,f[b,a]],f[a,f[a,b]]f[a,f[b,b]],f[a,f[a,b]]f[f[a,b],a],f[a,f[a,b]]f[f[b,a],a],f[a,f[a,b]]f[f[b,b],a],f[a,f[b,a]]f[a,f[a,b]],f[a,f[b,a]]f[a,f[b,b]],f[a,f[b,a]]f[f[a,b],a],f[a,f[b,a]]f[f[b,a],a],f[a,f[b,a]]f[f[b,b],a],f[a,f[b,b]]f[a,f[a,b]],f[a,f[b,b]]f[a,f[b,a]],f[a,f[b,b]]f[f[a,b],a],f[a,f[b,b]]f[f[b,a],a],f[a,f[b,b]]f[f[b,b],a],f[b,f[b,b]]f[f[b,b],b],f[f[a,a],a]f[a,f[a,a]],f[f[a,a],a]f[b,f[b,b]],f[f[a,a],a]f[f[b,b],b],f[f[a,a],b]f[b,f[a,a]],f[f[a,a],b]f[b,f[a,b]],f[f[a,a],b]f[b,f[b,a]],f[f[a,a],b]f[f[a,b],b],f[f[a,a],b]f[f[b,a],b],f[f[a,b],a]f[a,f[a,b]],f[f[a,b],a]f[a,f[b,a]],f[f[a,b],a]f[a,f[b,b]],f[f[a,b],a]f[f[b,a],a],f[f[a,b],a]f[f[b,b],a],f[f[a,b],b]f[b,f[a,a]],f[f[a,b],b]f[b,f[a,b]],f[f[a,b],b]f[b,f[b,a]],f[f[a,b],b]f[f[a,a],b],f[f[a,b],b]f[f[b,a],b],f[f[b,b],b]f[b,f[b,b]]}
In[]:=
ParallelMap[FindEquationalProof[#/.f->CenterDot,AxiomaticTheory["WolframAxioms"]]&,%195]
Out[]=
In[]:=
#["ProofLength"]&/@%
Out[]=
{102,138,58,136,102,119,91,103,120,102,118,103,93,119,119,118,120,121,102,58,58,136,137,102,119,120,122,121,91,103,120,102,121,121,93,103,122,102,58}
In[]:=
ListStepPlot[%]
Out[]=
Why does a lemma get repeated?
I.e. most theorems use the same lemmas....
What’s with the weird error messages??
Lemmas used by all proofs:
WHY do these theorems not help??
SImplify lemmas by var names
Which of these algebraic relations have standard names : {a·b b·a, a (a·b)·(a·a), (a·a)·(a·a) a, (a·b)·(b·b) b, a (a·b)·(a·(b·c)), a (a·b)·(a·(c·b)), a (a·b)·((b·c)·a), a (a·b)·((c·b)·a), a (b·a)·(a·(b·c)), a (b·a)·((b·c)·a), a (b·(b·b))·(a·a), a ((a·b)·a)·(a·a), a·a a·(a·(a·a)), a·a a·((a·a)·a), a·b a·((a·b)·a), a·b b·(b·(a·a)), a·b ((a·b)·a)·a, a·(a·a) b·(b·b), a·(a·a) (b·b)·b, a·(a·(b·a)) b·a, a·(b·a) a·(b·b), a·(b·a) (b·a)·a, a·(b·(a·b)) a·a, a·(b·(b·b)) a·a, a·(a·a) b·(b·b), a·(a·a) c·(c·c), a·(a·a) (b·b)·b, a·(a·a) (c·c)·c, a·(a·b) a·(b·b), a·(a·b) (b·b)·a, a·(a·c) a·(c·c), a·(a·c) (c·c)·a, a·(b·a) a·(b·b), a·(b·b) a·(a·b), a·(b·b) a·(b·a), a·(c·a) a·(c·c), a·(c·c) a·(a·c), a·(c·c) a·(c·a), b·(a·a) b·(a·b), b·(a·a) b·(b·a), b·(a·b) b·(a·a), b·(a·b) (a·a)·b, b·(b·a) b·(a·a), b·(b·a) (a·a)·b, b·(b·b) a·(a·a), b·(b·b) c·(c·c), b·(b·b) (c·c)·c, b·(b·c) b·(c·c), b·(b·c) (c·c)·b, b·(c·b) b·(c·c)}
Which of these algebraic relations have standard names : {a·b b·a, a (a·b)·(a·a), (a·a)·(a·a) a, (a·b)·(b·b) b, a (a·b)·(a·(b·c)), a (a·b)·(a·(c·b)), a (a·b)·((b·c)·a), a (a·b)·((c·b)·a), a (b·a)·(a·(b·c)), a (b·a)·((b·c)·a)}
In what fields of math do these algebraic relations occur. Make a list of relations and areas : {a·b b·a, a (a·b)·(a·a), (a·a)·(a·a) a, (a·b)·(b·b) b, a (a·b)·(a·(b·c)), a (a·b)·(a·(c·b)), a (a·b)·((b·c)·a), a (a·b)·((c·b)·a), a (b·a)·(a·(b·c)), a (b·a)·((b·c)·a), a (b·(b·b))·(a·a), a ((a·b)·a)·(a·a), a·a a·(a·(a·a)), a·a a·((a·a)·a), a·b a·((a·b)·a), a·b b·(b·(a·a)), a·b ((a·b)·a)·a, a·(a·a) b·(b·b), a·(a·a) (b·b)·b, a·(a·(b·a)) b·a, a·(b·a) a·(b·b), a·(b·a) (b·a)·a, a·(b·(a·b)) a·a, a·(b·(b·b)) a·a, a·(a·a) b·(b·b), a·(a·a) c·(c·c), a·(a·a) (b·b)·b, a·(a·a) (c·c)·c, a·(a·b) a·(b·b), a·(a·b) (b·b)·a, a·(a·c) a·(c·c), a·(a·c) (c·c)·a, a·(b·a) a·(b·b), a·(b·b) a·(a·b), a·(b·b) a·(b·a), a·(c·a) a·(c·c), a·(c·c) a·(a·c), a·(c·c) a·(c·a), b·(a·a) b·(a·b), b·(a·a) b·(b·a), b·(a·b) b·(a·a), b·(a·b) (a·a)·b, b·(b·a) b·(a·a), b·(b·a) (a·a)·b, b·(b·b) a·(a·a), b·(b·b) c·(c·c), b·(b·b) (c·c)·c, b·(b·c) b·(c·c), b·(b·c) (c·c)·b, b·(c·b) b·(c·c)}

Making a proof comprehensible is like doing natural science on “proof data”

What are the “effective laws” of the theorem prover?

Intuitional question: why would a theorem like that be true?

General answer PCE. Can one guess how complex the axiom will have to be?
Can one evolve to the axiom??
What kind of axioms force a particular pattern of models?

A lot of my kind of experimental math is very visual; one develops an intuition

Needs to connect to a concept we know [ now also CI and PCE ]

What are known concepts in universal algebra?
E.g. what are models of the various lemmas like?
Are there general algebraic properties (like “assio-associativity”) that the axiom specifies? And that eventually lead to e.g. commutativity?
Wolfram Cloud

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.


I understand and wish to continue anyway »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.