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 »
WOLFRAM NOTEBOOK
Where do human-found theorems live in metamathematical space?
Where do human-found theorems live in metamathematical space?
Cf where in 3D x,y,z space did people build cities on earth?
Boolean Algebra
Boolean Algebra
Entailment cone should give the true theorems, but not as efficiently
Entailment cone should give the true theorems, but not as efficiently
Can we tighten up what we find in the “entailment target/retention zone” [ “directed entailments” ]
Can we tighten up what we find in the “entailment target/retention zone” [ “directed entailments” ]
Ordinary theorem proving: we know the target, we want to find a single path
Traditional entailment cone: the entailments go out in all directions ... as opposed to making a “phased array” or an antenna in a particular direction
What are the proofs of interesting statements like?
What are the proofs of interesting statements like?
In[]:=
interesting=First/@{{a==a⋀a,"idempotent law for and"},{a==a⋁a,"idempotent law for or"},{a⋀b==b⋀a,"commutativity for and"},{a⋁b==b⋁a,"commutativity for or"},{a==a,"law of double negation"},{a⋀a==b⋀b,"definition of false (law of noncontradiction)"},{a⋁a==b⋁b,"definition of true (law of excluded middle)"},{(a⋁b)==a⋀b,"de Morgan law"},{(a⋀b)==a⋁b,"de Morgan law"},{a==a⋀(a⋁b),"absorption law"},{a==a⋁a⋀b,"absorption law"},{(a⋀b)⋀c==a⋀(b⋀c),"associativity of and"},{(a⋁b)⋁c==a⋁(b⋁c),"associativity of or"}};
In[]:=
AxiomaticTheory["BooleanAxioms"]
Out[]=
a.⊗b.b.⊗a.,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊕b.⊗a.,a.⊗b.⊕a.,a.⊕b.b.⊕a.,a.⊕b.⊗c.(a.⊕b.)⊗(a.⊕c.)
∀
{a.,b.}
∀
{a.,b.,c.}
∀
{a.,b.}
b.
∀
{a.,b.}
b.
∀
{a.,b.}
∀
{a.,b.,c.}
In[]:=
interesting/.{Square->OverBar,Vee->CirclePlus,Wedge->CircleTimes}
Out[]=
aa⊗a,aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a,⊗a⊗b,⊕a⊕b,⊗,⊕,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)
a
a
b
a
b
a⊕b
a
b
a⊗b
a
b
In[]:=
FindReplacePath[ForAll[a,aa⊗a],AxiomaticTheory["BooleanAxioms"]]
Out[]=
Statementa⊗aa,PathTestSuccess,RewriteTestSuccess,Justification{{{Axiom,1},Right,{}},{{Axiom,3},Right,{}},{{Axiom,2},Left,{}}},RewritesReplace[x1_x1⊕x2$11_⊗]/*ReplaceAll[x2$11_a._],Replace[x1_⊗x2_⊕x1_⊗x3_x1⊗(x2⊕x3)],Replace[x1_⊗(x2_⊕)x1],Path{a._⊗a._,a._⊗a._⊕a._⊗,a._⊗(a._⊕),a._}
x2$11_
x2_
a._
a._
In[]:=
FindEquationalProof[ForAll[a,aa⊗a],AxiomaticTheory["BooleanAxioms"]]
Out[]=
ProofObject
In[]:=
FindReplacePath[ForAll[{a,b,c},#],AxiomaticTheory["BooleanAxioms"],"Path"]&/@aa⊗a,aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a,⊗a⊗b,⊕a⊕b,⊗,⊕,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)
a
a
b
a
b
a⊕b
a
b
a⊗b
a
b
x2
b
x2
b
Out[]=
In[]:=
Length/@%
Out[]=
{4,4,2,2,16,6,6,704,704,34,36,205,205}
NOTE: LeafCount wrong because of _’s
In[]:=
MapThread[ListLinePlot[#,Frame->True,PlotLabel->#2]&,Map[LeafCount,%9,{2}],aa⊗a,aa⊕a,a⊗bb⊗a,a⊕bb⊕a,a,⊗a⊗b,⊕a⊕b,⊗,⊕,aa⊗(a⊕b),aa⊕a⊗b,(a⊗b)⊗ca⊗(b⊗c),(a⊕b)⊕ca⊕(b⊕c)]
a
a
b
a
b
a⊕b
a
b
a⊗b
a
b
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
Note that this is after cut elimination ....
Note that this is after cut elimination ....
Approximate the branching ratio for the entailment cone
Approximate the branching ratio for the entailment cone
With intermediate lemmas
With intermediate lemmas
Wannabe theorems:
I.e. there are no new variables generated.... [at least after canonicalization]
Other Axiom Systems
Other Axiom Systems
[ There are 3 proofs here; ATP found 1 ] [ There are many theorems; you pick the one you want ]
[ There are 3 proofs here; ATP found 1 ] [ There are many theorems; you pick the one you want ]
ATP is good if you already know the theorem you want
ATP is good if you already know the theorem you want
Discovering new theorems (e.g. my Boolean algebra axiom) is hard with ATP
Discovering new theorems (e.g. my Boolean algebra axiom) is hard with ATP
General approach: use models to find plausible theorems
General approach: use models to find plausible theorems
Start from the axioms and find all models consistent with the axioms ... then ask what relations satisfy those models
Directed Theorem Enumeration
Directed Theorem Enumeration
Instead of making the whole entailment cone, we only want “interesting theorems”
Instead of making the whole entailment cone, we only want “interesting theorems”
In the Metamath database, we’re seeing a skeleton of the entailment cone
In the Metamath database, we’re seeing a skeleton of the entailment cone
Metamath Database
Metamath Database
Imagine the entailment cone from the axioms of set theory
Imagine the entailment cone from the axioms of set theory
The MM database has a very thin skeleton of that entailment cone
The MM database has a very thin skeleton of that entailment cone
For the sake of argument, let’s assume MM’s proofs are minimal
For the sake of argument, let’s assume MM’s proofs are minimal
Can we estimate whether the skeleton is uniform across the entailment cone
Can we estimate whether the skeleton is uniform across the entailment cone
Guess is it’s not uniform in the EC, but instead it’s built out in towers....
Is there something special about the towers?
The big point is that higher-level math is possible; therefore having a sparse collection of towers may be “enough”
The big point is that higher-level math is possible; therefore having a sparse collection of towers may be “enough”
I.e. you can talk about math without going through all the detail of the whole entailment cone
What are the TEGs of the MM database?
What are the TEGs of the MM database?
The substitution entailment is more complicated in MM [ but it’s a simpler form of substitution, where it just replaces the variables ]
Each definition introduces a function symbol....
Each definition introduces a function symbol....
MM is embedding all math in an explicit entailment graph ...
MM is embedding all math in an explicit entailment graph ...
But most mathematical conclusions (AKA mathematical motion) never has to look down to axioms/emes/....
E.g. in physics we have laws of motion that don’t talk about the atoms of space....
Analog in math is “human-level proofs”
[ E.g. Euclid picked “human-like axioms” ]
Extreme coarse graining:
In a math result, you’re not necessarily talking about something very specific at the level of axioms, and certainly not at the level of emes....