Flow of Efforts...

Basic goal: to find a minimal idealization of mathematics + metamathematics that allows us to study it in bulk...

Mathematica + WL provides a good foundational framework
The various efforts of mathematical logic + ATP + proof assistants ... provide other, related frameworks

What is the essence of mathematics?

Assertion of statements as “true” [or at least entailed]
To be compared with physics where when some state is generated, one says that it happens
[ The mathematical observer can only observe something if that thing is present in metamathematical space ]
In the Tarski approach “X” vs X is what the observer “absorbs” vs. what’s actually out there

[Question of “X” vs “X is true”]

https://en.wikipedia.org/wiki/Semantic_theory_of_truth

Fundamental Characterization of Mathematics

Machine-level

[example is some human-level given in proof-assistant form]

Human-level [i.e. observer level]

Claim: to do human-level math you mostly just need human-level math
But ... to do computational paradigm stuff you need the machine level

The Process of Idealization

Empirical version of what human-level math is:
Typical math papers
Math in Mathematica
Euclid
Empirical version of “machine-level” math is:
ATP
Metamath
Proof assistant libraries

The Objects of Mathematics

Basic math representation: symbolic expressions

(which implicitly have pattern variables)
Out[]=

∀
{a.,b.,c.}
a.⊗(b.⊗c.)(a.⊗b.)⊗c.,
∀
a.
a.⊗

1
a.,
∀
a.
a.⊗
a.


1

Out[]=
ImpliesMcCuneAxioms
∀
{a.,b.,c.,d.}
a.⊗
b.⊗(c.⊗
c.
)⊗
d.⊗b.
⊗a.
d.,InverseOfComposite
∀
{a.,b.}
a.⊗b.

b.
⊗
a.
,InverseOfInverse
∀
a.
a.
a.,LeftIdentity
∀
a.

1
⊗a.a.,LeftInverse
∀
a.
a.
⊗a.

1


Expression may be of the form lhs  rhs or they may have other predicates

but in the typical way pure math is represented, the expressions are supposed to have truth values.

This is a special case of computation: the number 3 isn’t a mathematical proposition

First slicing of the “mathematical observer”: consider only expression that have a truth value

I.e. the “raw material” of math is theorems [not e.g. algorithms]

How Can We Idealize the Objects of Mathematics

First level: symbolic expressions with heads, arguments, etc. and pattern variables
[ There are fixed, literal “constants” and/or “named functions” ]
​
Second level: there is nothing intrinsic about the named objects; just use function application for everything .... this is combinators
[ probably with every variable being a pattern variable ] [i.e. no S, K etc.]
How does this compare to hypergraphs? In the math case, we’re imagine that we’re doing transformations on subtrees [i.e. that we have hierarchical structure]
We could represent everything in Polish notation, and have rules that appropriately walk around to emulate subtrees ... but to connect with math it’s easier to use tree structures if we want to connect with standard math notation etc.
Subtrees probably imitate the subtrees of human language (and/or the object/subobject organization that we put on the world)

Exercise: compile S, K combinators to tree substitutions with no variables [S on its own this should be fairly easy]

Claim: Naming is an affordance by the observer ; a name is just a compression of a subtree with some structure

The persistence of a name requires that certain subtrees persist. [E.g. the naming of a hurricane ... it’s realistic to name because it’s persistent ]
If things are “ground up” by entailment, there’s no point in naming them...

Potentially important feature: code = data (AKA you can operate on rules that are themselves used to operate on things)

In physics, we do not imagine that there are “genuine lemmas” that let you jump ahead in the evolution of the universe; these are only in the mind of the observer

Claim: in the end most of the phenomena will be visible in NKS-style “string math”

However, how the higher-level human observer interacts with that is not obvious
I.e. what equivalence classes of strings does the mathematical observer set up ?

The Dynamics of Mathematics

Primary action: proof (AKA entailment)

Typical pattern: given a few “objects”, an infinite collection are entailed

There is a machine-level version of entailment etc. ; there is also a human-level

