Formal Correspondences between Homotopy Type Theory and the Wolfram Model

This bulletin is a writeup of work done in collaboration with Xerxes Arsiwalla and Stephen Wolfram, as publicly presented and discussed in livestreams here, here and here. This bulletin is intended to be a high-level survey of the effort so far; a more formal article, intended to give rigorous formulations and proofs of the various ideas discussed here, is currently in preparation for submission to an appropriate journal.

Introduction

The field of “metamathematics”—a term first popularized by David Hilbert in the context of Hilbert’s program to clarify the foundations of mathematics in the early 20th century—may ultimately be regarded as the study of “pre-mathematics”. In other words, while mathematics studies what the properties of particular mathematical structures (such as groups, rings, fields, topological spaces, etc.) may be, metamathematics studies what the properties of mathematics itself, when regarded as a mathematical structure in its own right, are. Metamathematics is thus “pre”-mathematics in the sense that it is the structure from which the structure of mathematics itself develops (much like “pre-geometry” in theoretical cosmology is regarded as the structure from which the structure of the universe itself develops).

In much the same way, the Wolfram Physics Project may be thought of as being the study of “pre-physics”. The Wolfram model is not a model for fundamental physics in and of itself, but rather an infinite family of models (or, if you prefer, a “formalism”), within which concepts and theories of fundamental physics can be systematically investigated and validated. However, one of the most remarkable things that we have discovered over the year or so that we’ve been working on this project is that a shockingly high proportion of the known laws of physics (most notably, both general relativity and quantum mechanics) appear to be highly “generic” features of the formalism, i.e. they are exhibited by a wide class of models, as opposed to being features that are somehow peculiar to our specific universe, as one might otherwise expect. This leads us to the tantalizing possibility that, just as metamathematics aims to explain why mathematics has the structure that it does, the Wolfram model may serve to explain why physics has the structure that it does.

The correspondence between the Wolfram model and foundational metamathematics goes far deeper than this, though. It does indeed appear that many of the recent innovations in the foundations of mathematics (including dependent type theory, homotopy type theory, the univalence axiom, Urs Schreiber’s cohesive geometry, etc.) have considerable overlaps with our recent insights into the foundations of physics (particularly surrounding concepts such as the topology and geometry of rulial space, foliations and fibrations of the rulial multiway system, completion procedures and the inevitability of quantum mechanics, etc.). Indeed, what I aim to sketch out in this bulletin is a potential scheme for a new, computable foundation of both mathematics and physics, which can be thought of as an abstract unification of homotopy type theory and the Wolfram Physics Project.

I will discuss how the symbolic structure of the Wolfram Language’s automated theorem-proving framework reflects the Curry–Howard–(Lambek) correspondence in mathematical logic, and how the Wolfram model naturally generalizes this correspondence to the foundations of physics; I will provide a brief pedagogical introduction to homotopy type theory and the univalent foundations program, as well as to Michael Shulman’s cohesive variant of homotopy type theory and his synthetic differential geometry program; I will then discuss multiway systems as a candidate formalism for investigating ideas in homotopy type theory, with multiway rules corresponding to type constructors, completion rules corresponding to homotopies, etc.; next, I will discuss the significance of Grothendieck’s hypothesis for the origins of geometrical structure in both mathematics and physics, the implications it has for the interpretation of branchial graphs as projective Hilbert spaces, causal graphs as Lorentzian manifolds, etc., and will give informal justifications for our interpretation of the rulial multiway system as an infinity-topos endowed with a Grothendieck topology, as well as discuss the relationship between the univalence axiom and my previously developed “completion” interpretation of quantum mechanics; I will also introduce my new “relativistic” interpretation of the first incompleteness theorem, as a statement of the effective gauge dependence of semantic truth in mathematics, and its implications for the geometrization and computationalization of both proof theory and model theory, as well as the potential significance of the “generalized Einstein field equations” that act in the space of all possible mathematical proofs; I will then give some explicit examples of foliations and fibrations of rulial multiway systems for the special case of finitely presented algebraic structures; finally, I will discuss the geometrical and topological significance of fibrations in the rulial topos and their implications for the foundations of quantum mechanics (and, in particular, I will demonstrate a hitherto undiscovered relationship between the Wolfram model formalism and the dagger symmetric monoidal category formalism of categorical quantum mechanics), before ending with a brief philosophical note about how this new way of thinking about metamathematics and “metaphysics” may yield new insight into why both the laws of mathematics and the laws of physics (particularly those of quantum mechanics and general relativity) are actually true.

The Curry–Howard Isomorphism and Its Physical Generalization

Let me begin by describing the broad philosophical setup of this bulletin. In mathematical logic and theoretical computer science, there is a famous result named after Haskell Curry and William Alvin Howard (and deeply connected to the core ideas of intuitionistic logic and its operational interpretation) known as the “Curry–Howard isomorphism” or “Curry–Howard correspondence”. Loosely speaking, what it says is that all mathematical proofs can be interpreted as computer programs, and (somewhat more surprisingly) all computer programs can be interpreted as mathematical proofs. In other words, the core problems of proof theory in mathematical logic and programming language theory in theoretical computer science are actually identical.

At some level, the Curry–Howard isomorphism provides the formal justification for an otherwise obvious intuition. In pure mathematics, one starts from a set of “axioms”, one applies a “proof” (in accordance with a set of “rules of inference”) and one obtains a “theorem”. The abstract notion of computation can thus be thought of as being an ultimately desiccated version of the concept of mathematical proof, in which one starts with some “input”, one applies a “computation” (in accordance with a set of “algorithmic rules”) and one obtains an “output”. In other words, one has the formal correspondence:

&#10005

Indeed, the symbolic nature of the Wolfram Language allows us to see this correspondence explicitly. If we prove a trivial mathematical theorem (such as the theorem that a==c, starting from the axioms a==b and b==c, i.e. a proof of the transitivity of the equality predicate), then we obtain a symbolic proof object:

&#10005

&#10005

&#10005

Each statement in the proof, such as “a==c”, can be interpreted as a symbolic expression. Each application of an inference rule, such as “a → b” (which is, in turn, derived from the axiom “a==b”) can be interpreted as an application of a symbolic rewrite rule. Thus, the entire proof can be implemented as a symbolic piece of Wolfram Language code, in which the key steps of the proof are performed using the MapAt[...] and Replace[...] functions:

&#10005

Running this piece of code allows us to determine that the corresponding theorem is actually true:

&#10005 []

As such, we can interpret the Curry–Howard isomorphism as being the statement that every ProofObject in the Wolfram Language has an associated proof function (which we can explicitly demonstrate, as shown previously), and moreover that every piece of symbolic Wolfram Language code has a corresponding interpretation as a ProofObject for some theorem. The latter direction is easy to see once one appreciates that all terminating Wolfram Language programs are ultimately reducible to finite sequences of transformation operations being applied to symbolic expressions, just like in a mathematical proof.

To be a bit more rigorous, the Curry–Howard isomorphism involves invoking the so-called “propositions as types” interpretation of metamathematics; in other words, Curry–Howard states that a program that produces an output of a given data type can be interpreted as a proof that the corresponding type is inhabited, and vice versa. (Note that there is also a three-way “Curry–Howard–Lambek” correspondence employed within category theory, in which objects in a “Cartesian closed category” can be interpreted as propositions, and morphisms between those objects can then be interpreted as the corresponding proofs of implication between propositions. We will hint at some details of the Curry–Howard–Lambek correspondence later on in the bulletin when we discuss connections to category theory, but an exhaustive review of this relationship is beyond the scope of this article.)

