Metamodel of mathematics

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)

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

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,lhsEvaluate[rhs/.(Verbatim[#1]First[#1]&)/@Cases[lhs,_Pattern,All,HeadsTrue]]]}}
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],VertexLabelsAutomatic]
Out[]=
In[]:=
Graph[deleteDuplicatePatterns@TokenEventGraph[rules,theory,1,"EventDeduplication"->True,"TokenDeduplication"->True,"AllSubsets"->True,GraphLayout"SpringElectricalEmbedding","TokenLabeling"->None],VertexLabelsAutomatic]
Out[]=
Can the pool of patterns contain patterns that do not assert a truth value?

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

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

Metamodels of mathematics

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

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]

Entailment is just: apply a twp to a twp, to get a twp
21
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 category theory)

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....

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

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

“Phrase structured math”

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?

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...

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

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

And it’s not accessible by a computationally bounded observer

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?

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

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

Minimal TWP generator

Case 1: hypergraph-like relations

Case 2: tree structures

Case 1:

1. In patt1 (lhs1->rhs1) where does lhs2 (from patt2) apply?
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)
[ 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

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

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

“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

Token deduplication

[Event deduplication]

States constructed from tokens

Foliating events

Model theory coordinatizes metamathematical space

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
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 (?)

What is the analog of GR in math?

?? 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?

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

Abstraction and equivalence classes created by observers