Abstract
The goal of this project is to advance our understanding of axiom systems by methodically enumerating possible axiom systems and computing their entailment cones under both non-accumulative and accumulative conditions. By utilizing substitution and co-substitution techniques from various initial conditions, we aim to explore the structural properties of these systems.
The entailment cones, which represent the space of consequences derivable from a set of axioms, are analyzed to uncover their topological features. To achieve this, we will enumerate proof paths within these cones and apply methods from homology and homotopy theory to provide a deeper topological insight. This approach allows for a comprehensive examination of the interplay between different axiom systems and their logical consequences. Through this analysis, we seek to map out the intricate landscape of axiom systems, shedding light on their foundational structure and the nature of their derivable truths. The project will contribute to the broader field of mathematical logic and theoretical computer science, offering new perspectives on the formulation and implications of axiomatic systems.
The goal of this project is to advance our understanding of axiom systems by methodically enumerating possible axiom systems and computing their entailment cones under both non-accumulative and accumulative conditions. By utilizing substitution and co-substitution techniques from various initial conditions, we aim to explore the structural properties of these systems.
The entailment cones, which represent the space of consequences derivable from a set of axioms, are analyzed to uncover their topological features. To achieve this, we will enumerate proof paths within these cones and apply methods from homology and homotopy theory to provide a deeper topological insight. This approach allows for a comprehensive examination of the interplay between different axiom systems and their logical consequences. Through this analysis, we seek to map out the intricate landscape of axiom systems, shedding light on their foundational structure and the nature of their derivable truths. The project will contribute to the broader field of mathematical logic and theoretical computer science, offering new perspectives on the formulation and implications of axiomatic systems.
Introduction
In pure mathematics, our overarching aim is to establish the foundational theorems that underpin further mathematical developments. These foundational theorems serve as essential building blocks for a wide array of mathematical structures and concepts. The primary objective is the formulation and comprehension of these theorems, rather than merely focusing on the specific proofs that derive them. While this approach may initially appear counterintuitive, it is essential to recognize the distinctive nature of metamathematics.
Metamathematics, a branch of mathematical logic, prioritizes the study of theorems and the formal systems that produce them. The main goal in metamathematics is not just to prove individual theorems but to analyze and understand the overall structure and properties of theorems within a given formal system. This involves examining the processes by which theorems are derived, including the rules of inference, axioms, and the logical frameworks employed.
In this project, we aim to contribute to the field of metamathematics by exploring axiom systems and their entailment cones, both non-accumulative and accumulative, through the use of substitution and co-substitution techniques from different initial conditions. By enumerating possible axiom systems and computing their entailment cones, we intend to uncover the structural and topological characteristics of these systems. We will enumerate proof paths within these cones and apply methods from homology and homotopy theory to gain deeper insights into their topological features. This approach will help us understand the intricate landscape of axiom systems and the logical consequences they produce, thereby shedding light on the nature of mathematical truth and the process of theorem generation.
Our work aims to bridge the gap between pure mathematics and metamathematics, providing a comprehensive framework for studying the structure of theorems and the processes by which they are derived. This, in turn, will enhance our understanding of the foundations of mathematics and contribute to the advancement of mathematical logic and theoretical computer science.
Specifically, the goal of this project is to understand simple axiom systems by laying the groundwork for how theorems are solved. We employ a two-way system with arbitrary rules defined from A ⟷ A to BBB⟷BBB. By utilizing a proof path graph through multiple iterations, we generate various sample types where cycles are defined through a cycle graph, outlining the proofs. Using a graph union, we identify all cycles attached to the base axiom, thereby proving the structure and revealing its topological features. Subsequently, the entailment cone is computed using both substitution and co-substitution from different initial conditions.
Metamathematics, a branch of mathematical logic, prioritizes the study of theorems and the formal systems that produce them. The main goal in metamathematics is not just to prove individual theorems but to analyze and understand the overall structure and properties of theorems within a given formal system. This involves examining the processes by which theorems are derived, including the rules of inference, axioms, and the logical frameworks employed.
In this project, we aim to contribute to the field of metamathematics by exploring axiom systems and their entailment cones, both non-accumulative and accumulative, through the use of substitution and co-substitution techniques from different initial conditions. By enumerating possible axiom systems and computing their entailment cones, we intend to uncover the structural and topological characteristics of these systems. We will enumerate proof paths within these cones and apply methods from homology and homotopy theory to gain deeper insights into their topological features. This approach will help us understand the intricate landscape of axiom systems and the logical consequences they produce, thereby shedding light on the nature of mathematical truth and the process of theorem generation.
Our work aims to bridge the gap between pure mathematics and metamathematics, providing a comprehensive framework for studying the structure of theorems and the processes by which they are derived. This, in turn, will enhance our understanding of the foundations of mathematics and contribute to the advancement of mathematical logic and theoretical computer science.
Specifically, the goal of this project is to understand simple axiom systems by laying the groundwork for how theorems are solved. We employ a two-way system with arbitrary rules defined from A ⟷ A to BBB⟷BBB. By utilizing a proof path graph through multiple iterations, we generate various sample types where cycles are defined through a cycle graph, outlining the proofs. Using a graph union, we identify all cycles attached to the base axiom, thereby proving the structure and revealing its topological features. Subsequently, the entailment cone is computed using both substitution and co-substitution from different initial conditions.
Section I: Accumulative Entailment Structures
The entailment is a fundamental concept that describes the logical relationship between statements that hold the premise of either being true or false and that yields a valid argument in-which the conclusion of said logical argument holds logical structures that are built upon. From this, there can only be a conclusion that is entailed by its premise; this is because such a conclusion would have to hold a premise because of being a logical argument.
Partially explained earlier in the introduction, these are the rules stated below. The rules are the axiom systems that contain the two-way systems that will be used and define the experiment. First off, the code used defines axioms 1 through 196 (it should be noted for later reference that as we use these axioms, not all of them will be used), which for this case is used throughout this study. These rules list all axiom systems going down the list. These axioms will further the study as we continue in Section II by using these axioms’ proof graphs. These are the basis for the project and are used for the theorems.
Out[]=
AA | AB | AAA | AAB | ABA | ABB | AAAA | AAAB | AABA | AABB |
ABAA | ABAB | ABBA | ABBB | BA | BB | BAA | BAB | BBA | BBB |
BAAA | BAAB | BABA | BABB | BBAA | BBAB | BBBA | BBBB | AAA | AAB |
AAAA | AAAB | AABA | AABB | AAAAA | AAAAB | AAABA | AAABB | AABAA | AABAB |
AABBA | AABBB | ABA | ABB | ABAA | ABAB | ABBA | ABBB | ABAAA | ABAAB |
ABABA | ABABB | ABBAA | ABBAB | ABBBA | ABBBB | BAA | BAB | BAAA | BAAB |
BABA | BABB | BAAAA | BAAAB | BAABA | BAABB | BABAA | BABAB | BABBA | BABBB |
BBA | BBB | BBAA | BBAB | BBBA | BBBB | BBAAA | BBAAB | BBABA | BBABB |
BBBAA | BBBAB | BBBBA | BBBBB | AAAA | AAAB | AAAAA | AAAAB | AAABA | AAABB |
AAAAAA | AAAAAB | AAAABA | AAAABB | AAABAA | AAABAB | AAABBA | AAABBB | AABA | AABB |
Table I: This table shows most cases used in this study with emissions of 101 through 196 for the sake of showcasing.
In[]:=
With{rules=Take[Flatten[With[{strings=Flatten[Table[StringJoin[#]&/@Tuples[{"A","B"},i],{i,1,3}]]},Table[strings[[i]]<->strings[[j]],{i,1,Length[strings]},{j,1,Length[strings]}]]],{6,8}]},Labeled{#},2,"Sorting"->True,ImageSize->Medium,,Text[Style[#,GrayLevel[.4],Medium]]&/@rules
Out[]=
Section II: The Proof Path GraphsThe proof graphs here are based on sample rules 3, 4, 25, 100, 140, and 195. The rules selected have no real value outside showing the proof graphs and showing the interconnection of the axioms with each other. I am sure something well noted in all the sample rules is a small red line. That is simple proof and is not used in spokes graphs to show a cycle. As for the rest of the graphs, they all show the cycles and possibilities that show the axioms that make a theorem. In later sections, we will even take a random sample and show off the cycles in these graphs that can further show the organization.
I find it intrusting just looking at the graphs how the formal structure is the same as the axioms maintain an exact similar structure; I am not sure why that is, but is it something that I noted in this survey and the fact that these listings prove it must have something to do with the similarities if a rule is closer together, for example, rule 3 and 4 are next to each other, while rule 3 and 195 have hundreds of rules of separation between each other that the similarities are not there.
A good thing to note is the sink vertex. What is the sink vertex? It is the vertex (or node) that is computed (connected) by other vertexes that leads to it being connected. In our case here the vertex sink is where all the edges point to that leads to the answer, which if I take an example case from rule 3 would look like this: AAA AAAA, so the lead vertex ends at the sink, which is the answer.
Just to showcase again rule 3’s proof path again with no labels.
In[]:=
rules=Flatten[With[{strings=Flatten[Table[StringJoin[#]&/@Tuples[{"A","B"},i],{i,1,3}]]},Table[strings[[i]]<->strings[[j]],{i,1,Length[strings]},{j,1,Length[strings]}]]];h={rules[[3]]},3,"Sorting"->True,;vertlist=DeleteCases[DeleteCases[#,_Integer]&/@VertexList[h],x_/;ResourceFunction["ContainsQ"][x,"Event"]];graphs=TableModule{proofs},proofs=/@[h,{rules[[3]]},vertlist[[i]],8];proofgraphs=VertexPop[#,{"Event",___}]&/@proofs;HighlightGraph[GraphUnion@@proofgraphs,proofgraphs],{i,2,Length[vertlist]}
Out[]=
In[]:=
rules=Flatten[With[{strings=Flatten[Table[StringJoin[#]&/@Tuples[{"A","B"},i],{i,1,3}]]},Table[strings[[i]]<->strings[[j]],{i,1,Length[strings]},{j,1,Length[strings]}]]];h={rules[[25]]},3,"Sorting"->True,;vertlist=DeleteCases[DeleteCases[#,_Integer]&/@VertexList[h],x_/;ResourceFunction["ContainsQ"][x,"Event"]];TableModuleh={rules[[25]]},3,"Sorting"->True,,proofs,proofs=/@[h,{rules[[25]]},vertlist[[i]],8];proofgraphs=Graph[#]&/@proofs;HighlightGraph[GraphUnion@@proofgraphs,proofgraphs],{i,2,Length[vertlist]}
Out[]=
Section III: Fundamental group
Spoke graphs shows all cycles possible that are attached at the base axiom, which is really amazing how all this information is compact into such a graph that the inner defined part of the spoke has all this information around it, and how they form the cycles that go around it from the rules. Now, one of the interesting aspects of this graph is how spokes on the graph vary by cycle length as it goes around to complete a circuit and how chaotic it is in its organization.
Concluding Remarks
The summary for the results needs more work, but the present data for cycles suggests that the current results show underlining features that correlate with Boolean and other systems in how proofs are found. Still, I have not done this yet, and want to statistically show the results of which cycles will be are various rules and compare each cycle.
More work needs to be done in collecting large sample sizes and more data on different axiom systems the work needs to ensure that the data has a far larger sample size, as well as trying to establish a theorem for why these axioms in cycles act the way they do. More should be done also to understand in certain cases why disjointed unions exist in a union graph, and establish if it is a mere error, or if something else is going on mathematically. On a personal note, I need to get better at the Wolfram language, but I plan on this march to understand what is going on as I am determined to make this into a proper research paper.
One challenge I failed to complete during the Wolfram Summer program was take the entailment structure and contract equivalences to points and study structure of points, which I am determined to do later.
Keywords
•Two-way
•Proof Paths
•Entailment Cone
•Proof Space
•Cycle
•A lot help was given by James Boyd and Nik Murzin along with Stephen Wolfram for defining the direction of this project.
References
References
•James Boyd for all the help he has given me from coding, to understanding the Wolfram language and taking the time to explain everything from entailment cones to proof paths.
•Nik Murzin for taking time out of his day to join us at weird hours to go over issues both James and I are having with the code I did.
•Wolfram website for aiding me in my coding when not aided by either Nik or James, and for explaining a lot of terms and terminology that I may have missed in the lecture or needed to understand for my project.
CITE THIS NOTEBOOK
CITE THIS NOTEBOOK
A study in proof space Topology
by Richard Charette
Wolfram Community, STAFF PICKS, July 20, 2022
https://community.wolfram.com/groups/-/m/t/2575549
by Richard Charette
Wolfram Community, STAFF PICKS, July 20, 2022
https://community.wolfram.com/groups/-/m/t/2575549