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