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]
<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?
Is the entailment basically thinking about every expression as a function
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)
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....
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?
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 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”
“The same operator” might just mean causally connected...
Relation between operators and events??
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
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....
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
Entailment is the application of one equality to another
The special operators: Equal, Implies [ these connect to the metalogic ]
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]
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 ]
Category theory interpretation:
Functoriality is the possibility of motion i.e. homogeneity in [rulial space] metamathematical space
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]
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?
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 “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...
Example: multiway TMs: the sideways rule is not a simple TM (even though it is computable)
E.g. the translator between P complete (or NP complete) problems
What is a mathematical observer like?
Computationally bounded Sequentializes time Is subject to pure motion
? Univalence axiom :: that which is equivalent is equal [ 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
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
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
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 .......
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
Analogy: a non-thermodynamic coarse graining
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
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
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]
“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”]
Undecidability is rare in human-level math...
... because it requires that molecular/quantum effects survive arbitrarily long
We tend to concentrate on math for which we can form a conceptual description
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
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