#### 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)