In the Wolfram Physics Project, and in the field of physics more generally, one also considers an ultimately desiccated notion of what a “physical system” truly is. More specifically, one imagines the system beginning in some “initial state”, undergoing “motion” (in accordance with some “laws of motion”), and ending up in some final state. This immediately suggests a further refinement of the Curry–Howard isomorphism, in which programs, proofs and physical systems are really the same kind of thing:

&#10005

Viewed in this way, the Church–Turing thesis is neither a definition, a theorem, nor a conjecture; rather it is a hypothesis of fundamental physics. Namely, what the Church–Turing thesis truly says in this context is that the set of partial functions that can be computed by a universal Turing machine is exactly the set of partial functions that is instantiated by the laws of physics. Or, more concretely, the set of possible motions of a (physically realized) universal Turing machine is in one-to-one correspondence with the set of possible motions of any physical system, anywhere in the universe.

The rest of this bulletin will be dedicated to fleshing out the details and implications of this correspondence, both for the foundations of physics and for the foundations of mathematics.

Homotopy Type Theory, Univalent Foundations and Synthetic Geometry

Homotopy type theory is an augmentation of type theory (or, more specifically, of Per Martin-Löf’s intuitionistic type theory) with one key additional axiom, namely Vladimir Voevodsky’s axiom of univalence, whose significance we shall discuss later. The key philosophical idea underpinning homotopy type theory is a slight extension of the usual “propositions as types” interpretation of the Curry–Howard correspondence, in which “types” now correspond to topological spaces (homotopy spaces), “terms” of a given type correspond to points in those spaces, proofs of equivalence between terms of a given type correspond to paths connecting the associated points, proofs of equivalence between proofs correspond to (potentially higher) homotopies between the associated paths, etc. In other words, homotopy type theory is a way of endowing type theory (and the foundation of mathematics more generally) with a kind of inbuilt topological structure.

We know from ordinary topology that a homotopy is just a continuous deformation between paths. More precisely, given a pair of continuous functions f and g from a topological space X to another topological space Y, one can define a homotopy as being a continuous function h from the product space of X with the (closed) unit interval to Y, where the unit interval can be thought of as “parameterizing” that homotopy. To see this explicitly, suppose that we define function f to just be an ordinary Sin function:

&#10005

&#10005

In homotopy type theory, we would interpret this overall space as being a type, the endpoints of this path would be terms of that type and the path defined by the function f would correspond to the proof that those terms are equivalent. Now, in ordinary mathematics, we are used to the idea that a given theorem can have many (apparently distinct) proofs, such as in the case of the fundamental theorem of algebra, in which there is a great variety of possible proofs stemming from topology, complex analysis, abstract algebra, Riemannian geometry, etc. So suppose instead that we define g to be a slightly different function connecting the same two points:

&#10005

&#10005

Now we can interpret this path as being a different possible proof of the same proposition (namely the proposition that the terms corresponding to the endpoints of the path are equivalent). We can then define a smooth homotopy between these two paths as follows:

&#10005

&#10005

Although this homotopy lives naturally within this higher-dimensional space, we can easily project it back down onto our original space:

&#10005

Finally, this homotopy can be interpreted itself as being a proof that the two original (different) proofs are actually equivalent (in the sense that they both constitute valid proofs of the same theorem). As we have now seen explicitly, this homotopy can itself be interpreted as a path in some higher-dimensional space, so we can also proceed to define homotopies between those paths, which would correspond to proofs of equivalence between proofs of equivalence of proofs etc. Thus, there is actually a whole infinite hierarchy containing all possible higher-order homotopies, corresponding to the infinite hierarchy of all possible higher-order proofs of equivalence, and this hierarchy will become relevant to our discussion soon, once we start considering its implications for the geometry and topology of rulial space.

The effort to formalize mathematics in terms of homotopy type theory is commonly known as the “univalent foundations program”, in reference to the central role played by Voevodsky’s univalence axiom. One of the “big-picture” questions driving the advancement of univalent foundations (as well as many related areas, such as Michael Shulman’s formulations of “synthetic topology”, “cohesive geometry”, etc.) is a desire to better understand the role played by “space” in the foundations of mathematics.

In some ways, it is a great mystery why so many different mathematical structures (such as groups, rings, fields, Boolean algebras, lattices, etc.) somehow also come naturally equipped with a corresponding notion of “space”. For instance, in the context of group theory, a group is usually defined purely algebraically (i.e. as a closed algebraic structure obeying the axioms of associativity, identity and inverse), and yet one nevertheless has Lie groups, topological groups, matrix groups, loop spaces, etc., within all of which there naturally appears some kind of corresponding spatial structure (such as a differentiable manifold in the case of a Lie group, or a topological space in the case of a topological group, etc.), which just seems to “come along for the ride”, in the sense that the spatial structure is somehow respected by all of the underlying algebraic operations, without ever being explicitly “told” to do so.

We can make this idea manifest by considering the case of the Lie group SO(3). First, consider the set of all 3 × 3 orthogonal matrices of determinant 1; here, we shall look directly at a finite subset:

&#10005

Then, SO(3) can be defined purely syntactically in terms of a binary operation on this set of elements (in this case, corresponding to the operation of matrix multiplication) that obeys the axioms of associativity:

&#10005

identity:

&#10005

and inverse:

&#10005

However, because of the natural interpretation of 3 × 3 orthogonal matrices of determinant 1 as 3D rotation matrices, SO(3) comes naturally equipped with a spatial structure corresponding to the following differentiable manifold (and, hence, is indeed a Lie group):

&#10005

But why? The ZFC axioms of set theory are purely syntactical and algebraic: there is no inherent notion of “space” in ZFC. So why should objects (like groups) defined within ZFC in a purely syntactical and algebraic way induce a notion of space as if by magic? Homotopy type theory aims in part to address this mystery of the origin of space, by considering instead a foundation for mathematics that is explicitly spatial and topological at the outset, and in which the other aspect of mathematics (namely its syntactical structure) is somehow emergent.

In the context of the Wolfram Physics Project, we found ourselves addressing a very similar question. Our models are defined purely combinatorially, in terms of replacement operations on set systems (or, equivalently, in terms of transformation rules on hypergraphs). And yet, the correspondence between our models and the known laws of physics depends upon there existing a reasonable interpretation of these combinatorial structures in terms of continuous spaces. My derivation of the Einstein field equations, for instance, depends upon spatial hypergraphs having a reasonable continuum limit in terms of Riemannian manifolds (and hence on them being a reasonable candidate for physical space):

&#10005

And, moreover, it depends upon causal graphs having a reasonable continuum limit in terms of Lorentzian manifolds (and hence on being a reasonable candidate for spacetime):

&#10005

And, at a more abstract and speculative level, some of my more recent conjectures regarding the quantum mechanical aspects of our formalism depend upon the continuum limits of branchial graphs in multiway systems being interpretable in terms of projective Hilbert spaces:

&#10005

Or multiway causal graphs as being akin to twistor correspondence spaces:

&#10005

So could these two questions be related? Could the explanations offered by homotopy type theory for the origins of spatial structure in mathematics also imply, after appropriate translation, equivalent explanations for the origins of spatial structure in physics? And, if so, what would the things that we’ve recently discovered in the course of the Wolfram Physics Project so far imply regarding the foundations of (meta)mathematics?

Multiway Systems as Models for Homotopy Type Theory

As discussed previously, the axioms of a mathematical theory can be interpreted as defining sets of transformation rules between symbolic expressions. For instance, in the axioms of group theory:

&#10005

The associativity axiom can be interpreted as the following pair of (delayed) pattern rules:

&#10005

&#10005

And therefore a proof of a mathematical proposition can ultimately be represented as a multiway system. Indeed, at some level, this is precisely what a ProofObject is:

&#10005

&#10005

