The Univalence Axiom (in WPP): Foliations, fibrations and completions are equivalent.
“Multiway Invariance”: the induced multiway systems for each timelike path are all isomorphic as DAGs => justification for “collapsing” spacetime down to a single timelike path (since they are all observationally equivalent).
[[Consider an EPR pair. If they are spatially separated, and we want to measure the combined quantum state of that system, we implicitly perform a spatial completion (inducing “branchially local” multiway invariance).]]
“Extensionality” (in general): “StateEquivalenceFunction” in general mathematics. “Axiom of Extensionality”: consider two sets equivalent if they contain the same elements. “Propositional Extensionality”: consider propositions A and B as equivalent if A<->B. “(Homotopy) Type Extensionality”: consider paths to be the same if they are homotopy-equivalent.
Consider an AI who doesn’t see definite things happening (in which there is no invariant causal partial order)...
Let’s define cosmological rest frame as being the “free model”; define inertial reference frames as being “free models + one additional relation”. Analogy to spacetime: it requires a single additional equivalence (beyond the causal partial order defined by the conformal structure of spacetime) between spacelike-separated events in order to define a global inertial frame.
The free group is purely quantum mechanical; the maximally non-free group (i.e. in which all possible relations/completion rules have been applied) is purely classical. All “ordinary” groups lie somewhere on the quantum-classical spectrum.
In GR it takes irreducible computational effort to determine that the points in your claimed spacelike hypersurface are indeed consistent with the causal partial order. The steeper your foliation angle, the more such points one must verify, etc...
(There exists a natural “internal” coordinatization of expressions in the proof network in terms of part specifications...)
Consider axioms as defining a set of basis vectors for a Hilbert space. Then proof-theoretic independence of statements becomes linear independence of vectors, etc. Therefore, a natural coordinatization is given in terms of the number of necessary applications of a given axiom (or intermediate lemma) in the derivation of a subsequent lemma (i.e. the coefficients of a linear combination). [[This is an invariant prooftime interval.]]
As the technical sophistication of mathematics increases (AKA more theorems known), a generalized graduate student who is prepared to take these theorems “on faith” can proceed more quickly. But the task of formalizing all of mathematics gets more complicated (as a tradeoff).
Each new relation is defining an equivalence between a pair of proof-theoretically independent terms (which defines a hyperplane).
Considering its normal gives a unit normal direction to some hypersurface.
Each relation adds a new unit normal direction to a prooflike hypersurface.
In ordinary relativity, consider constructing a spacetime foliation while only having access to a discrete set of events (with a “time tag”), with respect to which to do pairwise synchronization.
Imagine a discrete collection of clocks, extended in time, and take a discrete set of slices through these timelike-extended paths. What you obtain is a discrete set of events with “time tags” from the clocks. This allows us to do a discrete approximation to standard relativistic synchronization in the configuration of spacetime foliations.
(Simultaneities of spacelike-separated events can be represented as sets of spacelike vectors...)
The Axiom of Choice permits nonconstructive proofs (and is therefore described as a “nonconstructive axiom”), and in particular, permits proofs of propositions that would be undecidable by any constructive means.
Interpreted as a basis vector on proof space, the AoC defines a family of necessarily lightlike paths.
At a (conventional relativistic) event horizon, light cones tip over such that to remain at the boundary would require following a lightlike curve. The event horizon is a family of paths that are consistent with the causal partial order, but cannot be followed by any subliminal observer.
Likewise (claim) the AoC defines a family of (lightlike) paths that are consistent with the causal partial order (e.g. defined by ZF), but cannot be followed by any “subluminal” model, i.e. any constructive model corresponding to a computationally-bounded mathematician.
Suppose you wanted to prove the proposition that one term on an event horizon implies another term on the same event horizon. Such a proof is necessarily nonconstructive. (i.e. the theorem can be proved syntactically by following an explicit lightlike path in the multiway system, but no model lying on the interior of its own proof cones could explicitly witness this proof.)
Relationship to the Morley categoricity theorem (regarding axiom systems that define unique models up to isomorphism): you can have a theory that defines some infinite model, and you can prove that this infinite model is unique up to isomorphism (in some cases). Why are the real numbers so annoying to work with, and the complex number so beautiful? The real numbers, as a dense linear order, are far from being unique. Whereas, the complex numbers are unique (up to isomorphism) as a closed algebraic field of characteristic zero (as guaranteed by Morley categoricity). Lowenheim-Skolem theorem: if you have a finite collection of sentences with a model of size some infinite cardinality, it will have a model of size k for any infinite cardinal k.
Positive curvature increases proof redundancy; negative curvature increases theorem diversity, i.e. number of distinct equalities (decreases proof redundancy). E.g. the fundamental theorem of algebra is probably a high positive curvature region of metamathematical space (since there are many diverse and apparently inequivalent proofs of the same proposition).
“Surprising theorem”: (conjecture) a relatively short path connecting apparently distant points in metamathematical space.
Existence of the Universe (Axiomatic Independence Of)
Is there a proof based on formal axiomatic transformation that the universe must exist?
[[[You give me an argument of the form “X implies that the universe exists.” (any such proof would necessarily have this form).]]]]
These axioms imply that a structure, called U, necessarily exists. Is U isomorphic to the physical Universe?
Axiom of Extensionality for Universes: Two universes are isomorphic if and only if every physical system inside them is identical.
[[[There is a Universe out there, and there is “the universe” referenced in your argument (which is a model of the actual physical Universe); how can I confirm that they are isomorphic?]]]
In other words, validating your argument is a problem of model-verification (confirming that U == “Universe”).
Consider second incompleteness theorem (consistency of Peano arithmetic is independent of Peano arithmetic): to prove consistency of PA would require enumerating all syntactically provable propositions in PA and demonstrating that there are no contradictions, but by first incompleteness theorem, no such enumeration exists.
Analog of first incompleteness theorem for physics: We can construct a physical Godel sentence by building a physical computer whose program says “If the rule for the universe predicts that this program will do X, then do Y, otherwise do X.” <=> Computational universality prevents us from computing features of the universe faster than the universe itself evolves.
Proving that U == “Universe” requires enumerating all physical systems entailed by U and demonstrating that this set is in one-to-one correspondence with the set of physical systems in “Universe”. (but physical incompleteness tells us that no such enumeration can be made...)
=> Kant was right all along (physical existence is an axiomatically undecidable predicate)
Philosophy of Mathematics
Constructivism, finitism (rejects infinite mathematical structures), ultrafinitism (rejects unfeasibly/unphysically large but finite mathematical structures), etc...
[[Finite groups require the convergence of distinct geodesics in the associated free group (and hence are associated with positive curvature). [More mass implies more curvature.]
Relations collapse branches (e.g. with sufficient collapsing, the free group becomes a finite group).]]
Is there a correspondence to the hierarchy of causality conditions in GR?
A theorem with only non-constructive proofs: a certain digit occurs infinitely often in the decimal expansion of Omega.
Realizability/BHK interpretation: talk to the Bauer.
Generalized Einstein equations: The higher the level of mathematical knowledge, the greater the proof redundancy (positive curvature).
The Axiom of Choice is “too powerful”: it produces so much mathematical knowledge, and induces so much proof convergence/redundancy. There’s a growth rate of mathematical knowledge, and there’s a growth rate of constructive proofs; the AoC is powerful enough that it boosts the growth rate of mathematical knowledge so much that the growth rate of constructive proofs cannot catch up.
AoC is adding “tame hypercomputation”.
With AoC, for each critical pair you force to converge, you get more (i.e. no finite completion), i.e. model construction is non-computable.
AoC is “maximally non-causal invariant” (i.e. no finite completion procedure).
If there is a finite completion procedure, K-B terminates, so word problem decidable. => (contrapositive) word problem undecidable implies no finite completion procedure.
Conjecture: Related to asymptotic dimension stability in GR?? (which is a constraint on “causal graph branchiness”...) I.e. satisfaction of the generalized Einstein equations <=> constructivism.
Intuitionism (a brand of constructivism) permits the principle of explosion (“ex falsus sequitur quodlibet”; if you have one contradiction you have infinitely many), whereas other constructivist mathematicses do not permit it.
With this formalism, we can construct a fine-grained hierarchy of constructivism, both in terms of computability and computational complexity of the associated models.
Implications for Aliens
The rulial multiway system is the ultimate Voyager golden disc (universal physics/universal mathematics).
Is Shinichi Mochizuki an alien? (Inter-Universal Teichmuller Theory)
(IUTeich allows you to define Teichmuller theory over arbitrary number fields equipped with an elliptic curve.)
IUTeich: suppose you have a number field equipped with an elliptic curve (a “mathematical universe”). Now, deform the multiplication operation for this ring structure, to obtain a “deformed” universe. IUTeich gives an explicit algorithm for computing the resultant effect on the addition operation.
(Using “log-links” and “theta-links” between (“Hodge theatres” within) “universes”)
(Conjecture: IUTeich offers one possible parametrization of the effect of continuous deformations on rulial space?)
ABC conjecture: it gives a nontrivial connection between addition and multiplication (why it’s interesting number-theoretically).
Each theory is a rulial fibre; the rulial multiway system induces a natural geometry on fibres, and hence on theories.
Curry-Howard-Lambek extends Curry-Howard to the case of closed Cartesian categories.
Grothendieck’s hypothesis as a definition of topology: topological spaces are infinity groupoids (by definition).