Metamathematics

Let’s start by talking about perhaps the most abstract potential application area: metamathematics. The individual “tokens of mathematics” can be mathematical statements, written in some symbolic form (as they would be in the Wolfram Language). In a sense these mathematical statements are like the hyperedges of our spatial hypergraph in physics: they define relations between elements, which in the case of physics are “atoms of space” but in the case of mathematics are “literal mathematical objects”, like the number 1 or the operation Plus (or at least single instances of them).

Now we can imagine that the “state of mathematics” at some particular time in its development consists of a large number of mathematical statements. Like the hyperedges in the spatial hypergraph for physics, these mathematical statements are knitted together through their common elements (two mathematical statements might both refer to Plus, just as two hyperedges might both refer to a particular atom of space). What is the “evolution of mathematics” like? Basically we imagine that there are laws of inference that take, say, two mathematical statements and deduce another one from them, either using something like structural substitution, or using some (symbolically defined) logical principle like modus ponens. The result of repeatedly applying a law of inference in all possible ways is to build up a multiway graph of—essentially—what statements imply what other ones, or in other words, what can be proved from what. But what does a human mathematician perceive of all this? Most mathematicians don’t operate at the level of the raw proof graph and individual raw formalized mathematical statements. Instead, they aggregate together the statements and their relationships to form more “human-level” mathematical concepts. In effect that aggregation can be thought of as choosing some “mathematical reference frame”—a slice of metamathematical space that can successfully be “parsed” by a human “mathematical observer”. No doubt there will be certain typical features of that reference frame; for example it might be set up so that things are “sufficiently organized” that “category theory works”, in the sense that there’s enough uniformity to be able to “move between categories” while preserving structure. There are both familiar and unfamiliar features of this emerging picture. There are the analog of light cones in “proof space” that define dependencies between mathematical results. There are geodesics that correspond to shortest derivations. There are regions of “metamathematical space” (the slices of proof space) that might have higher “densities of proofs” corresponding to more interconnected fields of mathematics—or more “metamathematical energy”. And as part of the generic behavior of multicomputational systems we can expect an analog of Einstein’s equations, and we can expect that “proof geodesics” will be “gravitationally attracted” to regions of higher “metamathematical energy”. In most areas of metamathematical space there will be “proof paths” that go on forever, reflecting the fact that there may be no path of bounded length that will reach a given statement, so that the question of whether that statement is present at all can be considered undecidable. But in the presence of large amounts of “metamathematical energy” there’ll effectively be a metamathematical black hole formed. And where there’s a “singularity in metamathematical space” there’ll be a whole collection of proof paths that just end—effectively corresponding to a decidable area of mathematics. Mathematics is normally done at the level of “specific mathematical concepts” (like, say, algebraic equations or hyperbolic geometry)—that are effectively the “populated places” (or “populated reference frames”) of metamathematical space. But by having a multicomputational model of the low-level “machine code of metamathematics” there’s the potential to make more general statements—and to identify what amount to general “bulk laws of metamathematics” that apply at least to the “metamathematical reference frames” used by human “mathematical observers”. What might these laws tell us? Perhaps they’ll say something about the homogeneity of metamathematical space and explain why the same structures seem to show up so often in different areas of mathematics. Perhaps they’ll say something about why the “aggregated” mathematical concepts we humans usually talk about can be connected without infinite paths—and thus why undecidability is so comparatively uncommon in mathematics as it is normally done. But beyond these questions about the “insides of mathematics”, perhaps we’ll also understand more about the ultimate foundations of mathematics, and what mathematics “really is”. It might seem a bit arbitrary to have mathematics be constructed according to some particular law of inference. But in direct analogy to our Physics Project, we can also consider the “rulial multiway system” that allows all possible laws of inference. And as I’ve argued elsewhere, the limiting object that we get for mathematics will be the same as for physics, connecting the question of why the universe exists to the “Platonic” question of whether mathematics “exists”.