Open Questions in our Metamathematical Framework
By James Douglas Boyd (Wolfram Research, Inc.)

Mathematics Under the Multicomputational Paradigm

Our metamathematical framework is strongly informed by recent methodological and theoretical advances made by the Wolfram Physics Project. The key methodological advance is multicomputation, a new paradigmatic approach to computation in which multiple evaluation paths for a given computation are permitted, with path-selection determined by system observers. The foundational theoretical advance is the conceptualization of the ruliad: an idealization of all possible formal systems. One can find a natural affinity between multicomputaiton and the ruliad: observers find that, from the ambit of all possible rules, certain computations are expressed within certain systems. We use ruliology to study the behavior of possible rules and metamodeling to understand which rules are expressed in the behavior of systems of interest. With a suite of new conceptual and computational functions
We might pose the following question as a key motivation of our metamathematical project: what does it mean to perform mathematics in the ruliad? A facile, expedient response is that all mathematics is in the ruliad. A multicomputationally-informed response is that the mathematics that we practice emerges from simple rules that the ruliad contains. In order to understand how such might be the case, it is helpful to present our metamathematical framework as a series of stages. In what follows, the stages are presented in a manner that should allow the reader to ‘follow’ the procession from the most elementary rules in the ruliad to the computation of proofs as is performed by the working mathematician.

The Framework

Levels and Interfaces: An Overview

[...]

The Machine Level