When I first started developing FindEquationalProof back in 2017, I designed the ProofObject to be formatted a little differently to the way multiway systems are conventionally formatted. The green (downward-pointing) arrows are the axioms, the dark green diamond is the hypothesis and the red square is the conclusion (in this case, the conclusion being that the corresponding hypothesis is true). Each of the orange circles is a substitution lemma, and can be thought of as being an ordinary multiway state node: it’s an intermediate lemma that is deduced along the way by simply applying the axiomatic transformation rules described before, just like in a regular multiway system. However, each of the dark orange triangles is a critical pair lemma, which is an indication of a place where the multiway system bifurcates, and in which an additional lemma is required in order to prevent it from doing so (in other words, it corresponds to a place where a completion procedure has been applied). Looking at a specific example of such a lemma

&#10005 [5]["Proof"]

we see here that two rules, indicated by “Rule” and “MatchingRule” (derived from axiom 2 and axiom 1, respectively) both match a common subpattern, indicated by “Subpattern”, and produce (syntactically) inequivalent expressions, thus producing a bifurcation in the multiway system. However, since both elements in the bifurcation were derived from a common expression by valid application of the rewrite rules, this bifurcation itself constitutes a proof that the two elements are equivalent, and hence we can declare them to be equal (which is the statement of the critical pair lemma). This declaration of equivalence immediately forces the bifurcation to collapse, so we deduce that by adding a sufficient number of critical pair lemmas to the rewrite system, we can therefore force the multiway system to have only a single path (at least up to critical pair equivalence). This, incidentally, is identical to the process of adding critical pair completions so as to force causal invariance in the Wolfram model, which (as I first proposed back in 2019) is the formal basis of our current operational model for quantum measurement; this deep correspondence with the foundations of quantum mechanics will be explored in more detail later.

Therefore, the proof graph may be thought of as being a kind of intermediate object between a single evolution thread and a whole multiway system; the substitution lemmas by themselves indicate the path of a single evolution thread, but the critical pair lemmas indicate the places where that evolution thread has been “plumbed into” a large, and otherwise bifurcating, multiway system. We can see this correspondence more directly by considering a simple string multiway system:

&#10005

We can clearly see that the strings “AA” and “ABBBABBB” are connected by a path in the multiway system—a fact that we can visualize more explicitly like so:

&#10005

&#10005

In effect, we can interpret this path as being a proof of the proposition that “AA” → “ABBBABBB”, given the axiom “A” → “AB”. To make the correspondence manifest, with a small amount of additional code we can also represent this path directly as a ProofObject:

&#10005

&#10005

&#10005

Of course, a key idea in homotopy type theory is that we can consider the existence of multiple paths connecting the same pair of points, and hence multiple proofs of the same proposition. For instance, take:

&#10005

&#10005

Homotopy type theory then tells us that we can represent the proof of equivalence of these proofs as a homotopy between the associated paths. Since an (invertible) homotopy is ultimately just a mapping from points on one path to corresponding points on the other path (and back again), this is easy to represent discretely as follows:

&#10005

&#10005

However, this homotopy is kind of a “fake”, in the sense that it has been explicitly “grafted on” to the multiway system after the fact. The more “honest” way to enact a homotopy of this kind would be to define explicit multiway rules mapping from states along one path onto states along the other, thus yielding:

&#10005

This new multiway system is analogous to the higher-dimensional space in which we constructed a continuous homotopy earlier on in the bulletin; by “projecting down” onto the lower-dimensional multiway system, we are able to infer equivalence between the corresponding proofs. This process of adding invertible rules mapping from one point along a branch to another is precisely what a completion procedure on critical pairs does, as commonly enacted in automated theorem-proving systems, as well as within our present interpretation of quantum measurement. The correspondence among critical pair completion, quantum measurement and homotopies can thus be seen directly for the first time, although to make this correspondence mathematically rigorous requires first understanding its connection to the univalence axiom, as we shall see later.

As Xerxes Arsiwalla pointed out, it is therefore appropriate to think of the multiway rules (like “A” → “AB”) as being analogous to type constructors in mathematical logic (i.e. rules for building new types), so as to allow the multiway systems themselves to be interpreted as inductive types, just as homotopy type theory requires. Moreover, these completion procedures described previously that allow us to define homotopies between paths are a kind of higher-order rule (i.e. they are rules for generating new rules, namely the completion rules), with the result being that the higher-dimensional multiway system that one obtains after applying such a completion procedure is the analog of a higher inductive type. Since there exists an infinite hierarchy of higher inductive types, it follows that there must exist a correspondingly infinite hierarchy of higher-order multiway systems, with the multiway system at level n being a partially “completed” version of the multiway system at level n – 1 (i.e. in which certain explicit homotopies have been defined between particular pairs of paths). So a natural question to ask is: what kind of mathematical structure would such a hierarchy represent?

Groupoids, Topoi and Grothendieck’s Hypothesis

In category theory, a “category” is just a collection of objects (which can be represented as nodes), along with a collection of “morphisms” between those objects (which can be represented as directed edges), and with the property that all morphisms are both associative and reflexive (i.e. there exists an identity morphism for each object). For instance, starting from a directed graph

&#10005

we can force every directed edge (i.e. every morphism) to be associative by computing the transitive closure:

&#10005

From here, we can then enforce reflexivity by adding a single self-loop (i.e. an identity morphism) around each vertex:

&#10005

Thus, this directed graph has a bona fide interpretation as a small category (“small” because the corresponding directed graph is finite). On the other hand, a “groupoid” is a special case of a category in which all morphisms are invertible (and hence are isomorphisms), which we can again demonstrate purely graph-theoretically by converting our directed graph into an undirected one:

&#10005

Or, to be even more explicit, we could add two-way directed edges to indicate the isomorphisms more directly:

&#10005

Groupoids are so named because they generalize the structure of ordinary algebraic groups; a group can essentially be thought of as being a special case of a groupoid that contains just a single object, and where the single invertible morphism corresponds to the (unary) group inverse operation.

Closely related to groupoids are objects known as “topoi”, which can be thought of as being the abstract categorical generalization of point-set topology. A “topos” is a category that “behaves like” the category of sets (or, to be more precise, like the category of sheaves of sets on a given topological space) in some suitably well-defined sense. The crucial feature of a topos that relates it to a groupoid, however, is that topoi necessarily possess a notion of “localization”.

In ordinary commutative algebra, rings are not required to possess multiplicative inverses for all elements, so one can “localize” the ring by introducing new denominators (such that the localization is like a restricted version of the field of fractions), thereby introducing multiplicative inverses for elements where they did not previously exist. Similarly, the localization of a category introduces some inverse morphisms where they did not previously exist, hence converting some collection of morphisms into isomorphisms, and thus causing the category to behave “locally” like a groupoid. All of our multiway systems are naturally equipped with a notion of localization; for instance, consider the string multiway system that we explored earlier:

&#10005

We can now select 10 edges at random and introduce their reverse directed edges, so as to simulate adding inverse morphisms for a collection of 10 random morphisms.

&#10005

&#10005

Much like in the foliation example given previously, this method of localization is kind of a “fake”, since we are just artificially grafting these inverted edges onto a preexisting multiway graph. Instead, we can simply adjoin the reversed edges as a new set of multiway rules:

&#10005

&#10005

Applying this localization procedure to the entire multiway rule, unsurprisingly, yields the following groupoid-like structure:

&#10005

Since, in the category of sets, all objects are sets and all morphisms are functions from sets to sets, and because for any function from set A to set B there can exist (at least locally) an inverse function from set B to set A, the category of sets is trivially localizable. It is in this sense that we can say that more general kinds of topoi “behave like” the category of sets.

