#### Basically looking at tree replacements of a certain type

Basically looking at tree replacements of a certain type

## Enumerating Possible Axiom Systems

Enumerating Possible Axiom Systems

First, consider cases where we have identified the operators [we can also consider cases where we’ve identified constants (i.e. arity-0 operators) ]

### Single binary operator

Single binary operator

With pure substitution, and initial conditions that are self application onto the axiom, do we generate exactly the “true” theorems here:

In[]:=

#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2]

Out[]=

{(a_·b_)·b_a_,a_·(b_·b_)a_}

In[]:=

ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{#},2,"TokenLabeling"->False,"TokenMultiplicity"->Automatic,AspectRatio->1]&/@(#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2])

Out[]=

,

In[]:=

(Cases[VertexList[#],_TwoWayRule]/.p_Pattern:>First[p])&/@%

In[]:=

ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{#},1,"TokenLabeling"->True,"TokenMultiplicity"->Automatic,AspectRatio->1]&/@(#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2])

Out[]=

,

In[]:=

findTree[patt_TwoWayRule]:=(UndirectedGraph[TreeGraph[ExpressionTree[#,TreeElementLabel->(All->None),TreeElementStyle->(All->Tiny)]],ImageSize->Tiny]&/@(patt/.p_Pattern:>First[p]))

#### [[[ Tree rendering : ]]]

[[[ Tree rendering : ]]]

In[]:=

TWPTreeGraph[patt_TwoWayRule,opts___]:=With[{g=TreeGraph[ExpressionTree[(#)]],vars=Union[Level[#,{-1}]]},Graph[treeLayout[EdgeList[g]],opts,VertexStyle->(#->If[MemberQ[vars,First[#]],ColorData[10][First@FirstPosition[vars,First[#]]],Gray]&/@VertexList[g])]]&/@(patt/.p_Pattern:>First[p])

In[]:=

treeLayout[g_]:=Graph[g,VertexCoordinates->Thread[VertexList@g->GraphEmbedding@GraphTree@g]]

In[]:=

%518[[1,11]]

In[]:=

UndirectedGraph[TreeGraph[ExpressionTree[#,TreeElementLabel->(All->None),TreeElementStyle->(All->Tiny)]]]&/@(((((((a·b)·b)·c)·d)·d)·e)·ef)

Out[]=

In[]:=

(Map[findTree,Cases[VertexList[#],_TwoWayRule]&@ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{#},1,"TokenLabeling"->False,"TokenMultiplicity"->Automatic,AspectRatio->1]]&)/@(#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2])

Out[]=

,

,

,

,

,

,

,

,

,

,

,

,

,

The a, b etc. should be shown as different colors of leaves

#### Even tinier axiom systems:

Even tinier axiom systems:

## Enumeration of possible axiom systems

Enumeration of possible axiom systems

These are all identical because the “a” must be inserted in the same number of places on the LHS:

Are there clusters of nodes here that would be “named the same theorem”

# Interpretation

Interpretation

#### Spacelike separated tokens can coexist in a particular branch of mathematical history

Spacelike separated tokens can coexist in a particular branch of mathematical history

#### Entailment/derivation cone of a statement is everything that can be derived just from that statement

Entailment/derivation cone of a statement is everything that can be derived just from that statement

E.g. for Euclid we have plots of what gets entailed from each of the axioms

E.g. in group theory we can have entailments (i.e. statements) from the general group axioms ... then we’ll have more entailments if we add the specific relations of a group

#### “Point to point geodesic”: there is a single statement that leads to another statement

“Point to point geodesic”: there is a single statement that leads to another statement

Many proofs may take multiple “input points” (i.e. axioms) to derive a single statement

In ATP one normally adds in the potential theorem, and sees if one can derive a tautology [[[ this has to do with using completions to make the path finding simpler ]]]

#### Is there confluence in these TEGs?

Is there confluence in these TEGs?

#### What are the reference frames of mathematical development?

What are the reference frames of mathematical development?

These contain statements that are “instantaneously independent” (?)

#### How are statements laid out branchially in these slices?

How are statements laid out branchially in these slices?

When statements are far apart, this means that to derive one from the other will take awhile...

### What does it look like when the theory is decidable?

What does it look like when the theory is decidable?

### How do models (as in model theory) relate to all of this?

How do models (as in model theory) relate to all of this?

### What does the presence of infinite paths mean? [Basically computational irreducibility]

What does the presence of infinite paths mean? [Basically computational irreducibility]

### Notion of “truth”:

Notion of “truth”:

Find a statement that you think is “obviously true” e.g. a == a

Now look for all statements that are connected to this; these are the true statements

Now look for all statements that are connected to this; these are the true statements

[True as in a==a has an entailment cone]

[But if there are other “obviously true” statements, they could have their own entailment]

[But if there are other “obviously true” statements, they could have their own entailment]

#### Notion of falsity

Notion of falsity

This is harder to define. Perhaps a_ == b_

## “Physicalized Interpretation”

“Physicalized Interpretation”

#### Proof structure knits together metamathematical space

Proof structure knits together metamathematical space

#### What is metamathematical energy? Metamathematical gravity?

What is metamathematical energy? Metamathematical gravity?

Density of activity in regions of metamathematical space

#### Singularity theorems if there is enough proof density, the theory will eventually be decidable

Singularity theorems if there is enough proof density, the theory will eventually be decidable

[ So presumably this means there are no more new theorems produced ]

#### Infinite future of math: expansion of the metamathematical universe, together with a bunch of black holes being formed

Infinite future of math: expansion of the metamathematical universe, together with a bunch of black holes being formed

Future entailment cone of the Peano axioms will still be infinite ... but there will be lots of “burned out” subcases left behind

# Model Theory

Model Theory

If there is a model of · , then for every of the k choices of each variable, the LHS and RHS will be the same...

So any given statement has essentially a barcode of what values its two sides can take on......

The model defines equivalences between expressions.... Which means that in the proof graph there is an overlay for a given model that connects things equivalent in that model...

#### ?? Finding a model is like a finding a valid foliation ??

?? Finding a model is like a finding a valid foliation ??

Actually more like find an “observer sampling”

#### You can get proof results that are equivalent to model results by adding enough relations

You can get proof results that are equivalent to model results by adding enough relations

#### Given a model, there is a definite representation for a==a ;

Given a model, there is a definite representation for a==a ;

#### ... so all tautologies [under the model] can be “painted” by seeing whether they have the same “bar code” as a==a

... so all tautologies [under the model] can be “painted” by seeing whether they have the same “bar code” as a==a

#### Assume that from an axiom A one can derive a theorem S. A model will give a “barcode” for LHS[A] and LHS[S]. The fact that S can be derived from A .... what does it say about the bar codes ???

Assume that from an axiom A one can derive a theorem S. A model will give a “barcode” for LHS[A] and LHS[S]. The fact that S can be derived from A .... what does it say about the bar codes ???

## Enumerating values of expressions for a particular model

Enumerating values of expressions for a particular model

So therefore the model is establishing a relation that cannot be derived proof theoretically.....

#### “Model values” are like hash codes: they are unequal, then the statements can’t follow from each other; but if they are equal, that might just be a “coincidence”/”hash collision” and have nothing to do getting from one to the other by a proof

“Model values” are like hash codes: they are unequal, then the statements can’t follow from each other; but if they are equal, that might just be a “coincidence”/”hash collision” and have nothing to do getting from one to the other by a proof

If the “model codes” are equal, one form of proof (e.g, substitution) might not connect them, but another (e.g. cosubstitution) might do it....