The machine level encompasses emes and the behavior that they exhibit with respect to one another. A key property of memes is their confluence under the application of rules, which we might call machine invariance. One curious characteristic of the machine level is, notwithstanding the uniqueness of emes themselves, the non-uniform distribution of their outputs. For instance, let’s consider combinator emes. Those familiar with combinators will be accustomed to s-k notation, where the rule of universal s-k combinators is s[x_][y_][z_]:>x[z][y[z]], k[x_][y_]:>x. However, it seems methodologically inappropriate to characterize the rules at the base of the ruliad (to which anthropic observers have only limited access) using the symbols s and k from the Latin Alphabet. We will choose to apply arbitrary notation instead in order to demarcate distance between machine-level behavior and observers, writing the universal combinator rule instead as △[▶_][◀_][◇_]:>▶[◇][◀[◇]], ▽[▶_][◀_]:>▶.
​
In order to study machine invariance amongst combinators at the machine level, we examine their fixed points. Included below is the evolution of the combinator △[▽[△[△]]][▽[△]] to a fixed point when given as input [▶][◀].
Out[]=
△[▽[△[△]]][▽[△]][▶][◀]
▽[△[△]][▶][▽[△][▶]][◀]
△[△][▽[△][▶]][◀]
△[◀][▽[△][▶][◀]]
△[◀][△[◀]]
Now, △[▽[△[△]]][▽[△]] is not the only combinator that yields the output △[◀][△[◀]] upon input [▶][◀]. There are 18 combinators of size 6 that are machine-invariant:
In[]:=
CloudGet["https://www.wolframcloud.com/obj/sw-blog/Combinators/Programs.wl"];​​machineassociation=AssociationThread[ResourceFunction["EnumerateCombinators"][6,{△,▽}]->FixedPoint[ReplaceAll[#,{△[▶_][◀_][◇_]:>▶[◇][◀[◇]],▽[▶_][◀_]:>▶}]&,Table[i/.b_->FunctionToApplication[b[▶][◀]],{i,FunctionToApplication[ResourceFunction["EnumerateCombinators"][6,{△,▽}]]}]//.f_g_:>f@g]];​​​​machinedata=PositionIndex[machineassociation];​​​​Dataset[Lookup[machinedata,△[◀][△[◀]]],DatasetTheme"Scientific"]
Out[]=
△[▽[△[△]]][▽[△]]
△[▽[▽]][△[△]][△]
▽[△[△][▽][△][△]]
▽[△[△][▽[△]][△]]
▽[△[△][▽[△][△]]]
▽[△[△][▽[△][▽]]]
▽[△[▽[△][△]][△]]
▽[△[▽[△][▽]][△]]
▽[▽[△][△][△][△]]
▽[▽[△[△][△]][△]]
▽[▽[△[△][△]]][△]
▽[▽[△[△]][△][△]]
▽[▽][△][△[△][△]]
▽[▽[△[△][△]][▽]]
▽[▽[△[△][△]]][▽]
▽[▽[△[△]][▽][△]]
▽[▽[△][▽][△][△]]
▽[▽][▽][△[△][△]]
Included below is a multicomputation of machine-invariant combinators, which we term an accretion:
Out[]=
Here, each path from the periphery to the fixed-point center is a distinct application of a combinator rule. One such path is highlighted below:
Out[]=
Suppose we were to run all possible combinators of size 6 using the universal rule. We find that such combinators exhibit machine invariance, such that the distribution of fixed points is non-uniform. Included below are the 10 most common fixed points and a histogram of all fixed points of combinators of size 6 under the universal rule:
In[]:=
GraphicsRow[{Take[Dataset[Reverse[Sort[Counts[FixedPoint[ReplaceAll[#,{△[▶_][◀_][◇_]:>▶[◇][◀[◇]],▽[▶_][◀_]:>▶}]&,Table[i/.b_->FunctionToApplication[b[▶][◀]],{i,FunctionToApplication[ResourceFunction["EnumerateCombinators"][6,{△,▽}]]}]//.f_g_:>f@g]]]],DatasetTheme"Scientific"],10],Histogram[Counts[FixedPoint[ReplaceAll[#,{△[▶_][◀_][◇_]:>▶[◇][◀[◇]],▽[▶_][◀_]:>▶}]&,Table[i/.b_->FunctionToApplication[b[▶][◀]],{i,FunctionToApplication[ResourceFunction["EnumerateCombinators"][6,{△,▽}]]}]//.f_g_:>f@g]],Automatic,"Probability",PlotTheme"Detailed",ScalingFunctions"Log"]},ImageSizeLarge]
Out[]=
The accretions for the fixed points with the highest accretion number, and their adjacency matrices, are given below:
Out[]=
Contents cannot be rendered at this time; please try again later or download this notebook for full functionality »
Taking all rules with size-two outputs (△[▶][◀][◇] ▶[◀], ▽[▶][◀] ◀[▶]; △[▶][◀][◇] ◀[▶], ▽[▶][◀] ▶[◀]; etc.) applied by combinators of size 6, we yield the following distribution:
The fixed points and corresponding accretions for all such rules are included in the menu below:

The Interface Between the Machine Level and the Metamathematical Level

One might ask how fixed points of combinator accretions at the machine level relate to statements in metamathematics. Such fixed points, although evacuated of recognizable operators and operands typically encountered in mathematics, nonetheless possess nontrivial structure, which is evinced by their representation as trees. For instance, let’s consider from the menu above the rule △[▶][◀][◇]  ▶[◀], ▽[▶][◀]  ◀[▶] and its fixed point ▶[▽[▽]][◀]. We represent the fixed point below as an expression tree:
Here, Application is the  operator. All fixed points can be represented as trees or graphs (with the vertex labels removed). Below are the expression graphs for the 10 fixed points with the highest accretion numbers for the rule △[▶][◀][◇]  ▶[◀], ▽[▶][◀]  ◀[▶]:
​
Of these fixed points, one, ▽[▽], is of particular interest. We find that the expression trees corresponding to ▽[▽] and ▽=▽ appear to possess the same tree structure:
We might find such similarity to be encouraging; after all, it might suggest to use that, from combinator accretions at the machine level, we obtain fixed points that resemble axioms (in this case, ▽=▽, the axiom of equality). However, apparent similarity as such is deceptive, for ▽[▽] is a fixed point, whereas ▽=▽ is not (once evaluated, it reduces to True):
The two trees are not isomorphic (when taken as graphs):
Thus, we infer that the tree structure of accretion fixed points does not offer a sufficient criterion for determining axiomatic equivalence. After all, we might note that the expression tree for ▽[▽] is also structurally similar to that of △=▽:
Nonetheless, our instinct regarding the relationship between ▽[▽] and ▽=▽ is worth pursuing further. It is important to keep in mind that are ▽ and △ are abstract functions at the machine level and that the  application is merely syntactic, with greater semantics being observer-dependent. The  application could, semantically, express summation, multiplication, equivalence, or other relations. When we intuit that ▽[▽]could be equivalent to the axiom of equality, we are stating that, under observer semantics, treating ▽ ▽ as ▽=▽ will yield useful mathematical observations (i.e. it affords the performance of consistent mathematical work). Conventionally, mathematicians regard the germs of their entailment cones (axioms) to be ‘self-evidently true’ in the sense that they generate cones with non-absurd statements. Regarding the case in point, an observer can make a model in which it is true that a application of a single function to itself ▽[▽] is equivalent to application of the same single function to itself ▽[▽]. Writing ▽ as f, we include such a model below:
On the other hand, it is not self-evidently true that it is ▽[▽] is equivalent to △[▽] (which we write as g[f]); after all, ▽ and △ can assume different values. Therefore, there are many models that satisfy equivalence between ▽[▽]and △[▽]. In the termary case, 729 models satisfy the equivalence. 50 such models are included below:
It is natural to pose the question: why ▽[▽]==▽[▽] is modeled as True whereas ▽[▽]==△[▽] proliferates models? In order to answer this question, let us treat the equivalence ▽[▽]==▽[▽]) as a two way rules (TWR) ▽[▽]▽[▽]. We use TWRs in our metamathematical framework to compute the entailment cones of axioms. For instance, the axioms of group theory consists of the the following TWRs:
In order to exemplify TWRs, let us begin the simplest possible example. Let us take an ‘empty pattern’ _ and apply it to itself via the rule _==_. We can take the accumulative token-event graph of this rule (applying both substitution and cosubstitution).
We can refer to such a graph as a ‘static computability graph’. With successive iterations, we perform new substitutions and cosubstitutions on our original statement, but we do not yield new statements. Consider, on the other hand, the rule _==▽[△]. After only one iteration, we have created a number of new variables.
And, as one might anticipate, the generation of variables tends towards explosiveness after only two generations.
As a general principle, when a two-way rule admits a variable on the right-hand side (RHS) that is absent on the left-hand side (LHS), it will tend towards explosiveness due to its propensity to generate all possible statements. Now, we expect metamathematical space to include all possible entailment cones, and thus, all statements. However, the mathematician will recognize that not all statements are true. In our metamathematical framework, such a mathematician, qua observer, chooses not to practice mathematics along the entailment cone of an axiom that yields explosiveness in a similar manner to mathematical logicians when they assign falsity to contradictions in adherence to the Principle of Explosion (‘all statements can be derived from a contradiction’). We refer to explosive entailment cones of axioms that general absurd statements as rulial viruses and posit that mathematical observers can only maintain a practice of preservable mathematics by evading such viruses.
Thus, we posit that observers assign the quality of truth to statements that serve as the germs of stable, consistent entailment cones and falsity to statements that constitute rulial viruses. Our use of models previously exhibits the truth/-falsity discrimination facilitated by the mathematical observer.
[...]

The Metamathematics Level

[...]

The Interface Between the Metamathematics Level and the Mathematics Level

[...]

The Mathematics Level

[...]

Open Questions