One can make this correspondence more mathematically rigorous by realizing (as noted by Xerxes) that, when interpreting multiway systems as inductive types and the associated multiway rules as type constructors, then so long as one includes a “subobject classifier” (namely a special object in the category that generalizes the notion of a subset identifier, where all subobjects of a given object in the category correspond to morphisms from the subobject onto the subobject classifier), and assuming that finite limits exist (where a limit is just a categorical construction that generalizes the universal constructions of products and pullbacks), the resulting multiway system that one obtains is precisely an elementary topos. We have furthermore made the conjecture (although we do not yet know how to prove it) that this subobject classifier is what endows our multiway systems with the concept of “foliation” that is so crucial for constructing branchial spaces, and for deducing both quantum mechanics and general relativity in the appropriate continuum limits, since, at least intuitively, each hypersurface in the foliation may be thought of as corresponding to a subobject in the corresponding category. We shall explore this conjecture more closely, and examine precisely what foliations of multiway systems mean from a metamathematical standpoint, within the next section.

For the time being, however, it suffices to realize that such an elementary topos comes naturally equipped (thanks to various results in cohesive geometry) with a functor (that is, a map between categories) to the topos of sets, as well as a pair of adjoint functors (where adjunction refers here to a kind of “weak” equivalence relation between functors) admitting the discrete and indiscrete topologies, respectively. Free topoi possessing this particular collection of functors provide a means of formalizing the notion of a topological space.

As discussed earlier, inducing a homotopy between two paths (or, equivalently, applying a completion procedure between multiway branches) can be thought of as introducing new, higher-order “rules of rules”, and hence has the effect of producing a higher-order object than the type (or multiway system) that one originally started with. This notion of “higher-order” objects can be made more precise using the language of category theory; if each path is interpreted as a morphism between objects (known as a “1-morphism”), then a homotopy can be interpreted as a morphism between 1-morphisms (known as a “2-morphism”), with the resultant structure being a “2-category”. Homotopies of homotopies can hence be interpreted as 3-morphisms within 3-categories, and so on, thus producing a whole infinite hierarchy of higher-order categories. The limit of this hierarchy is known as the “infinity-category”, which we can think of as being the structure obtained by inducing all possible homotopies (and, consequently, by applying all possible completion procedures) to a given multiway system.

In fact, by applying all possible completion procedures, and therefore applying all possible rules for generating rules, etc., we will inevitably populate the space of all possible rules of a particular size, so the resulting structure can also be thought of as being a “rulial multiway system”, defined in the conventional sense. Moreover, since each completion procedure introduces new inverse morphisms where they didn’t previously exist, and hence also enacts a certain kind of localization, the limiting structure is actually an “infinity-groupoid”. An infinity-groupoid is a “quasi-category” (i.e. a weakening of the definition of an ordinary category in which the composition of two morphisms need not be uniquely defined, and therefore in which the equalities that normally appear in the axioms of identity and associativity are replaced by isomorphisms up to higher homotopy), in which all morphisms are necessarily isomorphisms.

This realization is significant because of Grothendieck’s so-called “homotopy hypothesis”, which states that all infinity-groupoids can be interpreted as topological spaces (and consequently that all models of infinity-groupoids can be interpreted as homotopy types), which is ultimately one of the foundational assumptions of homotopy type theory. If Grothendieck’s hypothesis is true, it therefore provides rigorous justification for the claim that the rulial multiway system (which, as we have established, admits a natural interpretation as an infinity-groupoid) is itself a topological space, and hence is naturally endowed with a spatial structure. One immediate consequence of this is that, if we interpret the rulial multiway system as being a fibration, with the individual fibers corresponding to ordinary (non-rulial) multiway systems, and with spacetime causal graphs corresponding to the fibers of those multiway systems, etc., as we shall justify formally later, Grothendieck’s hypothesis effectively explains why our various combinatorial structures, such as multiway systems, branchial graphs, causal graphs, hypergraphs, etc., are additionally endowed with the spatial structures of things like projective Hilbert spaces and Lorentzian spacetimes: they are simply inheriting the spatial structure that is naturally endowed upon the rulial multiway system, as a consequence of the nature of these fibrations. We shall explore more precisely how this works momentarily.

We have so far neglected to mention the role that Voevodsky’s univalence axiom plays within this whole discussion. In the foundations of mathematics, the notion of “extensionality” commonly refers to the criteria by which objects are deemed to be identical (e.g. the “axiom of extensionality” in axiomatic set theory states that two sets are identical if and only if they contain the same elements); extensionality is thus the logical analog of a “StateEquivalenceFunction” in the case of our multiway system formalism. In conventional mathematical logic, “propositional extensionality” asserts that a pair of propositions may be considered identical if and only if they logically imply each other.

The univalence axiom is a grand generalization of the principle of propositional extensionality to what we may otherwise call “type extensionality”; it claims that two types can be considered identical if and only if they are equivalent (in the sense that they are connected by paths in the associated homotopy space). In fact, the statement of the axiom is a little bit more subtle than that (since it claims that the “if and only if” in the previous statement is itself a type-theoretic equivalence relation). But this captures the essential underlying idea.

When one induces a homotopy between two independent paths in a multiway system (which we can interpret as being a critical pair completion in the context of quantum measurement, or a proof of equivalence between proofs in the context of homotopy type theory), we effectively treat the corresponding paths as being identical, in the sense that they proceed to evolve as an effective single path in the multiway system. For instance, consider the following minimal case of a multiway system containing a single bifurcation that does not resolve:

&#10005

These two paths currently act as totally separate and disconnected branches, but if we now perform a critical pair completion

&#10005

the resultant multiway system behaves as though there is only a single path, since now there are new rules permitting one to “jump” instantaneously from one branch to the other:

&#10005

We are justified in treating these two paths as identical precisely because they are equivalent (thanks to their common ancestry in the “S” state). In other words, the formal justification for our interpretation of quantum measurement in the context of the Wolfram model, just like the formal justification for the identification of homotopy-equivalent paths in homotopy type theory, comes directly from the univalence axiom. Or, to put it slightly more poetically, quantum measurement, at least within our formalism, is simply “applied univalence” in a very precise sense.

We can think of “objective reality” in the context of mathematics as being effective causal invariance induced by the univalence axiom. We can also think of “objective reality” in the context of quantum mechanics as being effective causal invariance induced by the act of measurement. Both can be represented purely in terms of critical pair completions, and the correspondence between the two will be demonstrated in a very direct way later on.

Gauge-Dependence of Mathematical Truth and a “Relativistic” Interpretation of the Incompleteness Theorems

Kurt Gödel’s proof of the incompleteness theorems in 1931 established, via the ingenious technique of Gödel numbering, that Peano arithmetic (the standard axiom system for integer arithmetic) was capable of universal computation. Therefore, in particular, he demonstrated that Peano arithmetic could be set up so as to encode the statement “This statement is unprovable.” as a statement about ordinary natural numbers. Clearly, if this statement is true, then it is unprovable (so Peano arithmetic is incomplete), and if it is false, then it is provable (so Peano arithmetic is inconsistent).

As such, one way to phrase the first incompleteness theorem is “If Peano arithmetic is consistent, then there will exist propositions that are independent of the Peano axioms”. In other words, there will exist propositions where neither the proposition nor its negation are (syntactically) provable using the axioms of Peano arithmetic in any finite time. Thus, the first incompleteness theorem is ultimately a proof-theoretic statement: it concerns the class of propositions that are syntactically provable, independent of any semantic interpretation of the terms.

On the other hand, model theory studies what happens when one endows a mathematical theory with a concrete semantic interpretation of its propositional terms. For instance, returning to our previous example of the axioms of group theory, we have:

&#10005

