In[]:=
ExpressionTree/@Flatten[Table[eq[Nest[s,0,i+j],plus[Nest[s,0,i],Nest[s,0,j]]],{i,3},{j,3}]]
Out[]=
,
,
,
,
,
,
,
,
{eq[a_,b_],eq[b_,c_]}->{eq[a,c]}
What are the rules for combining these results?
What are the rules for combining these results?
In[]:=
ExpressionTree/@Groupings[{1,1,1,1,1},plus->2]
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
,
Rules for equivalence relations...
Rules for equivalence relations...
equal[a_,b_]->equal[b,a]
{eq[a_,b_],eq[b_,c_]}->{eq[a,c]}
plus[0,a_]->a
plus[s[a_],b_]->s[plus[a,b]]
In[]:=
plus[Nest[s,0,3],Nest[s,0,2]]
Out[]=
plus[s[s[s[0]]],s[s[0]]]
In[]:=
TokenEventGraph[{{plus[s[a_],b_]}:>{s[plus[a,b]]},{plus[0,a_]}:>{a}},{plus[Nest[s,0,3],Nest[s,0,2]]},3]
Out[]=
In[]:=
TokenEventGraph[{{plus[s[a_],b_]}:>{s[plus[a,b]],plus[a,b]},{plus[0,a_]}:>{a}},{plus[Nest[s,0,3],Nest[s,0,2]]},3]
Out[]=
Needs treelike replacements...
In[]:=
Replace[plus[Nest[s,0,3],Nest[s,0,2]],plus[s[a_],b_]:>s[plus[a,b]]]
Out[]=
s[plus[s[s[0]],s[s[0]]]]
Two kinds of “equality”: (1) “symbolic equality”, (2) substitutional equality
Two kinds of “equality”: (1) “symbolic equality”, (2) substitutional equality
equal[a,a]
In[]:=
TokenEventGraph[{{a_}:>{s[a]},{s[plus[a_,b_]]}:>{plus[s[a],b]},{a_}:>{plus[0,a]}},{0},3]
Out[]=
Can we construct “true theorems” (i.e. equalities) of the Plus world?
Can we construct “true theorems” (i.e. equalities) of the Plus world?
In Polish notation, we have to have strings-as-linked-lists to thread things back together
In Polish notation, we have to have strings-as-linked-lists to thread things back together
Or use trees, then have reinsertion...
Or use trees, then have reinsertion...
Can have rules that apply themselves at any level.... (cf https://www.wolframcloud.com/obj/wolframphysics/Tools/combinators )
Can have rules that apply themselves at any level.... (cf https://www.wolframcloud.com/obj/wolframphysics/Tools/combinators )
This is only establishing True for a particular
Multicomputational evaluator
Multicomputational evaluator
Ordinary case:
Transformations get done by mapping through the expression, and by reevaluation....
The usual evaluator involves a single total ordering of updates....
[ Rules can’t have been assigned because then the ordinary evaluator will try to use them ]
Things one could compute
Things one could compute
◼
Set of normal forms (e.g. multibranch recursive function)
◼
Path weight to normal form
◼
Existence of path to a given expression
◼
Path to a given expression, with all “incoming tentacles” included [i.e. proof of path]
◼
Equivalence classes of expressions produced
◼
Collections of expressions that can be considered “complete states”
Issue: whether to include path weights or not [included if there is not deduplication]
Issue: whether to include path weights or not [included if there is not deduplication]
Note: could look not for normal form, but for repeating form, etc. [and could do this in the ordinary evaluator as well]
Note: could look not for normal form, but for repeating form, etc. [and could do this in the ordinary evaluator as well]
Loop detection in the ordinary evaluator
Loop detection in the ordinary evaluator
What “trivial” behavior can occur?
What “trivial” behavior can occur?
Once it’s trivial, it’s pretty much guaranteed not to terminate....
Tree walking in the multicomputation graph
Tree walking in the multicomputation graph
Can put events in a certain order based on where they occur on the tree... The foliation corresponds to the traversal order...
Can put events in a certain order based on where they occur on the tree... The foliation corresponds to the traversal order...
Want to number nodes to indicate traversal order
Cross-Reference of Theorems
Cross-Reference of Theorems
This is a token-event graph sampled only for the “humanly interesting theorems”
This is a token-event graph sampled only for the “humanly interesting theorems”
Coarse-graining is by human aesthetics
Coarse-graining is by human aesthetics
Type Theory?
Type Theory?
Homotopy type theory
Homotopy type theory
Univalence axiom : “equivalence is equivalent to equality”
[[ Patterns are equivalent to types ... ]]
Type being inhabited ⇔ set has an element ⇔ [there is a construction for things of that type]
Type being inhabited ⇔ set has an element ⇔ [there is a construction for things of that type]
List : product type ; Alternatives : sum type
Except[_] : void type
Proof of inhabitance: exhibit an expression that matches
Analogous statement? paths with the same
Analogous statement? paths with the same
Tokens vs events :: expressions vs transformations
Tokens vs events :: expressions vs transformations
Mathematics
Mathematics
Translation between mathematical axiom systems ⇔ time dilation
Translation between mathematical axiom systems ⇔ time dilation
Singularities ⇔ decidability
Singularities ⇔ decidability
Proof density ~ energy
Different axiom systems ⇔ reference frames
Different axiom systems ⇔ reference frames
wrt a universal collection of proofs defined by a certain law of inference
Geometer vs algebraist: different reference frames + different coarse graining
Geometer vs algebraist: different reference frames + different coarse graining
At “mathematician scale” many equivalences are used: e.g. there are [700] underlying representations of a pentagon, but the mathematician says it’s a pentagon
At “mathematician scale” many equivalences are used: e.g. there are [700] underlying representations of a pentagon, but the mathematician says it’s a pentagon
Is there a universal mathematician? Category theorist
Is there a universal mathematician? Category theorist
Continuum hypothesis:
Continuum hypothesis:
1. It’s a certain reference frame that makes it true or false
2. There’s no human-compatible reference frame that makes it false (cf naked singularities ; no computable reference frame)
2. There’s no human-compatible reference frame that makes it false (cf naked singularities ; no computable reference frame)
Event horizon: separated area of math that’s decidable
Event horizon: separated area of math that’s decidable
E.g. you can’t derive number theory from Boolean algebra
Can there be a cosmological event horizon: math is broken into two parts?
Can there be a cosmological event horizon: math is broken into two parts?
Is the mathematical universe expanding? Yes, at the level of tokens. Not so obvious at the coarse-grained level
Is the mathematical universe expanding? Yes, at the level of tokens. Not so obvious at the coarse-grained level
Limit of mathematics: it’s all connected, except for the black holes [decidable theories] ... but note that there might be “no hair” for decidable theories ... i.e. they are all the same
Limit of mathematics: it’s all connected, except for the black holes [decidable theories] ... but note that there might be “no hair” for decidable theories ... i.e. they are all the same
What is the distribution of mathematical statements in “mathematical branchial space”?
What is the distribution of mathematical statements in “mathematical branchial space”?
Is there an analog of physical space in mathematics, or is it all branchial? [Is there an analog of pure motion in math?]
Is there an analog of physical space in mathematics, or is it all branchial? [Is there an analog of pure motion in math?]
Feature of ruliad: physical and branchial space are somehow equivalent
Feature of ruliad: physical and branchial space are somehow equivalent
What is the quantum theory of mathematics?
What is the quantum theory of mathematics?
It’s associated with the story of multiple proofs ;
right now, math is classical, because you just want to know that there is a proof...
right now, math is classical, because you just want to know that there is a proof...
Does the mathematical observer conflate proofs?
[“Extensional equality” : conflate all proofs]
[“Intensional equality” : multiple proofs construct the same result ]
< QM is about stopping part way through the proof, and seeing the distribution of where you got >
[“Extensional equality” : conflate all proofs]
[“Intensional equality” : multiple proofs construct the same result ]
< QM is about stopping part way through the proof, and seeing the distribution of where you got >
[ How do you parametrize the threads of proof? ]
Destructive interference: two proofs that have very distant intermediate stages [i.e. no single mathematician can “hold those two proofs in mind at the same time” (or they are actually contradictory) [ in terms of patterns, it becomes patterns that can’t be unified ] [ destructive interference: you have to prove the conjunction of the intermediate statements ]
[ probability distributions on intermediate proof states ]
[[ Virtual particles: ~ p⋁¬p continually being generated ]]
[[ Virtual particles: ~ p⋁¬p continually being generated ]]
[ ?? path integral in math ]
Are TEGs (“multicomputational graphs”) a good machine code for all foundational idealizations of math?
Are TEGs (“multicomputational graphs”) a good machine code for all foundational idealizations of math?
Equational proofs
Modus ponens proofs
HTT
Intuitionism
Modus ponens proofs
HTT
Intuitionism
⟶ metametamathematics
⟶ metametamathematics
WL is meta computational mathematics [general description of computational math]
WL is not (yet) the general description of proof-based math [needs a new evaluator]
WL is not (yet) the general description of proof-based math [needs a new evaluator]
What is a particle in math?
What is a particle in math?
Related to persistent concepts that exist at the “observer level”
Reference frame is defined by a set of patterns
Reference frame is defined by a set of patterns
Particle is a persistently matching expression that continues at different slices in the foliation
Foundations of computational math vs. foundations of mathematicians’ mathematics
Foundations of computational math vs. foundations of mathematicians’ mathematics
In a sense, Hilbert already defined the machine code of math ; like we’ve defined machine code of physics
But he didn’t figure out the continuum limit
But he didn’t figure out the continuum limit
Metamathematical space is the space in which the continuum limit will play out...
Metamathematical space is the space in which the continuum limit will play out...