Machine-level entailment is just (“meaningless”) operations on symbolic expressions

In a first approximation, mathematical observers only care about the objects of mathematics (i.e. mathematical statements)

Each step in a proof takes statements in, and produces entailed statements out....

Non-Cumulative Axiom Based Dynamics

[ “rulocumulative” dynamics ]

The only transformation rules are defined by fixed axioms
Cumulative: additional transformations (i.e. code) are made from data, and can then be applied
Physics is intrinsically non-cumulative, except by virtue of mediation by the observer [who can choose to make certain correspondences]

What Is the Basic Entailment?

I.e. the laws of inference [which are the metalogic of the system]
The most basic is pure substitution
statement/.lhs<->rhs
This is probably all you can do for a general statement that is an arbitrary symbolic expression [this is what WL does, except for the “thermodynamic driving” of  vs  ]
[This is the elementary entailment; notice that it’s the same basic structure as in WPP]

Entailment for rule-like constructs (or logic-like constructs)

a<->b/.lhs<->rhs
Then you can have “mix it up” entailments

Comparison with WPP

statement/.lhs<->rhs
This is a subtree substitution setup
{edge1,edge2,...}/.{edgepatt1,edgepatt2,...}->{newedge1,...}
Compare this with string substitution, CAs, TMs, etc.

The Metamathematical Multiway Graph (AKA Entailment Graph)