Everything that we have discussed so far has concerned what can be proven purely on the basis of the syntax of these axioms, in which terms like a, b and c (for instance, in the case of the associativity axiom) can take the form of any arbitrary symbolic expression. However, if one now defines an explicit “domain of discourse” (e.g. a set over which one is quantifying, such that a, b and c now correspond to elements of that particular set), then one has thereby defined a model, with the resulting semantic interpretation now introducing an additional richness of structure that was absent in the “mere” proof theory.

Incompleteness also admits a model-theoretic interpretation, in addition to a purely proof-theoretic one. For instance, Kurt Gödel and Paul Cohen (in 1940 and 1963, respectively) proved that the continuum hypothesis regarding the relative cardinalities of infinite sets is independent of the axioms of ZFC set theory. One way of understanding this result is that Gödel proved that there must exist models of ZFC in which the continuum hypothesis is semantically true (i.e. ZFC + CH is consistent if and only if ZFC is consistent), whereas Cohen proved, using his technique of set-theoretic forcing, that there must exist models of ZFC in which the continuum hypothesis is semantically false (i.e. ZFC + CH is inconsistent). Therefore, if ZFC is consistent, then the continuum hypothesis must be independent of the axioms, because any statement that is syntactically provable must be semantically true in all models, if the underlying system is consistent.

Therefore, I believe that our formalism permits the following new “pseudo-relativistic” interpretation of the first incompleteness theorem: incompleteness is ultimately just a statement of gauge dependence in mathematics.

In the conventional mathematical treatment of relativity, the conformal structure of spacetime induces a partial order (namely the “causal” partial order) on spacetime events. Since there are generically many different total orders that are consistent with a given partial order, we can infer that there are many possible gauge choices/reference frames/foliations of the spacetime that are consistent with the causal partial order generated by its conformal geometry. Thus, the requirement for Lorentz symmetry ultimately corresponds to the statement that the ordering of timelike-separated events (i.e. events whose ordering is specified by the partial order) is gauge invariant, but the ordering of spacelike-separated events is gauge dependent.

Accordingly, my basic claim is that proof theory defines a partial order on the space of all possible mathematical propositions, and choices of models are coordinatizations of the space of mathematical proofs that are analogous to the choices of gauge that allow one to construct total orders that are consistent with this partial order. As such, there will exist propositions whose truth is gauge invariant (namely those that are syntactically provable, as defined by proof theory), and there will exist propositions whose truth is gauge dependent (namely those that are either semantically true or semantically false, but otherwise independent of the axioms, as defined by model theory). To see this explicitly, consider our usual string multiway system:

&#10005

A proposition such as “ABAB” → “ABBBBABB” is syntactically provable, since there exists a finite path (or a “chain”) through the partial order of the multiway system such that “ABBBBABB” is preceded by “ABAB”:

&#10005

&#10005

On the other hand, a proposition such as “AABB” → “ABBA” is not syntactically provable, since the two expressions form an anti-chain, so their relative order is not specified by the partial order of the multiway system, and this therefore corresponds to an undecidable proposition (i.e. a proposition that is independent of the underlying axioms that define the multiway system):

&#10005

However, we know that there will exist models in which this proposition is semantically true, which we can see directly by making the following explicit gauge choice:

&#10005

&#10005

&#10005

Here, we can see directly that “ABBA” is preceded by “AABB” in the total order induced by the foliation, and so this model is clearly consistent with the proposition. However, consider an alternative gauge choice:

&#10005

We see now that that “AABB” is preceded by “ABBA” in this new total order, so the proposition “AABB” → “ABBA” is not consistent with the induced ordering, and therefore the corresponding model is inconsistent with the proposition.

Note that these foliations all correspond to “flat” or “inertial” reference frames, which correspond to what we might call “free models” (i.e. models within which, when viewed as an algebraic structure equipped with finitary operations, the only nontrivial equations that hold between elements of the model are those defined by the axioms themselves, plus one additional relation defining the slope of the foliation, by analogy with “free groups”, “free algebras”, “free lattices”, etc.). Of course, in general, models can have arbitrary additional sets of constraints and equations, and hence will induce the analog of more arbitrary “non-inertial” reference frames, e.g:

&#10005

&#10005

The precise connection between foliation choices and sets of relations in the presentation theory of algebraic structures will be outlined in the next section. For the time being, though, considering more arbitrary classes of possible foliations naturally presents the question of what concepts like “curvature” correspond to in the context of the space of all possible mathematical proofs. Considering, as we have previously, each possible proof as corresponding to a different geodesic within this space, we infer that the presence of a vanishing Ricci curvature (i.e. a space in which geodesics neither converge nor diverge) thus corresponds to the case in which all proofs consist of entirely linear sequences of substitution rule applications with no resultant bifurcation, and thus no need for critical pair lemmas, e.g.:

&#10005

&#10005

&#10005

One implication of the presence of this vanishing Ricci curvature is that making an infinitesimal perturbation to this geodesic (e.g. by “pulling back” one of the intermediate substitution lemmas so as to make it part of the axioms) will exert only a minimal effect on the length of the geodesic (e.g. shortening the proof length by just 1 step):

&#10005

&#10005

&#10005

Conversely, each critical pair lemma is an indication of the presence of an elementary non-holonomy in the associated manifold (since each critical pair describes an elementary triangle in the multiway system, and so the presence of an unresolved critical pair indicates a failure of parallel transport around the associated triangle to preserve geometrical information, since the two “endpoints” of the triangle end up at different points in the proof space). Since the Riemann curvature tensor measures the failure of commutativity of the covariant derivative operator on an arbitrary Riemannian manifold, we can therefore think of the critical pair lemma density in a particular “direction” as being the analog of the projection of the Riemann curvature tensor in proof space. For instance, the proof of commutativity of the “Wolfram axiom” for Boolean algebra contains a high density of critical pair lemmas, and therefore corresponds to a geodesic propagating through a space with a non-vanishing curvature:

&#10005

&#10005

&#10005

Accordingly, the analogous perturbation to this geodesic has a more dramatic effect on its length (e.g. shortening it by a total of 3 steps rather than just 1):

&#10005 [[3]]["Statement"]

&#10005

&#10005

&#10005

In these proof graphs, each dashed line indicates where a previously proved result is being used in the proof of some future lemma, and so corresponds to the analog of a causal edge in an ordinary multiway system. Indeed, we can see the correspondence directly by first inspecting the sequence of causal edges as seen in an ordinary string multiway system

&#10005

and then comparing against the sequence of dashed edges in the associated proof object representation:

&#10005

&#10005

Therefore, we may think of the presence of these dashed lines (and hence, of causal edges) as being an indication of the degree to which newly proved lemmas “build upon” previous results, which may, in turn, be interpreted as a crude measurement of the degree of mathematical abstraction used within the proof. In the conventional mathematical formulation of the Wolfram model, I also first proposed that the correct interpretation of the energy-momentum tensor is the flux of causal edges through a constant hypersurface in the causal graph (such that energy is flux through spacelike hypersurfaces, momentum is flux through timelike hypersurfaces, etc.).

The immediate corollary of these realizations is that the abstract analog of the energy-momentum tensor in spacetime should be a kind of “abstraction tensor” in the space of mathematical proofs, measuring the density of these causal edges. Furthermore, we can infer that a generalization of the Einstein field equations should hold within this space of all possible mathematical proofs, and that these equations will assert that the level of abstraction of the proof (i.e. our abstraction of the energy-momentum tensor) should be directly related to the density of critical pair lemmas (i.e. our approximation to the abstraction of the Ricci curvature, which is, correspondingly, a proxy to the computational difficulty of generating the proof).

