Consider the “current state of math” as a collection of symbolic expressions
Consider the “current state of math” as a collection of symbolic expressions
Addition facts:
In[]:=
Table[eq[Nest[s,0,i+j],plus[Nest[s,0,i],Nest[s,0,j]]],{i,3},{j,3}]
Out[]=
{{eq[s[s[0]],plus[s[0],s[0]]],eq[s[s[s[0]]],plus[s[0],s[s[0]]]],eq[s[s[s[s[0]]]],plus[s[0],s[s[s[0]]]]]},{eq[s[s[s[0]]],plus[s[s[0]],s[0]]],eq[s[s[s[s[0]]]],plus[s[s[0]],s[s[0]]]],eq[s[s[s[s[s[0]]]]],plus[s[s[0]],s[s[s[0]]]]]},{eq[s[s[s[s[0]]]],plus[s[s[s[0]]],s[0]]],eq[s[s[s[s[s[0]]]]],plus[s[s[s[0]]],s[s[0]]]],eq[s[s[s[s[s[s[0]]]]]],plus[s[s[s[0]]],s[s[s[0]]]]]}}
In[]:=
ExpressionTree/@Flatten[%7]
Out[]=
,
,
,
,
,
,
,
,
Each relation here is like a hyperedge, with certain shared atoms
Hyperedges can be combined through a token-event mechanism
Other examples:
boolean equivalences, order relations (e.g. 7 > 5) etc.
Other examples:
boolean equivalences, order relations (e.g. 7 > 5) etc.
boolean equivalences, order relations (e.g. 7 > 5) etc.
Substitution requires the concept of replacing variables with whole expressions
Substitution requires the concept of replacing variables with whole expressions
Or some other metalogical assumption
e.g.
a==b&&b==ca==c
But also need a novelty generator (e.g. add tautologies)
Worth considering geodesics because math derivations are at least fairly direct
Worth considering geodesics because math derivations are at least fairly direct
Multiway graph: multiple histories for math / multiple proof paths
Multiway graph: multiple histories for math / multiple proof paths
State of math: ~space ; history of math: ~spacetime ; proof: ~timelike curve
State of math: ~space ; history of math: ~spacetime ; proof: ~timelike curve
Proof cones
Proof cones
Proxy for “distance between relations”: how far apart they appear in a textbook [cf Euclid]
Proxy for “distance between relations”: how far apart they appear in a textbook [cf Euclid]
Perceptual distance in Euclid
Max speed in metamathematical space?
Max speed in metamathematical space?
How fast can one reach another area in math?
Rederivation knits together metamathematical space (?)
Rederivation knits together metamathematical space (?)
[ Conceptually: record every time a mathematician writes down any derivation ]
Metamathematical motion
Metamathematical motion
?Functors :: preservation of structure ?
Rulial version: all possible “mathematical laws” / all possible metalogics
Rulial version: all possible “mathematical laws” / all possible metalogics
A particular rulial frame = particular metalogic
Theorem proving
Theorem proving
Substitution lemma
Critical pair lemma
Critical pair lemma
Definitions are just abstract atoms
Definitions are just abstract atoms
If two relations refer to the same thing, they just connect to the same atom....
Is it only the atoms that are shared, or are common subexpressions also shared?
Is it only the atoms that are shared, or are common subexpressions also shared?
Instead of ordered hyperedges, use trees...
Instead of ordered hyperedges, use trees...
Generalization of ordered hypergraph; instead of simple chain, have tree. ? Analogy in causal multiway system
Transformations on expression trees instead of hyperedges ? [ Or have expression instead of hypergraph ]
unordered [ tree1, tree2, ... ]
Expression derivation
Expression derivation
Out[]=
Rules of inference
Rules of inference
Take two statements; make another
,
,
In[]:=
TreeExtract
,2
Out[]=
In[]:=
TreeExtract
,{2,2}
Out[]=
Axioms are statements in the initial state; evolution is rules of inference
Axioms are statements in the initial state; evolution is rules of inference
Spacelike surfaces are all possible statements of math at a particular time
Light cone of a given initial set of statements are the results for a single axiom system
Spacelike surfaces are all possible statements of math at a particular time
Light cone of a given initial set of statements are the results for a single axiom system
Light cone of a given initial set of statements are the results for a single axiom system
E.g. my Boolean axiom has a light cone that contains all statements of Boolean algebra
Causal dependence: which inferences affect which others : i.e. which inferences are in proof chains
Causal dependence: which inferences affect which others : i.e. which inferences are in proof chains
Ruliad limit: all possible initial states + all possible rules of inference
Ruliad limit: all possible initial states + all possible rules of inference
Model: add more statements e.g. in the initial state more things can be generated
Model: add more statements e.g. in the initial state more things can be generated
E.g. more is true about a specific group than a general group
Add too much “energy” in models and you get to a normal form, i.e. a spacelike singularity [?]
Add too much “energy” in models and you get to a normal form, i.e. a spacelike singularity [?]
Every shortest inference chain is a geodesic... (i.e. every “best derivation”)
Every shortest inference chain is a geodesic... (i.e. every “best derivation”)
The more axioms/statements one adds, the closer one gets to decidability (?)
The more axioms/statements one adds, the closer one gets to decidability (?)
Mathematical assertion ~ mass ; too much of it and you get a black hole (?)
Mathematical assertion ~ mass ; too much of it and you get a black hole (?)
E.g. a group: the more relations you add, the smaller the group gets... The smaller the group, the more identities between words are generated
Time dilation: you either drill down and make proofs about the original thing you’re talking about ... or you have to “move” to talk about something different ... then you use some of your laws of inference to make that move....
Time dilation: you either drill down and make proofs about the original thing you’re talking about ... or you have to “move” to talk about something different ... then you use some of your laws of inference to make that move....
If you stay in one area of math, you can make more proofs than if you try to make proofs about different kinds of things....
Twin paradox for mathematicians: a mathematician who keeps on exploring new areas won’t be able to prove as much.... because they’re using their inference rate to move rather than to “prove down” (i.e. to make a longer proof about a specific thing)