## Metamodel of mathematics

Metamodel of mathematics

#### Pool of patterns

Pool of patterns

{a_[b_,c_],b_[a_,c_],a_[b_],b_[c_],rule_[a_,b_]}

There is a pool of objects containing variables that can correspond to any expression tree....

theory={(*naturalnumberarithmetic*)e_[z_,n_],e_[a_,n_]->e_[s_[a_],n_],e_[nn_,n_]->p_[z_,nn_],A_[E_[n_,N_],A_[E_[m_,N_],P_[n_,s_[m_]]]]->s_[P_[n_,m_]](*modusPonens*)(*...*)};

e_[z_, n_] z (i.e. zero) is an element of the natural numbers

e_[a_,n_]->e_[s_[a_],n_], If a is a natural number, then so is successor[a]

#### Entailment rules (AKA events)

Entailment rules (AKA events)

In[]:=

logic={{x:Except[_Rule],y:Except[_Rule]}:>{x,y,A_[x,y]}};

In[]:=

modusPonens={rule:Rule[lhs_,rhs_],expr:Except[_Rule]}/;MatchQ[expr,lhs]:>{rule,lhs,Replace[expr,lhs:>Evaluate[(rhs/.(Verbatim[#]->First[#]&/@Cases[lhs,_Pattern,All,Heads->True]))]]};

### Nik/James code

Nik/James code

In[]:=

theory={(*naturalnumberarithmetic*)E_[z_,N_],E_[a_,N_]->E_[s_[a_],N_],E_[n_,N_]->P_[z_,n_],A_[E_[n_,N_],A_[E_[m_,N_],P_[n_,s_[m_]]]]->s_[P_[n_,m_]](*modusPonens*)(*...*)};

In[]:=

logic={{x:Except[_Rule],y:Except[_Rule]}:>{x,y,A_[x,y]}};

In[]:=

modusPonens={rule:Rule[lhs_,rhs_],expr:Except[_Rule]}/;MatchQ[expr,lhs]:>{rule,lhs,Replace[expr,lhs:>Evaluate[(rhs/.(Verbatim[#]->First[#]&/@Cases[lhs,_Pattern,All,Heads->True]))]]};

In[]:=

rules=Append[logic,modusPonens];

In[]:=

rules

Out[]=

{{x:Except[_Rule],y:Except[_Rule]}{x,y,A_[x,y]},{rule:(lhs_rhs_),expr:Except[_Rule]}/;MatchQ[expr,lhs]{rule,lhs,Replace[expr,lhsEvaluate[rhs/.(Verbatim[#1]First[#1]&)/@Cases[lhs,_Pattern,All,HeadsTrue]]]}}

In[]:=

deleteDuplicatePatterns[g_Graph]:=Subgraph[g,DeleteDuplicates[VertexList[g],MatchQ[#1,#2]&&MatchQ[#2,#1]&]]

In[]:=

Graph[deleteDuplicatePatterns@TokenEventGraph[rules,theory,2,"EventDeduplication"->True,"TokenDeduplication"->True,"AllSubsets"->True,GraphLayout"SpringElectricalEmbedding","TokenLabeling"->None],VertexLabels(v_:>Placed[v,Tooltip])]

Out[]=

In[]:=

Graph[deleteDuplicatePatterns@TokenEventGraph[rules,theory,2,"EventDeduplication"->True,"TokenDeduplication"->True,"AllSubsets"->True,GraphLayout"SpringElectricalEmbedding","TokenLabeling"->None],VertexLabelsAutomatic]

Out[]=

In[]:=

Graph[deleteDuplicatePatterns@TokenEventGraph[rules,theory,1,"EventDeduplication"->True,"TokenDeduplication"->True,"AllSubsets"->True,GraphLayout"SpringElectricalEmbedding","TokenLabeling"->None],VertexLabelsAutomatic]

Out[]=

Can the pool of patterns contain patterns that do not assert a truth value?

#### The full pool contains all possible pattern expressions....

The full pool contains all possible pattern expressions....

We look at a certain slice of this pool, and that gives us recognizable math....

### Simple case: single arbitrary axiom

Simple case: single arbitrary axiom

Plus some rules about equality?

#### Enumerations:

all possible initial conditions (i.e. arbitrarily sized pool of patterns) [or could be generated from nothing, by rules]

all possible rules

Enumerations:

all possible initial conditions (i.e. arbitrarily sized pool of patterns) [or could be generated from nothing, by rules]

all possible rules

all possible initial conditions (i.e. arbitrarily sized pool of patterns) [or could be generated from nothing, by rules]

all possible rules

## Metamodels of mathematics

Metamodels of mathematics

#### Possible model: equational axiom systems

Possible model: equational axiom systems

Pure substitution model

The distinguished operator is ==, AKA and ←

? constructivist view: you can only do substitutions at the root ??

Critical pair lemmas require using equality...

## Metamodels

Metamodels

### Case 1:

Case 1:

Expression expression using an axiom

Equational logic:

In here, lhs can be a subpart of expr1

This requires some additional rules for <-> (e.g. the fundamental rule is with , but there is a rule that allows reversal [and the reversal could involve rewriting what is a pattern variable])

### Basic design issue: is there a meaningful notion of a 2-way pattern? [twp]

Basic design issue: is there a meaningful notion of a 2-way pattern? [twp]

Entailment is just: apply a twp to a twp, to get a twp

21

How are variables shared across twps?

The · should be shared. The individual a’s etc. should not.

The goal of the equational theorem prover is to produce TWPs of the form lhs ↔ True

E.g.

There is nothing absolute about True;

cf there is no absolute space....

Everything is defined by relations; even the concept of truth....

cf there is no absolute space....

Everything is defined by relations; even the concept of truth....

(cf category theory)

#### Fundamental assumption: our TWPs are operating on trees/expressions

Fundamental assumption: our TWPs are operating on trees/expressions

This could be modeled with hypergraphs, but that’s lower level.

Hypergraphs may be more convenient for physics; trees for math....

Hypergraphs may be more convenient for physics; trees for math....

#### In physics, we are dealing with pure “relations” i.e. one-level lists....

In physics, we are dealing with pure “relations” i.e. one-level lists....

#### In math, modeling human language, we’re dealing with trees...

In math, modeling human language, we’re dealing with trees...

“Phrase structured math”

## Analog of TWPs for hypergraphs

Analog of TWPs for hypergraphs

With this foliation, it just alternates back and forth:

### What does it look like if there is “learning” in the set of rules?

What does it look like if there is “learning” in the set of rules?

I.e. from a rule we derive another rule, by evolving one of the sides of the rule

This is inducing transitive closure in the transformations between elements

### Encoding with hyperedges...

Encoding with hyperedges...

### Comparison between math and physics:

Comparison between math and physics:

In math, every relation that has been discovered is used any time in the future

In (ordinary) physics, things happen again and again; they are not cached

We can imagine a transitive closure of physics, where anything that has happened is cached; in the ordinary model, only the “underlying rules” are cached

In (ordinary) physics, things happen again and again; they are not cached

We can imagine a transitive closure of physics, where anything that has happened is cached; in the ordinary model, only the “underlying rules” are cached

#### Caching in the ruliad

Caching in the ruliad

The ruliad involves all possible rules. But given a particular point in the ruliad, it takes time to reach other rules, because you have to build them up from your local rules.

#### In the presence of computational irreducibility “it’s already there” is something super-computational

In the presence of computational irreducibility “it’s already there” is something super-computational

And it’s not accessible by a computationally bounded observer

### Difference between math and physics

Difference between math and physics

In physics, we imagine that there are a finite set of underlying rules from which we can derive everything; but ... we could have “cached” higher-level rules

In math, we imagine that there a finite set of axioms from which we can derive everything ... but we like to have higher-level cached lemmas

PCE implies that you can start from essentially any set of rules, in both physics and math. What then matters is the relation of the observer to these rules.

#### Are the observed laws of mathematics based on the observed laws of physics, or vice versa?

Are the observed laws of mathematics based on the observed laws of physics, or vice versa?

### Analogy: given a random UTM, we can make it emulate [whatever we want]

Analogy: given a random UTM, we can make it emulate [whatever we want]

Given a random tree rewriting system ... we can make it emulate some area of math

Axioms and their typical laws of inference are just one possible basis for math; any computational system is also a basis

### Construction of reference frames ↔ what instrumentation is available in science

Construction of reference frames ↔ what instrumentation is available in science

The mathematical interpretation of the advance of instrumentation is different reference frames in the ruliad

#### Axiomatic math will be brittle wrt reference frame; math as practiced by mathematicians will not be

Axiomatic math will be brittle wrt reference frame; math as practiced by mathematicians will not be

## Minimal TWP generator

Minimal TWP generator

#### Case 1: hypergraph-like relations

Case 1: hypergraph-like relations

#### Case 2: tree structures

Case 2: tree structures

### Case 1:

Case 1:

1. In patt1 (lhs1->rhs1) where does lhs2 (from patt2) apply?

Create patt3 from all possible such rule applications

Create patt3 from all possible such rule applications

Are there in fact two kinds of things in math? (a) expressions, and (b) rules? [cf. objects and morphisms] [in type theory: general types ; function types ]

(all of these representations happen to [nowadays] use arrows for the rules/morphisms/functions)

(all of these representations happen to [nowadays] use arrows for the rules/morphisms/functions)

[ We might minimally build up just as category theory does... ]

modus ponens rule....

What we want is a multiway graph whose states are complete lists of TWPs : those states are states of mathematics, with certain proofs made

## Decidability in the bulk limit

Decidability in the bulk limit

There might be things which depend on details at the molecular dynamics level ... but which inevitably come out a certain way for human-like mathematical observers at the bulk scale where mathematicians operate

#### Calculus and continuum structures are used both in physics and in mathematics

Calculus and continuum structures are used both in physics and in mathematics

The continuous description of the mathematical world is like the continuous description of the physical world

Mathematicians think in terms of the continuum; ATPs think in terms of discrete symbolic expressions

## Truth

Truth

“statement” vs “statement is true”

There may be statement which can’t be generated within a certain reference frame, or can’t be seen there

Constructivism : can “statement” be constructed?

### Types of equivalence classes in TEGs

Types of equivalence classes in TEGs

#### Token deduplication

Token deduplication

#### [Event deduplication]

[Event deduplication]

#### States constructed from tokens

States constructed from tokens

#### Foliating events

Foliating events

### Model theory coordinatizes metamathematical space

Model theory coordinatizes metamathematical space

#### For a given model, more than the general theorems will be true (e.g. group theory)

For a given model, more than the general theorems will be true (e.g. group theory)

Certain theorems are true of all groups; more are true for specific groups

I.e there are additional TWPs that will be true if we just construct them with a particular model for the operator

This TWP might be provable from the axioms we’ve chosen...

Or it might just be that a specific model (e.g. finite model) for f (and for a, b etc.) will make it true

Or it might just be that a specific model (e.g. finite model) for f (and for a, b etc.) will make it true

E.g.

Semigroup theory...

But there is a particular multiplication table which is symmetric, and for which

is true..

By using models, we can go faster than the speed of proof.... Because we can immediately reach a TWP that would take many proof steps to reach

E.g. look at TWPs that can be generated by many models; how close is that set to the set that can be generated by proofs?

E.g in Peano arithmetic, look at reverse mathematics and ask what theorems can robustly be generated in many models...

#### Special relativity is a statement about the equivalence of models (?)

Special relativity is a statement about the equivalence of models (?)

## What is the analog of GR in math?

What is the analog of GR in math?

#### ?? the continuum exists

?? the continuum exists

In metamathematics, we’re taking the continuum limit in proof space. How is that related to the continuum limit in “physical” space?

Are these related through the ruliad, and Grothendieck’s hypothesis?

Claim: if we’ve done enough proofs, we’ll start seeing signs of the continuum

If one has enough theorems about integers ... it’ll be like making a statement about reals [???]

### Can we find proof cones in TWP dynamics?

Can we find proof cones in TWP dynamics?

Probably: proof cones will emerge if the entailment rules maintain bounded information content

## Abstraction and equivalence classes created by observers

Abstraction and equivalence classes created by observers