CITE THIS NOTEBOOK: A Classification for Xenomathematical Systems by Hongyi Zhang. Wolfram Community JAN 12 2023.
In this project, we look for a possible scheme for classifying arbitrary axiom systems. By looking at the properties of the proof graph of Knuth-Bendix completion of existing axiom systems, a possible classification scheme is developed based on the number of theorems an axiom system entails, hoping to provide information about the desirability of a xenomathematical system. We apply this algorithm to a set of arbitrary axiom and demonstrates a few examples. The graphical property discussed in this project is very primitive,and need further development.
Purpose
Purpose
Modern day mathematics is a body of knowledge consisting of a starting axiom system and the theorems derived from it. We tend to question where do these axioms come from. One explanation is that they come from human’s intuition based on real life experiences. For example, the parallel postulate in Euclidean geometry can be concluded from observations of parallel lines on a plane. Later, when people tried to replace the parallel postulate with something else, they discovered non-Euclidean geometry, which describes the geometric objects on curved surfaces.
This explains our incentive for investigating xenomathematics: inventing a mathematical system that is seemingly irrelevant, but can potentially offer insight in a new field of mathematics. But the arbitrariness of axiom systems makes it impossible for us to study every one of them. Inspired by “The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics”, we want to apply rewrite algorithm to a list of arbitrary axioms. Particularly, we look at the graphs of existing axiom systems and look for desirable properties for xenomathematics axiom systems that is potentially useful.
This explains our incentive for investigating xenomathematics: inventing a mathematical system that is seemingly irrelevant, but can potentially offer insight in a new field of mathematics. But the arbitrariness of axiom systems makes it impossible for us to study every one of them. Inspired by “The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics”, we want to apply rewrite algorithm to a list of arbitrary axioms. Particularly, we look at the graphs of existing axiom systems and look for desirable properties for xenomathematics axiom systems that is potentially useful.
Knuth-Bendix Completion
Knuth-Bendix Completion
Using the Two Way Rule Token Event Graph on axioms often generate a never terminating entailment cone, which requires much computation and is thus difficult to analyze. We instead use the Knuth-Bendix Completion algorithm on these axioms to ensure an order of the rewrite rule, so the axiom systems have a better chance of terminating and outputting a desirable result.
Knuth-Bendix Completion is an algorithm that turns two way rules and a specific order into rewrite rules and then applies them to initial conditions. Specifically, the Knuth-Bendix Completion that we use in the project is one with a decreasing length of symbolic expressions (more symbols to less symbols) and left branch to right branch.
Knuth-Bendix Completion is an algorithm that turns two way rules and a specific order into rewrite rules and then applies them to initial conditions. Specifically, the Knuth-Bendix Completion that we use in the project is one with a decreasing length of symbolic expressions (more symbols to less symbols) and left branch to right branch.
The Graphs of Known Systems
The Graphs of Known Systems
We first rewrite the existing axiomatic system of today’s mathematics. Comparing the number of theorems at different time constraint, namely 1 second and 2 seconds, we find that there is no significant difference in the number of theorems proved, which means all of the axiomatic systems would terminate. The graph is a histogram of axiom systems and the number of steps taken to terminate or reach the time constraint. As is shown, the number of steps spread almost uniformly between 0 and 500, which indicates that there is seldom a trivial short case or an extremely large case.
Out[]=
Some examples might be the graph of Group axioms, Boolean axioms, and Huntington axioms, as is shown below respectively. We can read from the graph that they all reach a final termination point.
po1=KBC[AxiomaticTheory["GroupAxioms"]]["ProofGraph"]
In[]:=
po2=KBC[AxiomaticTheory["BooleanAxioms"]]["ProofGraph"]
Out[]=
In[]:=
po3=KBC[AxiomaticTheory["HuntingtonAxioms"]]["ProofGraph"]
Out[]=
With these intuition in mind, we are looking for axioms with similar graphical properties, namely termination and a moderately complex proof graph.
The Classification of “Axioms in the Wild”
The Classification of “Axioms in the Wild”
The arbitrary axioms that we consider here are the axioms with 2 variables, one operator, and length of 3 on each side of the equation. We have tested axioms whose length is 2 but that only generates very trivial examples. After enumerating all axioms of this kind, we apply Knuth-Bendix Completion to the axioms. We first look at whether they would terminate. Due to limited computational capacity, we only look at the first 100 axioms and compare their theorems given different time constraint.
A1 is the list with time constraint 1 second, and A2 is the list with time constraint 2 seconds. 98 out of 100 terminates in 2 seconds, which shows that termination is a common feature for Knuth-Bendix Completion.
A1 is the list with time constraint 1 second, and A2 is the list with time constraint 2 seconds. 98 out of 100 terminates in 2 seconds, which shows that termination is a common feature for Knuth-Bendix Completion.
A1=Table[Length[LocalSymbol["A1"][[i]]["Theorems"]],{i,100}];A10=Table[Length[LocalSymbol["A10"][[i]]["Theorems"]],{i,100}];
In[]:=
Count[Table[A1[[i]]>=A10[[i]]-5,{i,100}],True]
Out[]=
98
We now plot the number of theorems in a histogram.
In[]:=
Histogram[Table[Length[A0[[i]]["Theorems"]],{i,960}]]
Out[]=
Comparing the graph to the histogram of number of theorems to existing axiomatic theories, we find that it’s significantly smaller, so we select those axioms with number of theorems greater than 50, because they resembles real world axiom systems more and see what their proof graphs look like. 295 out of 960 axiom systems have more than 50 theorems. These are three examples.
In[]:=
Grid[{Table[A11[[i]]["Axioms"],{i,3}],Table[A11[[i]]["ProofGraph"],{i,3}]},FrameAll]
Out[]=
∀ a.,b. | ∀ a.,b. | ∀ a.,b. |
They have very similar structures with the proof graph of known systems: the complexity and the same end point. Below are some of the proof graphs with theorems less than 5. Some have many proof steps (like the first one), but demonstrates repetitiveness.
In[]:=
A12=Select[A0,Length[#["Theorems"]]<5&];Grid[{Table[A12[[i]]["Axioms"],{i,4}],Table[A12[[i]]["ProofGraph"],{i,4}]},FrameAll]
Out[]=
∀ a.,b. | ∀ a.,b. | ∀ a.,b. | ∀ a.,b. |
Based on these graphs we make a conjecture that number of theorems in Knuth Bendix Completion entails their graphical structure, and therefore can reveal desirability for an axiom system.
Concluding Remarks and Future Plans
Concluding Remarks and Future Plans
This project is an attempt to present a possible scheme for classifying the axiom system that we could potentially be interested in. It turns out that the number of theorems derived from Knuth-Bendix Completion could be an indicator. With this method, we narrow the pool of axioms from 960 to 295. However, we have only investigated a certain set of theorems, but there are many other systems in the wild.
The future goal is to apply this similar method to other more complex axiom systems, as well as to look for other graph properties other than the number of theorems to improve the filter for desirable axiom systems. The topological property of rewrite entailment cone or Knuth-Bendix
The future goal is to apply this similar method to other more complex axiom systems, as well as to look for other graph properties other than the number of theorems to improve the filter for desirable axiom systems. The topological property of rewrite entailment cone or Knuth-Bendix
Keywords
Keywords
◼
Metamathematics
◼
Rewrite System
◼
Knuth-Bendix Completion
Acknowledgment
Acknowledgment
Mentor: James Boyd, Nikolay Murzin
I am expressing my sincere gratitude to James Boyd and Nikolay Murzin for being extremely supportive. This project is impossible without them. They helped me devised this interesting topic and pointed out the possible directions that this can be further developed. I would like to specially thank to Nikolay Murzin who helped me a lot with coding in Wolfram Language.
I am expressing my sincere gratitude to James Boyd and Nikolay Murzin for being extremely supportive. This project is impossible without them. They helped me devised this interesting topic and pointed out the possible directions that this can be further developed. I would like to specially thank to Nikolay Murzin who helped me a lot with coding in Wolfram Language.
References
References
◼
The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics https://writings.stephenwolfram.com/2022/03/the-physicalization-of-metamathematics-and-its-implications-for-the-foundations-of-mathematics/#top
◼
Knuth-Bendix Completion Algorithm https://mathworld.wolfram.com/Knuth-BendixCompletionAlgorithm.html