In[]:=
NestGraph[Values[substitutionLemmas[#,x_x_[x_]]]&,{x_x_[x_]},3]
Out[]=
In[]:=
NestGraph[Values[substitutionLemmas[#,x_x_[x_]]]&,{x_x_[x_]},3,GraphLayout"LayeredDigraphEmbedding",AspectRatio1/2]
Out[]=
In[]:=
VertexList[%161]
Out[]=
{x_x_[x_],x_x_,x_x_[x_[x_]],x_x_[x_][x_[x_]],x_[x_]x_[x_],x_[x_]x_,x_x_[x_[x_[x_]]],x_x_[x_[x_][x_[x_]]],x_x_[x_[x_]][x_[x_[x_]]],x_[x_]x_[x_[x_]],x_x_[x_][x_],x_x_[x_][x_[x_[x_]]],x_x_[x_][x_[x_][x_[x_]]],x_x_[x_][x_[x_]][x_[x_][x_[x_]]],x_[x_]x_[x_][x_[x_]],x_[x_[x_]]x_[x_],x_[x_][x_[x_]]x_[x_],x_x_[x_[x_[x_[x_]]]],x_x_[x_[x_[x_][x_[x_]]]],x_x_[x_[x_[x_]][x_[x_[x_]]]],x_x_[x_[x_[x_]]][x_[x_[x_[x_]]]],x_[x_]x_[x_[x_[x_]]],x_x_[x_[x_][x_]],x_x_[x_[x_][x_[x_[x_]]]],x_x_[x_[x_][x_[x_][x_[x_]]]],x_x_[x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_x_[x_[x_][x_[x_]]][x_[x_[x_][x_[x_]]]],x_[x_]x_[x_[x_][x_[x_]]],x_x_[x_][x_][x_[x_][x_]],x_[x_]x_[x_][x_],x_x_[x_][x_[x_[x_[x_]]]],x_x_[x_][x_[x_[x_][x_[x_]]]],x_x_[x_][x_[x_[x_]][x_[x_[x_]]]],x_x_[x_][x_[x_[x_]]][x_[x_][x_[x_[x_]]]],x_[x_]x_[x_][x_[x_[x_]]],x_x_[x_][x_[x_][x_]],x_x_[x_][x_[x_][x_[x_[x_]]]],x_x_[x_][x_[x_][x_[x_][x_[x_]]]],x_x_[x_][x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_x_[x_][x_[x_][x_[x_]]][x_[x_][x_[x_][x_[x_]]]],x_[x_]x_[x_][x_[x_][x_[x_]]],x_x_[x_[x_]][x_[x_]],x_x_[x_[x_]][x_[x_[x_[x_]]]],x_x_[x_[x_]][x_[x_[x_][x_[x_]]]],x_x_[x_[x_]][x_[x_[x_]][x_[x_[x_]]]],x_x_[x_[x_]][x_[x_[x_]]][x_[x_[x_]][x_[x_[x_]]]],x_[x_]x_[x_[x_]][x_[x_[x_]]],x_x_[x_][x_[x_]][x_[x_]],x_x_[x_][x_[x_]][x_[x_][x_]],x_x_[x_][x_[x_]][x_[x_][x_[x_[x_]]]],x_x_[x_][x_[x_]][x_[x_][x_[x_][x_[x_]]]],x_x_[x_][x_[x_]][x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_x_[x_][x_[x_]][x_[x_][x_[x_]]][x_[x_][x_[x_]][x_[x_][x_[x_]]]],x_[x_]x_[x_][x_[x_]][x_[x_][x_[x_]]],x_[x_[x_]]x_,x_[x_][x_[x_]]x_,x_[x_[x_]]x_[x_[x_]],x_[x_][x_[x_]]x_[x_[x_]],x_[x_[x_]]x_[x_][x_[x_]],x_[x_][x_[x_]]x_[x_][x_[x_]],x_[x_[x_[x_]]]x_[x_],x_[x_[x_][x_[x_]]]x_[x_],x_[x_[x_]][x_[x_[x_]]]x_[x_],x_[x_][x_]x_[x_],x_[x_][x_[x_[x_]]]x_[x_],x_[x_][x_[x_][x_[x_]]]x_[x_],x_[x_][x_[x_]][x_[x_][x_[x_]]]x_[x_]}
[bug:]
Given this mathematical setup, these are entailed statements...
Can we identify “named subtrees” that help us understand what’s going on?
Eventually, all “true” / entailed statements (presumably) show up ... though there’s no guarantee how many steps it will take....

How quickly are the true statements generated?

Number trees based on this sequence:
[[ Probably a better approach is to treat each tree in terms of a binary digit sequence ]]
​

Is the proof graph confluent? [I.e. if you wait long enough you’ll always prove your favorite theorem, whatever path you take]

Alternative is that it might have event horizons.... Or it might just be too tree-like ....

Can X be Proved?

Straightforward approach: just find X in the full multiway proof graph

The proof from the original axioms is then the path (or tree) that gets you to the required X
[ It can be a tree if one starts from more than one axiom ]

Alternative: given a set of asserted theorems (AKA axioms) can one reach X in the forward entailment cone of those theorems?

It could in principle be reachable, but only by an arbitrarily long path ... hence undecidability

This approach to proof/truth is: if it’s produced, it’s “true”

This is essentially constructive mathematics .... The notion that there is a “false” version of a statement that can be derived from the true version doesn’t really enter here
(In usual logic, it’s straightforward to negate a statement; here it is not. Given a “true” statement, there is no guarantee of exhibiting a corresponding false statement)

ATP

Makes direct use of the concept of a “True”
Assume that something “self evident” is True, e.g. x == x
(If our only operators are composition and equality, the way we represent “True” is with x==x )
Our goal in ATP is to take axioms+hypothesis and derive True
This would imply that hypothesis is equivalent to True
(In a non-cumulative setup, you would just have a path graph that keeps on applying different axioms at each step...)
It’s a more complicated tree if it’s rulocumulative

Can we flatten the graph from FindEquationalProof to a non-rulocumulative form?

Partial rulocumulativity

One possibility: every time you’ve derived a new  result, always use it
Other possibility: just pick a few  results, and use them

Causal Graphs

These help track the fate of named objects ... because they show us how fragments of states get passed through

The evolution graph ignores what’s “merely a spectator” and treats everything as being “involved”

Potential Difference Between Math and Physics

In math, we are always looking at large swaths of branchial space

As math evolves, we as observers are more spread out in branchial space; our near-term future entailment cone is bigger

Motion in metamathematical/branchial space: exploring more math [charting the unknown in math]

Time computational activity; in mathematics entailment is always “there to happen” ... but we may or may not choose to “make it happen” as observers. In physics, evolution is there to happen, but we may or may not choose foliations where it does

In both cases, it is the perception of the observer that “causes” time to be perceived as passing

Different proof paths can involve quite different areas of mathematics, or similar ones

I.e. to get to a certain statement, it could just be a bundle of nearby paths, or there could be homotopically distinct bundles
Is the proof continuously deformable at all stages, or is there an obstruction?

“Pure motion” in branchial space is about transporting a cluster of results in one area of math to another [i.e. the functor story]

Model Theory

Let’s imagine that we can define a “numeraire” for every statement
Given a model, both might turn into numbers ... and then there might be a result that every deduction must be a larger number
In x  x[x] our “numeraire” is just the size of the tree. Now we have a result that says we can only get bigger trees...
This type of model is like a foliation....

Models break all possible expressions into equivalence classes, thereby defining which ones can be equal

(They can overdo it, like hash codes)

What is the relation between a model and what an observer observes with coarse graining?

For the integers, the model of Peano arithmetic that is the ordinary integers is effectively a coarse graining of the full symbolic representation of Peano arithmetic [?]
For group theory, we have abstract results about groups ;; but we can take a specific groups as our model, and doing that does lots of coarse graining and makes many equivalences that wouldn’t otherwise be there, be there....

How do we go from pure group theory, to the theory of a specific group?

The proof graph of
will give all the true statements of abstract group theory, with no additional relations (i.e statements that are true in particular for the free group)
When we add in the relations for a particular group [i.e. we add them as axioms], we will get more true statements ... and we get more relations (which are true statements)
To have a valid group, the defining relations must be consistent with the general properties of a group .... i.e. they produce extra connections in the proof graph
BUT they can never generate a node that was not present before... [except if the system is cumulative, then those extra edges can be turned into nodes]

Normally making it a specific group adds edges which effectively put existing nodes together

[Lawvere’s model theory]

Relation to Formalized Math

[ Analogy: We have empirical data about gravity between the Earth and the Moon ..... how can we use this to know about what happens with the atoms of space? ]

A piece of branchial space [for Euclid]

Proof graph for Euclid

What are the entailments here?
Volume of past entailment cone for each theorem:

[Transitive reduction of proof graph is the always-leading-edge way of exploring math]

Euclid all theorems:

Emergent axioms of Boolean algebra:

If you add a new statement to the proof graph, it’ll have an entailment cone, and the overall graph will be bushier

There are presumably many statements that we would call the Pythagorean theorem, but they are different in metamath...

Depending on curvature in proof space ... there may be some separation or not of the geodesics

Which Features Are Essential for a Human Mathematical Observer?

Tree-iness

Cumulative-ness / code = data

Or ... is a string multiway system a good model?

If we want to preserve the “humanizability of mathematics”, we probably have to assume certain axioms

Right now, it may be fine to assume CH is true or is false ... but the “wrong” assumption will lead to non-humanizable math [e.g. math that shreds to the molecular level ... so that it’s full of undecidability] [CH is like an investment, and we’re long in CH now....]

How many elements are there in human-interesting metamathematical proof graphs?

How does it compare to the elements in the universe? [Given that in math we have a systematic way to use reducibility]

Relativity for Metamathematics

It doesn’t matter in what order you prove the theorems, you can always get to the same math in the end

There are many foliations of proof space; they are all ultimately equivalent

[ We need to find a case where time stops ... no further entailments ]

The fact that there are always more theorems to prove (at least at the machine level) speaks to the endless frontier of math
Could it be that there are no more human-level theorems to prove? No: because in metamathematics there is inevitable GR
For fundamental multicomputational reasons, the structure of proof space can’t just shred [~ 2nd Law etc. have to keep on holding]

Future of math could be ruliology .. except that it has a different aesthetic ... which is a human-derived aesthetic, which doesn’t match the machine-level approach

~ machine learning takes over science ... with models we can never understand

Structure of Bulk Metamathematics

BA axiom is out in the wilderness of proof space ... without any continuum connection

Human mathematical observer ... extended in branchial space

Therefore conflates theorems that are trivially lemma-related to each other....
I.e. you have a theorem, and then you a halo of trivially related other theorems

Main multicomputational fact: a mathematical observer extended in branchial space can be persistent, and not be shredded

This is why human-level mathematics is possible.....
[But human-level ruliology may not be possible]
This why you don’t fall into ATPs immediately ... and people have been able to do math...

Representation of Higher-Level Math

We don’t go all the way to the formal bedrock ... because if we did it become incomprehensible
Going all the way to the bedrock is like shredding things. It’s not self-evident that you can jump between high-level representations .... you might have to go to the bedrock to say what’s happening
Rather than making a broad brush stroke statement .... it might shatter into pixie dust
[Does it shatter like the Cantor set...]
Can one preserve the continuum or not?
What is the metamathematical analog: i.e. as you iterate in proof space, the difference between nearby axioms/assumptions/... doesn’t have a big effect ..... vs. it gets shredded.
It doesn’t get shredded if you have the right kind of “observer equivalence class” ; we as physical observers have that, and we can grandfather that into mathematics....
[ But if we pick a weird observer equivalence class, it might get shredded ]

Proof Graph vs. All Syntactically Possible Statements

The proof graph lives in a ocean of syntactically possible statements; many of them it never reaches

If there is a definition of negation, we could check it never reaches both a statement and its negation

Continuum for Observers and for Math

A persistent observer necessarily believes in the continuum

What is the relationship between this and the continuum inside mathematics?

When the observer makes a model of mathematics, do they introduce the continuum?

Humans assume some degree of continuity

The nontrivial fact is that that is consistent with the proof / entailment evolution ... and that what was a little region of continuity doesn’t get shredded
I.e. that the concept of a point, for example, is persistent

Invention vs. Discovery for Math

It’s discovery in the sense that the ruliad is all out there....
It’s “invention” in the sense that it’s our fate what to observe, based on the history of our biology, culture, etc.
[In the sense that it depends on our mathematical technology, it’s invented]
Cumulative buildup: like self-invention of math
Discovered in the same sense that we discover aspects of the physical universe (“find the source of the Nile”)
There are only certain aspects of the physical universe that we sense ;; we are responsible (at some level) for what we can sense
We invent tech for observing the universe: microscope, telescope, amplifier, ...
We invent tech for observing the mathematical world : e.g. WL [visualization allow you to humanize what you couldn’t otherwise]

We notice pieces of the ruliad that have to do with things like arithmetic and geometry ... and that are modelable/interpretable/observable in those terms

These come from directly leveraging our physical existence and our physical observer status

How far in rulial space have mathematicians managed to go away from our physical observations : i.e. how alien are mathematicians?

Have mathematicians been the most distant travelers in rulial space?

If a mathematician is far away in rulial space ... there’s a reason why nobody cares

Because nobody shares that worldview...

[Physical observations are our common experience]

In the future UIs are also common experience [[ e.g. hyperlinks are common experience ]]
< Networks became understood >

The Continuum Hypothesis

Qualitative idea: if there is an intermediate set, then this is something that the proof process could lead you into ... but if there is no such set, then the proof process can’t leak into the weirdness of the intermediate case ... and it’s always just integers or reals....
(Possibly related to intermediate degrees)

Does falsity of the continuum hypothesis imply that you could be in the hyperruliad?

Is CH findable in the ruliad, or do you have to go to the hyperruliad?

[[It’s a question of what you “notice”]]

[[If you don’t notice anything intermediate between integers and reals]]

Math Genealogy vs Branchial Space

Genealogical graph of mathematicians is also a multiway graph
Natural foliation of that multiway graph is physical time

Citation network of mathematics will be similar

[ Bibliometric graph ]