Just as all relativistic observers with nonzero mass are required to lie strictly on the interior (and not on the boundary) of elementary light cones, so too are computationally bounded models required to lie strictly on the interior of elementary “proof cones”. For instance, all geodesics highlighted in red here constitute syntactically valid proofs of the proposition “AA” → ”ABBBBABBBB“ (since all are ultimately consistent with the induced partial order):

&#10005

&#10005

However, two of these proofs lie strictly on the boundary of the associated “proof cone”, and hence correspond to the analog of lightlike, rather than ordinary timelike, paths:

&#10005

&#10005

&#10005

Therefore, although these proofs (here highlighted in yellow and purple) are syntactically correct, they cannot be witnessed by any computationally bounded (i.e. “subluminal”) model. Thus, we can conclude that non-constructive proofs correspond to the analog of lightlike paths in the associated proof space. One immediate and amusing consequence of this correspondence is that the analog of the Penrose–Hawking singularity theorems would imply that, in the presence of sufficient “abstraction density” in proof space, proofs will inevitably become non-constructive (i.e. the analog of a black hole event horizon).

To be more precise, we can infer that certain axioms (such as the axiom of choice in ZFC set theory and the law of excluded middle in classical logic) that are known to permit non-constructive proofs of propositions can be thought of as inducing the formation of black holes in the space of mathematical proofs. On the surface of a black hole event horizon, there will exist pairs of points where the only geodesics connecting them correspond to lightlike paths. Similarly, in a system of mathematics based on non-constructive axioms, there will exist pairs of terms (i.e. propositions) where the only proofs connecting them are non-constructive, and so one would require effective hypercomputation (corresponding to a model “traveling” at the analog of the “speed of light”) in order to be able to witness them model-theoretically.

Another rather interesting implication of this formalism is that there should exist model-theoretic analogs of logical speedup theorems, which correspond to the analog of Lorentz transformations in proof space. For instance, the famous Gödel speedup theorem asserts that, in formal axiomatic systems that are at least as rich as Peano arithmetic, there will exist propositions whose shortest proofs are of arbitrary length, but that such proofs can always be made shorter (i.e. “sped up”) by working in a stronger axiomatic system. We can easily see this by constructing explicitly the statement “This statement is unprovable using fewer than n symbols.”, which, via Gödel numbering, can be encoded as an elementary statement in Peano arithmetic. Clearly, if Peano arithmetic is consistent, then the shortest proof of this statement must contain at least n symbols, but it is nevertheless trivial to prove in the stronger axiomatic system PA + Con(PA) (i.e. the Peano axioms, plus an additional axiom asserting the consistency of the Peano axioms).

Similarly, we see that we now have a model-theoretic version of the same idea; by shifting to a “boosted” foliation, we can reduce the computational effort necessary to verify a theorem (i.e. to confirm that a particular path is consistent with the total order induced by the model), which is the analog of relativistic time dilation, but the tradeoff is that more computational effort is required in order to verify the model (since there now exist more terms on each slice of the foliation, all of which must be confirmed as being valid anti-chains with respect to the partial order of the proof network, in order for the model to be verified as being consistent with the underlying axioms), which forms the analog of relativistic length contraction, as seen here:

&#10005

&#10005

As such, the “invariant spacetime interval” now becomes the effective difference between the time complexity of verifying the theorem and the time complexity of verifying the associated model, such that, by making a parameterized change of model, there can be “no free lunch” (any computational saving made in one verification task is offset by a computational loss made in the other task). For instance, as mathematicians continue to increase the level of mathematical abstraction of the field by proving more theorems, a “generalized graduate student” who is prepared to accept the validity of those theorems on faith is able to make faster progress than they would have done if the abstraction level had been lower, but the tradeoff is that the foundations of mathematics become harder to formally verify as a result. In particular, we therefore conclude that non-constructive proofs are ones whose associated models would require infinite computational power to verify, as we conjectured previously.

This entire correspondence rests upon an interpretation of “spacelike-separated” terms as being ones that are mutually independent of the underlying axioms (and therefore among which relations can be defined without contradicting the underlying theory). If we interpret the axioms as forming an orthonormal basis for the proof space, then these mutually independent terms become precisely the linearly independent vectors in that space (in other words, proof-theoretic independence becomes linear independence). We can see how this analogy works explicitly by considering the particular example of finite presentation theory on generic algebraic structures, as we do subsequently.

Foliation Choices for Finitely Presented Algebraic Structures

Consider the pair of highlighted terms in the following multiway proof network:

&#10005

Since they are not comparable within the partial order defined by the proof network (i.e. since they form an anti-chain), the associated proposition may be considered to be independent of the underlying axiom system, as discussed previously. If we add an additional proposition asserting the equivalence of these terms, then, in the absence of any further relations, we will obtain something akin to the following (inertial) foliation:

&#10005

In other words, we see here a flat foliation in which the proposition is semantically true, since “ABBA” immediately precedes “AABBB” in the total order induced by that foliation choice. The addition of this relation then implies further relations between terms, which is why the foliation lines are extrapolated out to cover the entirety of proof space; if further relations were to be explicitly enforced, then we would obtain a more arbitrary (non-flat, non-inertial) foliation choice, as we showed before.

To see more directly how this works, consider the case of the finite presentation theory for simple algebraic structures. Note that we can represent generators for algebraic structures as unidirectional multiway rules like “A” → “AB”, and that the associativity of any such structure is enforced by the natural associativity of the concatenation operator for strings. Therefore, by examining the following multiway system

&#10005

we see that we naturally obtain the finitely presented semigroup with two generators, “A” and “B”. One could argue that strings more typically form a monoid, since the empty string "" constitutes a natural choice of identity element, but let’s choose instead to specify the identity element more explicitly as “E”, thus yielding the following finitely presented monoid:

&#10005

Further specifying inverse elements “X” and “Y” for “A” and “B”, respectively, yields a finitely presented group:

&#10005

This multiway system consequently designates the free group on generators “A” and “B”—the group is free in the sense that it does not obey any additional relations beyond those necessitated by the group actions themselves, and its “freedom” can be seen directly from the fact that the associated network has four essentially independent “branches” (one for each of the elements “A”, “B”, “X” and “Y”). It is important to note that these multiway systems are not Cayley graphs, since they contain strictly more information: Cayley graphs solve the word problem implicitly (e.g. if “E” is the identity element, then there is no vertex “EAE” in a Cayley graph—there is only “A”), whereas in one of these multiway models there is an explicit path demonstrating the solution of the word problem directly, e.g. “EAE” → “AE” → “A” etc. Since each edge corresponds directly to the application of a group axiom, a generator or a relation, these multiway systems are thus much closer to the underlying structure of the group axioms than a Cayley graph otherwise would be.

As an illustrative example, we could now force elements “A” and “B” to commute with one another by incorporating the additional relation “AB” == “BA”:

&#10005

Note that, within this scheme, generators are specified using unidirectional rules such as “A” → “AB”, whereas relations are specified using bidirectional rules such as “AB” ↔ “BA”. Unsurprisingly, the inclusion of such a relation has the effect of “binding” the two branches corresponding to elements “A” and “B” together, thus causing them to act as a single effective branch (since there is now a pair of rules that allows one to “jump” easily from one branch to another). In other words, the inclusion of this relation is equivalent to performing a critical pair completion on the associated branches, or, alternatively, to inducing a foliation on the multiway system (since the set of elements within which one is imposing equivalences in the context of a critical pair completion can equally well be thought of as being the set of elements within the level surface of some multiway foliation). Forcing commutativity of “X” and “Y” through the relation “XY”==“YX” has the same effect of binding the “X” and “Y” branches together:

&#10005

As one might reasonably expect, adding relations to enforce commutativity among all elements is equivalent to imposing an axiom of commutativity at a purely proof-theoretic level, and so the resulting multiway structure is isomorphic to that of an ordinary abelian group, in which all branches essentially collapse down to form a single branch:

