#### Have math statements

Have math statements

All syntactically valid constructs, sometimes repeating atoms (or at least connecting atoms)

#### What is the hypergraph which is the current “math state” of e.g. Metamath?

What is the hypergraph which is the current “math state” of e.g. Metamath?

With Euclid, connected theorems based on their proof dependencies...

Here, want to connect statements based on their structural commonalities

Here, want to connect statements based on their structural commonalities

#### Time in math is what knits the hypergraph together

Time in math is what knits the hypergraph together

Because rules of entailment generate one hypergraph from another, and define light cones

Without time, there would just be an ocean of syntactically correct statements

#### Can we reproduce “2021 Metamath” as “free expansion” of e.g. 1988 Metamath?

Can we reproduce “2021 Metamath” as “free expansion” of e.g. 1988 Metamath?

Not as such. We need to know of the possible

#### There can be many disconnected pieces to metamathematical space

There can be many disconnected pieces to metamathematical space

There are regions connected by time evolution .... which also connect definitions

### Definitions

Definitions

Just names for things... But what a “thing” is, is nontrivial

In an immutable system, “things” are better defined

E.g. in 2+2 = 4, where does the first initial 2 (as a “thing”) go?

## Rules of entailment

Rules of entailment

#### statement1 + statement 2 statement 3 [typical ATP format]

statement1 + statement 2 statement 3 [typical ATP format]

#### statement1 statement 1a ?+ statement 1b

statement1 statement 1a ?+ statement 1b

### When does an equality turn into a transformation?

When does an equality turn into a transformation?

expr1 == expr2

### How are definitions entailed?

How are definitions entailed?

Simplest definitions: names for statements

In[]:=

AxiomaticTheory["RingAxioms"]

Out[]=

a.⊕(b.⊕c.)(a.⊕b.)⊕c.,a.⊕b.b.⊕a.,a.⊕a.,a.⊕,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊗(b.⊗c.)(a.⊗b.)⊗c.,(a.⊕b.)⊗c.a.⊗c.⊕b.⊗c.

∀

{a.,b.,c.}

∀

{a.,b.}

∀

a.

0

∀

a.

a.

0

∀

