Homotopic foundations of Wolfram Models
by Xerxes D. Arsiwalla
Pompeu Fabra University, Barcelona, Spain
by Xerxes D. Arsiwalla
Pompeu Fabra University, Barcelona, Spain
Project Goals: The main objective of this project is to contextualize the Wolfram physics models within the foundations of Homotopic Type Theory. This mathematical foundation helps formalize the notion of space and seeks to address the subset of rules that lead to physically plausible universes. Homotopy Type Theory (HoTT) provide the mathematical grounding for a synthetic theory of structure. Logic, topology and geometry are then formulated upon those structures. A natural question would be to ask what the physical counterparts of these mathematical objects may manifest themselves as within the Wolfram models? Moreover HoTT also characterizes inductive and higher inductive rules for transforming between rules. This parallels the rules and rules of rules in the Wolfram model. The significance of expressing physical models in this language of HoTT is that it makes precise the links between proofs and geodesics, thereby demonstrating a realization of the Einstein equations for higher types (and a corresponding Wheeler-DeWitt equation at each level). This exploration also provides a mathematical interpretation of the Knuth-Bendix completion within Wolfram models as an application of the Univalence Axiom in HoTT.
At its crux, the Wolfram physics project seeks to explore the most fundamental structures in the universe that admit the laws of physics as we know it. In order to achieve this, models in the project seek to understand how simple rules compose together leading to complex structures in possible physical universes. The quest for understanding fundamental structures has parallels in the foundations of physics as well as mathematics. The purpose of this article is to explore the mathematical foundations of multiway hypergraphs, branchial spaces and rulial spaces appearing in Wolfram models of the universe.
In recent years, Homotopic Type Theory (HoTT) has been developed as a framework for formalizing the foundations of mathematics. HoTT combines Martin-Lof Type theory from Intuitionistic Logic along with Voevodsky’s univalence axiom to provide the formal foundations for all mathematical structures. This program subsumes traditional set theory and generalizes to higher types that eventually provide a precise notion of spatial structures via Grothendieck’s hypothesis. In what follows, we illustrate how the formalism of HoTT relates to Wolfram models of physics. We begin with a discussion of multiway models of generic mathematical structures from the point of view of HoTT and how these objects can be identified as a free topos of space. This construction when interpreted as a section of the rulial space presents a multiverse of multiway systems. We discuss potential structures necessary to admit the laws of physics on these spaces. Finally, we discuss a further generalization of the full rulial multiverse as an ∞-topos and a potential classification of these universes as cellular automata.
In recent years, Homotopic Type Theory (HoTT) has been developed as a framework for formalizing the foundations of mathematics. HoTT combines Martin-Lof Type theory from Intuitionistic Logic along with Voevodsky’s univalence axiom to provide the formal foundations for all mathematical structures. This program subsumes traditional set theory and generalizes to higher types that eventually provide a precise notion of spatial structures via Grothendieck’s hypothesis. In what follows, we illustrate how the formalism of HoTT relates to Wolfram models of physics. We begin with a discussion of multiway models of generic mathematical structures from the point of view of HoTT and how these objects can be identified as a free topos of space. This construction when interpreted as a section of the rulial space presents a multiverse of multiway systems. We discuss potential structures necessary to admit the laws of physics on these spaces. Finally, we discuss a further generalization of the full rulial multiverse as an ∞-topos and a potential classification of these universes as cellular automata.
Multiway Models of Mathematical Structures
Rules in Wolfram models formally correspond to Type Constructors equipped with universal properties. In type theory, these constructors correspond to mathematical operations or objects, repeated application of which, generates the corresponding structure. For example, with type constructors corresponding to a binary product, a generator, an identity and an inverse (along with conditions of associativity) one generates a group structure. In the Wolfram model, these rules generate a multiway system, which is in fact the Cayley graph of the group. With the addition of co-products, the multiway system yields a co-algebra. In this way, the multiway models are capable of representing several mathematical structures.
Comparing type theoretic constructions of multiway models to HoTT, one can identify the multiway system to an ∞-Groupoid (this is a quasi-category where inverse morphisms exist and equalities of identity and associativity are replaced by isomorphisms up to homotopy of infinitely higher types). As per Grothendieck’s hypothesis, ∞-Groupoids are formal homotopic spaces, where terms of given types correspond to points and paths to type-theoretic proofs. Paths between terms can be isomorphic up to higher homotopies (when isomorphisms are strict equalities, we simply obtain a 1-category, in that sense, an ∞-Groupoid is a natural structure with fewer restrictions). When interpreted in type-theoretic terms, this is exactly the underlying construction of multiway systems. Additionally, if one includes a subobject classifier Ω (which is the categorical generalization of a subset identifier) among the type constructors and ensures that finite limits exist, one get an elementary topos T (sometimes referred to as a logical topos). Such a construction comes equipped with a functor Γ to the topos of sets along with two adjoint functors Δ and ∇ which respectively admit the discrete and indiscrete topology upon T. A free topos with these string of adjoint functors formalizes the notion of a homotopic space. The multiway systems of the Wolfram models precisely present the respective graphs of such homotopic spaces. Foliations in the multiway correspond to a sub-category, referred to as a branchial space. Completions in the multiway models are precisely identifications of propositional extensionality in Type theory (subsequently generalized to identification of types using the Univalence Axiom). These spaces are more general than those obtained from ZFC based set-theoretic constructions, in that they may may not always admit the law of the excluded middle or the axiom of choice. Rather, these topoi of spaces come equipped with Voevodsky’s Univalence Axiom.
Comparing type theoretic constructions of multiway models to HoTT, one can identify the multiway system to an ∞-Groupoid (this is a quasi-category where inverse morphisms exist and equalities of identity and associativity are replaced by isomorphisms up to homotopy of infinitely higher types). As per Grothendieck’s hypothesis, ∞-Groupoids are formal homotopic spaces, where terms of given types correspond to points and paths to type-theoretic proofs. Paths between terms can be isomorphic up to higher homotopies (when isomorphisms are strict equalities, we simply obtain a 1-category, in that sense, an ∞-Groupoid is a natural structure with fewer restrictions). When interpreted in type-theoretic terms, this is exactly the underlying construction of multiway systems. Additionally, if one includes a subobject classifier Ω (which is the categorical generalization of a subset identifier) among the type constructors and ensures that finite limits exist, one get an elementary topos T (sometimes referred to as a logical topos). Such a construction comes equipped with a functor Γ to the topos of sets along with two adjoint functors Δ and ∇ which respectively admit the discrete and indiscrete topology upon T. A free topos with these string of adjoint functors formalizes the notion of a homotopic space. The multiway systems of the Wolfram models precisely present the respective graphs of such homotopic spaces. Foliations in the multiway correspond to a sub-category, referred to as a branchial space. Completions in the multiway models are precisely identifications of propositional extensionality in Type theory (subsequently generalized to identification of types using the Univalence Axiom). These spaces are more general than those obtained from ZFC based set-theoretic constructions, in that they may may not always admit the law of the excluded middle or the axiom of choice. Rather, these topoi of spaces come equipped with Voevodsky’s Univalence Axiom.
Out[]=
Figure: A single rule multiway system as a prototype of mathematical structures.
Multiverse Models of Physical Structures
Given the above identification of multiway systems as formal spaces, the question we address here is what type of multiway models realize physically relevant spaces? The key mathematical question is: what type of topoi admit geometric structures relevant for physics? Not all multiways in HoTT admit smooth topological spaces with Riemannian or pseudo-Riemannian metrics. This is where very recent developments in Cohesive HoTT come into play [Shulman]. These authors have shown that topoi whose objects themselves are R^n (as a type, not necessarily a set) for all n ∈ N, admit smooth structures giving Riemannian geometries. Though it is not precisely known what collection of type constructors will specifically lead to such topoi, one can infer that the constructors needed have to at least include function types, natural number objects and identity types, among others. Additionally, for getting the category of quantum mechanics, a tensor product type constructor would be required. In the Wolfram models, hypergraphs with multiple rules corresponding to the abovementioned constructor types would potentially yield a realization of a geometric topos. Of course, here all quotients of R^n and their automorphisms are allowed. This is in fact, a multiverse of multiway models (each multiway corresponding to a single rule). Proof completions in the multiverse are now elegantly captures by the univalence axiom which generalizes propositional extensionality to type extensionality. Moreover, the sub-category obtained from a foliation of this multiverse precisely yields the categorical quantum mechanics of [Abramsky, Coecke] provided we have included the tensor product constructor. In other words, the branchial space of the multiverse is simply a categorical tensor product of finite dimensional vector spaces admitting an inner product. The geometric structure at the level of the rulial space is that the multiverse of physics is obtained as a fiber bundle, where a section of the rulial space forms a base and multiways corresponding to individual rules form fibers.
Out[]=
Figure: Schema of a multiverse generated from multiple rules
Classification of the Rulial Topos as Cellular Automata?
One can now go beyond the section of the rulial space generating a multiverse and ask what the full rulial space and its fibers correspond to? In fact, the most general rulial space will correspond not just to rules, but also to rules of rules. In HoTT, such objects are known as Higher Inductive Types (HITs). With HITs, the rulial space by itself acquires the structure of an ∞-Groupoid. Given that a multiverse without HITs was a topos, what we now obtain is in fact an ∞-topos (where the fibers collectively form all possible multiverses). However, one may ask whether the full ∞-topos may even be relevant for physics? One way to think about this issue is to classify multiverse fibers in a way analogous to the classification of one dimensional cellular automata. Having a universe built from every possible rule will inevitably include rules similar to rule 30 leading to multiverses that are computationally irreducible (class 3 cellular automata). This may not lead to computationally reducible universes. Physics itself may result from only those subsections of rulial space that allow for a certain degree of computational reducibility, corresponding to the class of computational automata (class 4). On the other hand, sectors of rulial space corresponding to computationally irreducible multiverses may potentially be relevant for describing potentially non-computational structures (for instance, mental attributes - which might be modelled as an observer-dependent projection of a computationally irreducible fiber to a reducible one, creating an illusion of "understanding").
{ArrayPlot[CellularAutomaton[110,{{1},0},50]],ArrayPlot[CellularAutomaton[30,{{1},0},50]]}
Out[]=
,
Figure: Are the multiverses of physics akin to cellular automata as rule 110 or rule 30?
Keywords
Keywords
◼
Homotopy Type Theory
◼
∞-Groupoids
◼
Univalence Axiom
◼
Grothendieck’s Homotopy Hypothesis
Acknowledgments
Acknowledgments
Mentor: Jonathan Gorard
The author profusely thanks Jonathan and Stephan for many inspiring and informative discussions. Thanks also to the entire organizing team of the WSS 2020!
References
References
◼
M. Shulman, Homotopy Type Theory: The Logic of Space, New Spaces for Mathematics and Physics, 2017
◼
S. Abramsky, B. Coecke, Categorical Quantum Mechanics, Handbook of Quantum Logic and Quantum Structures, 2009