&#10005

To take a slightly more subtle example, imagine instead imposing the relations “A”==“Y”, “B”==“X” (in other words, explicitly declaring that “A” is the inverse of “B”, and vice versa). The resultant multiway structure is

&#10005

which we can see is ultimately just a more “decorated” version of the multiway structure for the free group generated by a single element “A”, with a single inverse “X”:

&#10005

As such, a Knuth–Bendix completion applied to a multiway system corresponding to the free group on two generators can therefore be interpreted as applying all possible sets of relations

&#10005

and consequently generating the “maximally non-free” group structure:

&#10005

As an illustration of its “maximal non-freeness”, we can for instance see explicitly that this structure (which one can think of as being effectively the rulial space of all groups with two generators) exhibits, for instance, commutativity of elements “A” and “B”:

&#10005

And, being a rulial space, it follows that all other groups on two generators can be constructed via an appropriate fibration of this “maximally non-free” group structure, as we shall now try to demonstrate. Due to the correspondence between completion procedures in the context of imposing group relations and completion procedures in the context of performing quantum measurements, we can therefore think of the free group as being a “purely quantum mechanical” group structure, while the maximally non-free group is a “purely classical” group structure, with all other groups lying somewhere on the intermediate spectrum.

Fibrations of the Rulial Topos and the (Inevitable) Emergence of Geometry

I first developed the function MultiwayTuringMachine (as used in Stephen’s recent bulletin on exploring rulial space in the case of Turing machines) as a means of visualizing the evolution of arbitrary nondeterministic Turing machines using our multiway system framework; for instance, we can visualize the evolution of the 2-state, 2-color nondeterministic Turing machine constructed from deterministic Turing machine rules 100 and 150 as follows:

&#10005

After more evolution steps, we begin to see the following emergent structure in the states graph:

&#10005

One rather elegant ancillary benefit of the MultiwayTuringMachine functionality is its ability to produce visualizations of rulial space with ease, by simply constructing a multiway evolution from the application of all possible deterministic Turing machine rules of a particular size. For instance, we can visualize the rulial space of all 2-state, 2-color Turing machine rules ranging from 1 to 200 as follows:

&#10005

As discussed earlier, the rulial multiway system (which, within this new context, we may think of as being the structure that one obtains by starting from a particular multiway system and applying all possible completion rules, or equivalently by inducing all possible homotopies between paths), is naturally endowed with the structure of an infinity-topos, allowing us to localize by converting collections of morphisms into isomorphisms. We can do this because the rulial multiway system invokes all possible rules of a particular size, so if there exists a rule mapping state A to state B, then there will always necessarily exist another rule mapping state B back to state A etc. This realization makes it very natural to conjecture that the rulial topos can be “fibrated” in such a way that every particular multiway system corresponds to a particular “fiber” of rulial space in some fairly precise sense. For instance, the multiway system associated with the {100, 150} nondeterministic Turing machine shown previously would correspond to the fiber shown in red here:

&#10005

In ordinary topology, a “fibration” is a way of making precise the notion that it is possible to parameterize one topological space (known as a “fiber”) in terms of another topological space (known as a “base space”). In the more restricted “fiber bundle” construction, every fiber needs to be a copy of the exact same topological space (or, at the very least, the fibers must all be homeomorphic), but in the more general case of an arbitrary fibration, the only condition is that each pair of fibers be “homotopy-equivalent”, meaning that there must exist continuous maps from one fiber to the other such that the composition of those maps is homotopic to the identity map on the corresponding fiber. In particular, in order to demonstrate that the construction described is indeed a valid fibration in the topological sense, we must proceed to demonstrate that it satisfies the so-called “homotopy lifting property”.

In an ordinary fiber bundle, the “connection” is a rule for “lifting” an elementary step in the base space up to a corresponding elementary step in the fiber; thus, in our context, where each particular multiway system is interpreted as a base space, and the subgraph of the overall rulial multiway system that corresponds to that particular multiway system is interpreted as the corresponding fiber, our “connection” is the rule that allows one to map edges in the ordinary multiway system to the corresponding edges in the rulial multiway system. The “homotopy lifting property” is thus the property that any homotopies in the base space will naturally be “lifted up” by the connection to homotopies in the corresponding fiber. To see how this works directly, consider the following pair of paths in our original (nondeterministic Turing machine) multiway system:

&#10005

&#10005

&#10005

We can now proceed to define a homotopy between these paths in the usual way:

&#10005

&#10005

The homotopy lifting property will be satisfied (and, consequently, our interpretation of the ordinary multiway system as being the base space for an associated fiber in the rulial multiway system will be formally justified) if and only if for every such homotopy between pairs of paths the homotopy is “lifted” by the connection to form a valid homotopy in the rulial multiway system as well—a fact which we can now make manifest:

&#10005

This interpretation of ordinary multiway systems as being the fibers of some rulial topos, when combined with Grothendieck’s hypothesis, therefore explains not only why so many discretely defined mathematical structures (like groups, rings, algebras, lattices, etc.) come naturally associated with a notion of a continuous spatial structure (such a differentiable manifold for a Lie group, a topological space for a topological group, a collection of clopen subsets of a topological space for a Boolean algebra, etc.), as explained by Shulman’s synthetic topology and cohesive geometry programs. Indeed, in this context, it suffices to treat Grothendieck’s hypothesis less as a hypothesis and more as an abstract definition of what it means to be a topological space (i.e. anything with an infinity-groupoid structure). It also explains why our discretely defined physical structures (such as hypergraphs, causal graphs, multiway graphs, etc.) also come naturally associated with a continuous spatial structure (such as a Riemannian manifold for a hypergraph, a Lorentzian manifold for a causal graph, a projective Hilbert space for a branchial graph, [conjecturally] a twistor correspondence space for a multiway causal graph, etc.)

At some ultimate level, all of these objects are simply inheriting their topology and geometry from that of the rulial multiway system, and its natural infinity-topos structure; the rulial multiway system endows its fibers (the ordinary multiway causal graphs) with the spatial structure of (conjecturally!) a twistor correspondence space. These multiway systems then endow their hypersurfaces (the branchial graphs) with the spatial structure of a projective Hilbert space, and also endow their fibrations (the ordinary spacetime causal graphs) with the spatial structure of a Lorentzian manifold; these spacetime causal graphs in turn endow their hypersurfaces (the spatial hypergraphs) with the spatial structure of a Riemannian manifold, etc.

So does anything exciting happen when we choose to “descend down” from the geometry of the full rulial topos to the rather more mundane geometry of a particular multiway system (of the kind that we conventionally use in our descriptions of quantum mechanics)? Well, as it turns out, the answer seems to be yes…

Symmetric Monoidal Categories and the (Inevitable) Foundations of Quantum Mechanics

Categorical quantum mechanics, as pioneered by Samson Abramsky and Bob Coecke, aims to define a relatively weak set of axiomatic constraints (for instance, much weaker than the usual Hilbert space axioms used in the standard operator-theoretic formulations of quantum mechanics) that can nevertheless reproduce the salient features of key quantum phenomena; its basic setting is a so-called “dagger symmetric monoidal category”. A “monoidal category” is a category equipped with an additional associative “bifunctor” (i.e. a map from a pair of categories down to a single category), mapping the product of the category with itself onto itself, that can be interpreted as an additional tensor product structure on that category, along with an element that acts as both a left and right identity for this tensor product bifunctor (where associativity and identity are enforced only up to natural isomorphism). A “symmetric monoidal category” is hence a monoidal category in which the tensor product bifunctor is “as symmetric as possible”, in the sense that the tensor product of A and B is naturally isomorphic to the tensor product of B and A. Finally, a “dagger symmetric monoidal category” is a symmetric monoidal category equipped with an additional involutive “dagger structure”, whose significance we shall discuss momentarily.