{a.,b.,c.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

In[]:=

AxiomaticTheory["RingAxioms","Dataset"]

Out[]=

In[]:=

Last/@a.⊕(b.⊕c.)(a.⊕b.)⊕c.,a.⊕b.b.⊕a.,a.⊕a.,a.⊕,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊗(b.⊗c.)(a.⊗b.)⊗c.,(a.⊕b.)⊗c.a.⊗c.⊕b.⊗c.

∀

{a.,b.,c.}

∀

{a.,b.}

∀

a.

0

∀

a.

a.

0

∀

{a.,b.,c.}

∀

{a.,b.,c.}

∀

{a.,b.,c.}

Out[]=

a.⊕(b.⊕c.)(a.⊕b.)⊕c.,a.⊕b.b.⊕a.,a.⊕a.,a.⊕,a.⊗(b.⊕c.)a.⊗b.⊕a.⊗c.,a.⊗(b.⊗c.)(a.⊗b.)⊗c.,(a.⊕b.)⊗c.a.⊗c.⊕b.⊗c.

0

a.

0

In[]:=

ExpressionTree[a.⊕(b.⊕c.)(a.⊕b.)⊕c.]

Out[]=

In[]:=

ExpressionTree/@%79

Out[]=

,

,

,

,

,

,

The function nodes are like tagged atoms of space.... The variable nodes are more like anonymous atoms

### Symbolic equality vs. “action equality”

Symbolic equality vs. “action equality”

Abstract predicates vs. predicates with built-in meanings

### Homotopy type theory

Homotopy type theory

Intensional equality: transitivity etc. ( associativity of equal )

## Empirical Case

Empirical Case

#### Look at complete collection of math statements in the current state of e.g. Metamath library

Look at complete collection of math statements in the current state of e.g. Metamath library

How much of the current state is “syntactically entailed”, with no new definitions

#### E.g. in Boolean algebra

E.g. in Boolean algebra

We can readily enumerate true statements, without having any more definitions

Syntactic possible BA statements:

Out[]//TraditionalForm=

{ab,a(¬a),a(¬b),(¬a)(¬b),a(a∧a),(¬a)(a∧a),a(a∨a),(¬a)(a∨a),(a∧a)(a∨a),a(a∧b),(¬a)(a∧b),(a∧a)(a∧b),(a∨a)(a∧b),a(a∨b),(¬a)(a∨b),(a∧a)(a∨b),(a∨a)(a∨b),(a∧b)(a∨b),(a∧b)(a∧c),(a∨b)(a∧c),(a∧b)(a∨c),(a∨b)(a∨c),a(b∧a),(¬a)(b∧a),(a∧a)(b∧a),(a∨a)(b∧a),(a∧b)(b∧a),(a∨b)(b∧a),a(b∨a),(¬a)(b∨a),(a∧a)(b∨a),(a∨a)(b∨a),(a∧b)(b∨a),(a∨b)(b∨a),a(b∧b),(¬a)(b∧b),(a∧a)(b∧b),(a∨a)(b∧b),(a∧b)(b∧b),(a∨b)(b∧b),a(b∨b),(¬a)(b∨b),(a∧a)(b∨b),(a∨a)(b∨b),(a∧b)(b∨b),(a∨b)(b∨b),a(b∧c),(¬a)(b∧c),(a∧a)(b∧c),(a∨a)(b∧c),(a∧b)(b∧c),(a∨b)(b∧c),a(b∨c),(¬a)(b∨c),(a∧a)(b∨c),(a∨a)(b∨c),(a∧b)(b∨c),(a∨b)(b∨c),(a∧b)(c∧a),(a∨b)(c∧a),(a∧b)(c∨a),(a∨b)(c∨a),(a∧b)(c∧b),(a∨b)(c∧b),(a∧b)(c∨b),(a∨b)(c∨b),(a∧b)(c∧c),(a∨b)(c∧c),(a∧b)(c∨c),(a∨b)(c∨c),a(¬(¬a)),(¬a)(¬(¬a)),(a∧a)(¬(¬a)),(a∨a)(¬(¬a)),(a∧b)(¬(¬a)),(a∨b)(¬(¬a)),a(¬(¬b)),(¬a)(¬(¬b)),(a∧a)(¬(¬b)),(a∨a)(¬(¬b)),(a∧b)(¬(¬b)),(a∨b)(¬(¬b)),(¬(¬a))(¬(¬b)),(a∧b)(¬(¬c)),(a∨b)(¬(¬c)),a(¬a∧a),(¬a)(¬a∧a),(a∧a)(¬a∧a),(a∨a)(¬a∧a),(a∧b)(¬a∧a),(a∨b)(¬a∧a),(¬(¬a))(¬a∧a),a(a∧¬a),(¬a)(a∧¬a),(a∧a)(a∧¬a),(a∨a)(a∧¬a),(a∧b)(a∧¬a),(a∨b)(a∧¬a),(¬(¬a))(a∧¬a),(¬a∧a)(a∧¬a)}

Now, using logic as logic has developed (with its “standard axioms”):

Alternatively, just pick any set of syntactic statements, and start seeing what statements they syntactically entail....

In the entailment rules, a(a∧a) the “a” here is replaced by a unique atom when the entailment transformation is made....

#### The operators (and constants) have persistent names [i.e. definitions]

The operators (and constants) have persistent names [i.e. definitions]

#### <What are the laws of entailment??> [These are the built-in metalogic transformations]

<What are the laws of entailment??> [These are the built-in metalogic transformations]

In the progress of mathematics, one may be continually regenerating “the same” statement ... except that it has different atoms in it (e.g. differently named variables)

Perhaps the operators can evolve, and the perception that the Plus here and there is the same is a matter of observer [+ reference frame]

#### Does the mathematical observer conflate all the 2’s in the universe?

Does the mathematical observer conflate all the 2’s in the universe?

#### Is the entailment basically thinking about every expression as a function

Is the entailment basically thinking about every expression as a function

### What if equality were purely syntactic?

What if equality were purely syntactic?

With certain axioms e.g. a==(b==c) (a==b)==c

#### In the metalogic, transformation is special... [it “just happens” (cf Heraclitus, Leibniz)]

And it is the passage of time (in our perception)

In the metalogic, transformation is special... [it “just happens” (cf Heraclitus, Leibniz)]

And it is the passage of time (in our perception)

And it is the passage of time (in our perception)

Without transformation, all the possible statements are just floating separately. Transformation is what knits them together (entangles them...) ... [[ how important is the role of shared atoms? ]]

In principle, we could tree everything out...

#### In the most simpleminded form, every different derivation of 2+2=4 is a different “state”/statement....

In the most simpleminded form, every different derivation of 2+2=4 is a different “state”/statement....

But .... the first role of the observer is to conflate “relabeling-equivalent” forms

Once the operator is created, it probably just gets “infinitely grandfathered”...

#### How does Plus beget Times?

How does Plus beget Times?

It seems like an observer-determined thing to call this Times[5,a]

#### We can compile everything to very simple “logical atoms” (AKA ruliological atoms)

We can compile everything to very simple “logical atoms” (AKA ruliological atoms)

#### We start just from an abstract binary operator

We start just from an abstract binary operator

Just like variables, this gets transformed to another abstract binary operator....

We also don’t imagine that

constants X and Y

#### Expressions are equivalent to the observer if they have the same “tagged topology”, i.e. variables can be anything, but constants and operators have to “follow the tagging”

Expressions are equivalent to the observer if they have the same “tagged topology”, i.e. variables can be anything, but constants and operators have to “follow the tagging”

“The same operator” might just mean causally connected...

#### Relation between operators and events??

Relation between operators and events??

#### Possible claim: operators are conflated if they are causally connected

Possible claim: operators are conflated if they are causally connected

[To make a new operator, just mine a new part of the ruliad]

#### What we want: make derivations in several toy theories that all involve, say, a single binary operator

What we want: make derivations in several toy theories that all involve, say, a single binary operator

E.g. Nand calculus, semigroup

All these live in the same “operator syntactic space” ... they all involve just a single binary operator

Some wind up being “the same theory”, though differently stated; others are different theories....

Some wind up being “the same theory”, though differently stated; others are different theories....

I.e. these are disconnected when the dynamics is entailment [i.e. there is an event horizon between them]

These are basically “black hole axioms” [i.e. these axioms live in metamathematical black holes]

This has to resolve to an LHS and an RHS.....

[ SMP did not distinguish $x on the LHS from $x on the RHS f[$x] :: $x^2 ]

#### In the ruliad, there is a sea of all possible transformations ... or ... a sea of equality expressions

In the ruliad, there is a sea of all possible transformations ... or ... a sea of equality expressions

Entailment is the application of one equality to another

### The special operators: Equal, Implies [ these connect to the metalogic ]

The special operators: Equal, Implies [ these connect to the metalogic ]

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

## Meta Objectives

Meta Objectives

#### In the physics project, given our human observations of the universe, the goal is to find laws of physics (AKA underlying rules) consistent with those observations

In the physics project, given our human observations of the universe, the goal is to find laws of physics (AKA underlying rules) consistent with those observations

An alien’s observations might lead to different laws of physics [with some rulial motion to translate to ours]

[translation must always be possible, because of PCE]

[translation must always be possible, because of PCE]

#### In the metamathematics project, given our human observations of math (i.e. 3M published theorems), find the laws of mathematics consistent with those observations

In the metamathematics project, given our human observations of math (i.e. 3M published theorems), find the laws of mathematics consistent with those observations

The laws of mathematics could be geometry, or arithmetic etc. You can think about all math in terms of geometry (or in terms of arithmetic) etc. There is a translation between these...

In physics, we only have one physics; in math we have multiple ways to describe to same underlying “Platonic” thing (which is always a slice of the ruliad)

[In physics, we could talk in positions, or in terms of momentum; or use different coordinate systems, canonical coordinates, particle content descriptions, etc.] [ In physics, these correspondences are dualities ]

In physics, we only have one physics; in math we have multiple ways to describe to same underlying “Platonic” thing (which is always a slice of the ruliad)

[In physics, we could talk in positions, or in terms of momentum; or use different coordinate systems, canonical coordinates, particle content descriptions, etc.] [ In physics, these correspondences are dualities ]

#### Category theory interpretation:

Category theory interpretation:

Functoriality is the possibility of motion i.e. homogeneity in [rulial space] metamathematical space

### Time is the source of entanglements/knitting

Time is the source of entanglements/knitting

Without time, everything is dissociated

Feature of physics project: locality in the rules [self evident from finite information in rules]

#### In math, time is entailment, which is also proof

In math, time is entailment, which is also proof

## “Spatial Computation” | Homotopic Computation | Path-to-Path Computation

“Spatial Computation” | Homotopic Computation | Path-to-Path Computation

#### Vs higher categories

Vs higher categories

You deduce “later” states from earlier ones [transformations are applied]

How do we deduce the homotopically equivalent paths? How do we go from path to an equivalent path?

We have to “jump branch pairs”

Which paths can you get between? [Specify the path between paths by giving a list of branch pairs that have to be flipped...]

Where is the first divergence point between different paths? After the divergence point, have to say which way to go at each branch point.

#### What is path-to-path evolution in a TEG?

What is path-to-path evolution in a TEG?

There isn’t an obvious states path...

#### In ordinary time evolution, there is a fixed rule that gets repeatedly applied

(though in the rulial case, there could be a sequence of different rules)

In ordinary time evolution, there is a fixed rule that gets repeatedly applied

(though in the rulial case, there could be a sequence of different rules)

(though in the rulial case, there could be a sequence of different rules)

#### In “sideways” (homotopic) evolution, there are typically different “this event ‘leads to’ this event”

In “sideways” (homotopic) evolution, there are typically different “this event ‘leads to’ this event”

#### Rulially, it’s all the same: because there is a rule that goes sideways...

Rulially, it’s all the same: because there is a rule that goes sideways...

Example: multiway TMs: the sideways rule is not a simple TM

(even though it is computable)

(even though it is computable)

E.g. the translator between P complete (or NP complete) problems

## What is a mathematical observer like?

What is a mathematical observer like?

#### Physical observer:

Physical observer:

Computationally bounded

Sequentializes time

Is subject to pure motion

Sequentializes time

Is subject to pure motion

#### Mathematical observer:

Mathematical observer:

? Univalence axiom :: that which is equivalent is equal

[ There is a single thread of time ]

[ There is a single thread of time ]

I.e. it doesn’t matter which proof path you go on

#### Physical observer coarse grains across threads of time

Physical observer coarse grains across threads of time

#### Mathematical observer coarse grains across proofs [?]

Mathematical observer coarse grains across proofs [?]

Mathematics is built on theorems

(each one can have many different proofs)

Analogy: the building blocks of physical experience are classical observations

(each one can have many different proofs)

Analogy: the building blocks of physical experience are classical observations

#### Parallel transport in proof space

Parallel transport in proof space

If there is confluence, there is no curvature. Slow confluence (or none at all) gives curvature

You see different mathematical sights on these different proof paths

You see different mathematical sights on these different proof paths

If the distance between proof paths exceeds the extent of the observer in proof space, then one will see “metamathematical quantum effects”

What is the analog of virtual particles in proof space?

On two different proof paths, you end up with two incompatible statements for a while .......

## Fluid-level description

Fluid-level description

#### Talk in terms of concepts not instances [“human relatable constructs”]

Talk in terms of concepts not instances [“human relatable constructs”]

I.e. points and lines as concepts, not their “atoms”

#### Non-human-accessible reference frame is one that is shredded by evolution under entailment

Non-human-accessible reference frame is one that is shredded by evolution under entailment

Analogy: a non-thermodynamic coarse graining

#### Concept coarse graining: e.g. the concept of integers

Concept coarse graining: e.g. the concept of integers

Given an intuitive description of the integers, do entailments lead to non-standard messy stuff?

The intuitive description is a coarse graining: under which there many specific instance ... do they all lead to similar coarse-grained results, or not?

Are you inexorably led to large cardinals, etc.?

Can you preserve the coarse graining? [Same as thermodynamics: you can preserve the gas laws, but not some detailed statement about microscopic motions...]

Human mathematics is the stuff you can preserve

Whereas: ATP includes stuff you can’t preserve

Whereas: ATP includes stuff you can’t preserve

## Claim: for any nontrivial axiom system there is a conceptual description that is similar

Claim: for any nontrivial axiom system there is a conceptual description that is similar

The mathematical observer can only handle certain overall concepts, not atomic details ... just as the physical observer can only handle overall features of space, not atomic details

#### Coarse-grained in proof space is the stuff a human mathematician doesn’t need to bother to describe

Coarse-grained in proof space is the stuff a human mathematician doesn’t need to bother to describe

If you as a human make a proof, you just make some somewhat general statement ... you don’t need to atomize it

[E.g. not really understanding the reals]

[E.g. not really understanding the reals]

#### “Human-level math” is like computational language vs. machine code

“Human-level math” is like computational language vs. machine code

CL implements a definite path in machine code .... but it’s “close enough” to our intuitive notion that it’s an OK proxy

A formalized math system should take a human-level description, and give one instantiation of it

[and if it ends up in a different human-level description, that’s “chaos theory in math”]

[and if it ends up in a different human-level description, that’s “chaos theory in math”]

## Undecidability is rare in human-level math...

Undecidability is rare in human-level math...

#### ... because it requires that molecular/quantum effects survive arbitrarily long

... because it requires that molecular/quantum effects survive arbitrarily long

#### We tend to concentrate on math for which we can form a conceptual description

We tend to concentrate on math for which we can form a conceptual description

### Bristle motion in painting vs. formalization in math ?

Bristle motion in painting vs. formalization in math ?

A sufficiently fast and long brush stroke might care about bristle motion...

## Einstein equations / gravity in metamathematics

Einstein equations / gravity in metamathematics

The presence of lots of entailment (AKA energy/mass) lead to focusing of proof paths ... i.e. not wandering as far afield in metamathematical space i.e. sticking closer to the point. Math will be more focused if there’s a higher density of entailments ... i.e. so you can “get back on track” more easily.

Probably number theory is a case where you can wander far afield .... because there are not so many local cross-connections

Universal algebra has more “gravity”, so proof paths stay more concentrated

Eventually there are so many proof paths that it becomes a decidable black hole

Probably number theory is a case where you can wander far afield .... because there are not so many local cross-connections

Universal algebra has more “gravity”, so proof paths stay more concentrated

Eventually there are so many proof paths that it becomes a decidable black hole