Arsiwalla subsequently observed that, with an appropriate interpretation of the tensor product type constructor, Abramsky and Coecke’s formulation of categorical quantum mechanics is precisely the formulation that we obtain upon foliating the rulial multiway system to obtain ordinary (quantum mechanical) multiway systems. More specifically, a particular multiway (nondeterministic) Turing machine, such as the one generated by deterministic 2-state, 2-color Turing machine rules 100, 150 and 200

&#10005

will exhibit a particular branchial graph structure upon appropriate foliation into branchlike hypersurfaces, which in this specific case happens to correspond to the rather simple pattern of disconnected triangular graph components shown here:

&#10005

On the other hand, the rulial multiway system, such as the one generated by deterministic Turing machine rules 1 to 300

&#10005

being naturally a much richer combinatorial structure, will in general produce a much more complicated branchial graph structure upon foliation into rulelike hypersurfaces:

&#10005

However, because the multiway graph itself corresponds to the base space for a particular fiber in the associated rulial multiway graph, we can consequently highlight where the triangles in the branchial graph structure for the ordinary multiway system have been “embedded” into the branchial graph structure for the overall rulial multiway system, as follows:

&#10005

So the obvious question now becomes: since the rulial multiway system is essentially constructed via a concatenation of all possible multiway rules, can we consequently interpret the rulial branchial graphs as corresponding to some generalized tensor product of all possible multiway branchial graphs? In other words, is a tensor product in branchial space simply a concatenation operation of rules in rulial space?

More work is required in order to make this correspondence mathematically rigorous (as we shall demonstrate in our forthcoming paper), but I shall give here a plausibility argument instead. The tensor product operation is characterized by a universal property of being the maximally free bilinear operation; loosely speaking, it is the most general bilinear operation (i.e. the most general operation mapping a product of vector spaces to a vector space, in such a way as to be linear in each of its arguments) that “behaves like a multiplication operation should behave”.

Take, as an illustrative example, the following pair of (isomorphic) multiway systems:

&#10005

Upon foliation, these yield the following pair of path-like branchial graphs, which we may interpret as corresponding to simple one-dimensional vector spaces:

&#10005

By concatenating the associated multiway rules together, we obtain a kind of “reduced” rulial multiway system with a somewhat more intricate structure

&#10005

yet one where the fibers associated with the original two multiway graphs are still easily discernible:

&#10005

Likewise, upon foliation of the reduced rulial multiway graph, the branchial graphs now form a two-dimensional vector space structure

&#10005

yet the original one-dimensional vector spaces involved in the tensor product can be identified as essentially forming the spanning set of this higher-dimensional space:

&#10005

Therefore, exactly as Arsiwalla had conjectured, the object obtained by foliation of the rulial multiway graph does indeed have a category-like structure, equipped with an additional “tensor product–like” bifunctor, whose associativity and commutativity (up to isomorphism) are guaranteed by the trivial associativity and commutativity of rule concatenation in multiway systems—or, in other words, we get exactly a symmetric monoidal category. This gives us a new, and much more eminently categorical, way of thinking about the formulation of quantum mechanics within our formalism, since now the branchial structure obtained through any foliation of the overall rulial multiway graph into ordinary multiway systems will necessarily correspond to a tensor product of (potentially finite-dimensional) Hilbert spaces, just as one would expect from the foundations of “ordinary” quantum mechanics. There is also much more to discuss here regarding this new interpretation of the tensor product operation in monoidal categories as being essentially a joining operation on type constructors, and the various algebraic and geometrical implications that it has.

One immediate, and rather interesting, implication this new interpretation entails is that the fibrations we were constructing before, which essentially allowed us to “split” a rulial multiway system into its constituent ordinary multiway systems, can be thought of as corresponding to a kind of generalized partial trace operation. This, in turn, provides further formal justification for our present interpretation of branchial graphs as being effective “graphs of entanglement” between microstates of the universe (i.e. graphs in which each vertex corresponds to a microstate, and in which the natural combinatorial distance metric on the graph corresponds to a measure of entanglement entropy), because now we can see explicitly that if a pair of microstates are “entangled” (i.e. if they are connected by a branchial edge), then any fibration that attempts to separate them will necessarily lose the information associated with that branchial edge. This corresponds precisely to the statement in ordinary quantum mechanics that any attempt to partially trace out one subsystem from a pair of entangled subsystems will necessarily cause the state to lose purity etc.

I mentioned previously that I would return to the remaining issue of the origins of the dagger structure in these models. The “dagger” in the dagger symmetric monoidal categories of categorical quantum mechanics is an additional structure that the monoidal category is equipped with that acts as an “involutive” functor (i.e. a functor that constitutes its own inverse operation), with the broad intuition being that the dagger operation corresponds to some appropriate generalization of the Hermitian adjoint operation from ordinary functional analysis, and hence can be used to define the appropriate generalizations of self-adjoint and unitary operators in categorical quantum mechanics. Of course, there are many possible choices of involutive functorial transformations that one could conceivably apply to a branchial graph (for instance, the reversal of a particular subset of directed branchial edges would be perhaps the most obvious example), but identifying which particular involutive transformation yields the most appropriate interpretation of the dagger structure within our models will require further work.

A Pseudo-Philosophical Remark about the Foundations of Physics

Indeed, the realizations discussed in this bulletin potentially give us a new insight into why the laws of both quantum mechanics and general relativity are actually true. As we have seen, the fact that the infinite limits of the combinatorial structures associated with causal graphs correspond to Lorentzian manifolds (for which, as I proved formally in the context of our models, the most general set of constraints needed to guarantee this limit correspond exactly to the Einstein field equations of ordinary general relativity) is guaranteed by Grothendieck’s hypothesis and the inheritance of spatial structure from fibrations of the rulial topos. But now, we see also that a symmetric monoidal category–like structure, and hence the entire formalism of categorical quantum mechanics, is also an inevitable feature arising from foliations of this exact same topos. And, as we have now established, the univalence axiom is precisely the assumption that allows us to transform these foliations into fibrations and back again (and hence, it is ultimately univalence that guarantees the logical consistency between quantum mechanics and general relativity in the context of our formalism, and demonstrates that both theories are really just different manifestations of the same fundamental principle of causal invariance). Thus, for the first time, we perhaps begin to glimpse not just what the laws of physics are, but also why the laws of physics (and, indeed, of mathematics) must be so.

Some Immediate Next Steps

• Complete the writeup of the supplementary mathematical paper to this bulletin.
• Work to obtain a better understanding of the potential origins of the involutive dagger structure in foliations of the rulial multiway system, and its implications for the foundations of quantum mechanics.
• Develop efficient code for converting neatly between multiway systems and proof objects.
• Perform a systematic experimental study of mathematical proofs generated using FindEquationalProof, in an attempt to determine empirically the form of the generalized “Einstein field equations” in the space of possible mathematical proofs (i.e. the quantitative relationship between the density of critical pair lemmas and the density of causal edges, as projected in particular directions).
• Determine the nature and interpretation of topological obstructions in the space of all possible mathematical proofs (my personal conjecture: at least when viewed as a rulial space, these obstructions will correspond to the analog of NP-complete problems that prevent one from performing the analogs of polynomial-time reductions between models/complexity classes).
• Investigate hypergraphs as a potentially appropriate formalism for representing “thickened” branchial graphs (i.e. branchial graphs in which state ancestry goes back further than a single evolution edge), and the possibility of thus obtaining an abstract generalization of categorical quantum mechanics.