This report defines a hole for the proof space arising in multiway system graphs generated by string-substitution rules. A proof is a path from an initial string to a target string (the initial and final string is a theorem) in the graph.  By contracting each proof to a single vertex and connecting two proofs when they differ in exactly one step (when they form a single diamond sub-graph), at the end it constructs a proof graph whose connectedness tells the fact of continuously deforming one proof into another.  A hole is defined as follows: #Holes = #ConnectedComponents - 1
Adding new symbols or asymmetric rules quickly introduces holes.

Homotopies in multiway system graphs

Goal: We aim to study the process of reaching theorems, not just the theorems themselves. We will do this by directly examining the structure of the proof space.
Consider the rule set {A->BBB, BB->A} and the theorem A->ABA. To find all possible proofs, we must first identify a path from A to ABA in the multiway system.

With[{g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"BBB","BB"->"A"},"A",8,AspectRatio->1.5]},HighlightGraph[g,Style[PathGraph[FindShortestPath[g,"A","ABA"],DirectedEdges->True],({{"[◼]", "MetamathematicsStyleData" }})["ProofPathStyle"],Arrowheads[.04],Thick]]]

In this particular case, there are 20 distinct paths (also called proofs for this theorem A->ABA)

With[{g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"BBB","BB"->"A"},"A",7,VertexShapeFunction->Automatic,EdgeStyle ->Directive[ Arrowheads[.1],Darker[ResourceFunction["WolframPhysicsProjectStyleData"]["StatesGraph", "EdgeStyle"]]],AspectRatio->1.5,ImageSize->50]},HighlightGraph[g,Style[PathGraph[#,DirectedEdges->True],({{"[◼]", "MetamathematicsStyleData" }})["ProofPathStyle"],Thickness[0.05]]]&/@FindPath[g,"A","ABA",All,All]]

All these different proofs, can in a sense, be continuously deformed into each other. Therefore, we need to define what makes a proof be continuously deformed into another one, in this case we do that by progressively changing just one step at a time. In this case, the proofs are equivalent. This starting point will later serve as a baseline against which finer topological structures on proof space can be compared.

Now consider the rule {A ->AA, A -> BAAB} . With this axiom system, there are 15 possible proofs for the theorem A ->BAABAABAAB :

The proofs on the left side cannot be continuously deformed into the proofs on the right side. This indicates the presence of a topological “hole” between these two groups of proofs (that is, a non-trivial loop separating the two clusters of proofs). 
Observations: Note that the existence and nature of such holes depend crucially on the particular theorem under investigation.

Brainstorm

Defining “no holes” and “holes” in the proof space

g=Graph[With[{g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"AA","A"->"BAAB"},"A",5,VertexShapeFunction->Automatic]},HighlightGraph[g,Style[PathGraph[#,DirectedEdges->True],({{"[◼]", "MetamathematicsStyleData" }})["ProofPathStyle"],Arrowheads[0],Thick]&/@FindPath[g,"A","BAABAABAAB",All,All]]],AspectRatio->1/2,ImageSize->Full];
diamVertices={"AA","BAABA","BAABAA","AAA"};
closed=Append[diamVertices,First[diamVertices]];
coords=GraphEmbedding[g];                       (*posiciones fijas*)
pos=AssociationThread[VertexList[g]->coords];
rombo=Graphics[{Opacity[0.25],Blue,Polygon[pos/@closed]}];
path1={"A","AA","AAA","BAABAA"};          (*rojo*)
path2={"A","AA","BAABA","BAABAA"};          (*verde*)

edges1=MapThread[DirectedEdge,{Most[path1],Rest[path1]}];
edges2=MapThread[DirectedEdge,{Most[path2],Rest[path2]}];
base=Graph[g,VertexCoordinates->coords];
grafico=HighlightGraph[base,{Style[edges1,Blue,Thick],(*ruta 1*)Style[edges2,Green,Thick]    (*ruta 2*)}];
Show[rombo,grafico,ImageSize->Full]

G=Graph[With[{g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"AA","A"->"BAAB"},"A",5]},GraphUnion@@(PathGraph[#,DirectedEdges->True]&/@FindPath[g,"A","BAABAABAAB",All,All])],VertexShapeFunction->({{"[◼]", "MetamathematicsStyleData" }})["StateVertexShapeFunction"],EdgeStyle->Directive[({{"[◼]", "MetamathematicsStyleData" }})["ProofPathStyle"],Arrowheads[.04],Thick],
PerformanceGoal->"Quality"];
diamVertices={"AA","BAABA","BAABAA","AAA"};
closed=Append[diamVertices,First[diamVertices]];
coords=GraphEmbedding[G];                       (*posiciones fijas*)
pos=AssociationThread[VertexList[G]->coords];
rombo=Graphics[{Opacity[0.25],Blue,Polygon[pos/@closed]}];
path1={"A","AA","AAA","BAABAA"};          (*rojo*)
path2={"A","AA","BAABA","BAABAA"};          (*verde*)

edges1=MapThread[DirectedEdge,{Most[path1],Rest[path1]}];
edges2=MapThread[DirectedEdge,{Most[path2],Rest[path2]}];
base=Graph[G,VertexCoordinates->coords];
grafico=HighlightGraph[base,{Style[edges1,Blue,Thick],(*ruta 1*)Style[edges2,Green,Thick]    (*ruta 2*)}];
Show[rombo,grafico,ImageSize->Full]

The main task is to define precisely what it means for the proof space to have a hole. Before studying the theorem A  BAABAABAAB, we begin by examining a simpler theorem: A  BAABAA, for which we want to prove that no holes exist in its proof space. In this case, there are only two distinct proofs for the theorem. We contract each path into a single node to build a new graph the proof graph for this theorem (the graph of every possible proof for the theorem). We then define an edge between two nodes if the corresponding proofs differ by exactly one diamond. 

The resulting graph may be connected, or disconnected. If it is connected we say that the topological space of proofs for this theorem has no holes, meaning every proof could be continuously deformed into any other. Essentially, the proof space is path-connected and can be considered as having a single equivalence class of proofs. 

On the other hand, if the graph is disconnected, this indicates the presence of a hole in the proof space, separating distinct classes of proofs.

At the end this would be the resulting graph for the theorem A  BAABAA.

Graph[{"P1"<->"P2"},VertexStyle->{"P1"->Blue,"P2"->Green},VertexLabels->Placed["Name",Above]]

And now we have a first definition to count the number of holes in a theorem: metatheorem: (#Holes) = (#connected components) - 1

Let' s look at the next example whose rule is {A->BBB, BB -> A} and think about the theorem A  AA.

g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"BBB","BB"->"A"},"A",5,AspectRatio->1.5]

A=With[{g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"BBB","BB"->"A"},"A",6,VertexShapeFunction->Automatic,EdgeStyle ->Directive[ Arrowheads[.1],Darker[ResourceFunction["WolframPhysicsProjectStyleData"]["StatesGraph", "EdgeStyle"]]],AspectRatio->1.5,ImageSize->100]},HighlightGraph[g,Style[PathGraph[#,DirectedEdges->True],({{"[◼]", "MetamathematicsStyleData" }})["ProofPathStyle"],Thickness[0.03]]]&/@FindPath[g,"A","AA",All,All]]

{P1,P2,P3,P4}

There are four different proofs for this theorem. Look at the first two paths  P1 (red), P2 (blue) and overlap them in different colors:

PromboEdges={DirectedEdge["A","BBB"],DirectedEdge["BBB","BA"],DirectedEdge["BA","BBBB"],DirectedEdge["BBA","AA"]};
P2romboEdges={DirectedEdge["BBBB","ABB"],DirectedEdge["ABB","AA"]};
HighlightGraph[g,{Style[Subgraph[g,PromboEdges],Red,Thickness[0.009]],Style[Subgraph[g,P2romboEdges],Blue,Thickness[0.009]]}]

Note that the two paths draw a diamond (BBBB,BBA,AA,ABB):

coords=GraphEmbedding[g];
pos=AssociationThread[VertexList[g]->coords];
diamVertices={"BBBB","BBA","AA","ABB"};
Show[Graph[g,VertexCoordinates->coords],Graphics[{Opacity[0.2],Blue,Polygon[pos/@diamVertices]}],HighlightGraph[g,{Style[Subgraph[g,PromboEdges],Red,Thickness[0.009]],Style[Subgraph[g,P2romboEdges],Blue,Thickness[0.009]]}]]

So the two paths P1,P2 are contracted in two nodes and since they form only one diamond. In the resulting graph they are connected:

Graph[{"P1"<->"P2"},VertexStyle->{"P1"->Red,"P2"->Blue},VertexLabels->Placed["Name",Above]]

Do the same with the other proofs P3 (green), P4 (Orange) and overlap them in different colors:

PromboEdges={DirectedEdge["A","BBB"],DirectedEdge["BBB","AB"],DirectedEdge["AB","BBBB"],DirectedEdge["BBA","AA"]};
P2romboEdges={DirectedEdge["BBBB","ABB"],DirectedEdge["ABB","AA"]};
Show[Graph[g,VertexCoordinates->coords],Graphics[{Opacity[0.0001],Blue,Polygon[pos/@diamVertices]}],HighlightGraph[g,{Style[Subgraph[g,PromboEdges],Green,Thickness[0.03]],Style[Subgraph[g,P2romboEdges],Orange,Thickness[0.04]]}],Graph[g,VertexCoordinates->coords],Graphics[{Opacity[0.19],Blue,Polygon[pos/@diamVertices]}]]

Graph[{"P3"<->"P4"},VertexStyle->{"P3"->Green,"P4"->Orange},VertexLabels->Placed["Name",Above]]

And by doing the same process with P4,P2 and P1,P3 we complete the graph:

difierenPorUnoQ[c1_,c2_]:=Module[{dif1,dif2},dif1=Complement[c1,c2];dif2=Complement[c2,c1]; Length[dif1]+Length[dif2]==2];
Ru={"A"->"BBB","BB"->"A"}(*Rule*);
St="A"(*Start*);
Dn=5(*Degree of the graph (times we apply the rule)*);
g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[Ru,St,Dn,VertexShapeFunction->Automatic,AspectRatio->1/2,ImageSize->Full];
vertices=VertexList[g];(*obtenemos todos los nodos de la gráfica*)
lastNodes=Select[vertices,VertexOutDegree[g,#]==0&]; (*obtenemos los últimos nodos de la gráfica*)
caminos=Table[FindPath[g,St,ToString[lastNodes[[i]]],All,All],{i,Length[lastNodes]}];(*lista donde cada elemento tiene todas las pruebas de un teorema*)
pares=Table[Subsets[Range[Length[caminos[[i]]]],{2}],{i,Length[caminos]}];(*todos los subconjuntos de dos elementos 2 elementos que se pueden formar con la cantidad de caminos del i-esimo teorema*)
aristasGPi=Table[Select[pares[[i]],difierenPorUnoQ[caminos[[i]][[#[[1]]]],caminos[[i]][[#[[2]]]]]&],{i,Length[caminos]}];(*aplico el algoritmo*)
pathLabels=Table[Table["P"<>ToString[j],{j,Length[caminos[[i]]]}],{i,Length[caminos]}];
G=With[{verts=Range[Length[caminos[[1]]]],
        labels=Thread[Range[Length[caminos[[1]]]]->pathLabels[[1]]],
        edges=UndirectedEdge@@@aristasGPi[[1]]},
    Graph[verts,edges,VertexLabels->labels]]

Import["C:\\Users\\saull\\Downloads\\animation.gif","AnimatedImage",ImageSize->Medium]

We compute (#Holes = #ConnectedComponets - 1) and we get that the number of holes for this particular theorem is 0. This discovery is quite impressive since it is telling us not only that the theorem has no holes, but which is the continuous path to go from one proof to another proof by changing one step at a time. 

Now we know how to search for holes, let’s launch the algorithm and let’s apply the algorithm to the theorem: A  ABA. First we plot de graph.

g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"BBB","BB"->"A"},"A",7,AspectRatio->1.5]

With[{g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[{"A"->"BBB","BB"->"A"},"A",7,VertexShapeFunction->Automatic,EdgeStyle->Directive[Arrowheads[.1],Darker[ResourceFunction["WolframPhysicsProjectStyleData"]["StatesGraph","EdgeStyle"]]],AspectRatio->1.5,ImageSize->50]},GraphicsRow[MapIndexed[Labeled[HighlightGraph[g,Style[PathGraph[#1,DirectedEdges->True],({{"[◼]", "MetamathematicsStyleData" }})["ProofPathStyle"],Thickness[0.05]]],Style["P"<>ToString[#2[[1]]],Bold]]&,FindPath[g,"A","ABA",All,All]],10,ImageSize->1300]]

Then convert every path into a node and construct the edges by using the relation “two paths are connected if the proofs are different in only one step”. And we obtain the graph, which only has a connected component, then this theorem has no holes. It is amazing that the new graph is telling us which is the metapath to go from one proof to another one continuously.

caminos=FindPath[g,"A","ABA",All,All];nuevosNodos=Table["P"<>ToString[i],{i,Length[caminos]}];pares=Subsets[Range[Length[caminos]],{2}];
aristasPi=Select[pares,difierenPorUnoQ[caminos[[#[[1]]]],caminos[[#[[2]]]]]&];GraphPlot3D[UndirectedEdge@@@aristasPi,VertexLabels->Thread[Range[Length[nuevosNodos]]->nuevosNodos]]

Now we are ready to solve the initial problem we were asked by applying the algortihm, let’s show the theorem A  BAABAABAAB has a hole:

This is the resulting graph after applying the algortim, #holes = #ConnectedComponents - 1 = 2-1=1. So this theorem, actually, as we have thought has a hole.

difierenPorUnoQ[c1_,c2_]:=Module[{dif1,dif2},dif1=Complement[c1,c2];dif2=Complement[c2,c1]; Length[dif1]+Length[dif2]==2];
Ru={"A"->"AA","A"->"BAAB"}(*Rule*);
St="A"(*Start*);
Dn=5(*Degree of the graph (times we apply the rule)*);
g=({{"[◼]", "TwoWayRuleStringNestGraph" }})[Ru,St,Dn,VertexShapeFunction->Automatic,AspectRatio->1/2,ImageSize->Full];
caminos=FindPath[g,St,"BAABAABAAB",All,All];
pares=Subsets[Range[Length[caminos]],{2}];
aristasGP=Select[pares,difierenPorUnoQ[caminos[[#[[1]]]],caminos[[#[[2]]]]]&];
pathLabels=Table["P"<>ToString[j],{j,Length[caminos]}];
G=With[{verts=Range[Length[caminos]],labels=Thread[Range[Length[caminos]]->pathLabels],edges=UndirectedEdge@@@aristasGP},Graph[verts,edges,VertexLabels->labels]]

The easiest hole

It is a bit harder to find a "simple" graph that contains a hole (a theorem for which at least one proof cannot be converted into another by switching at most one step). To understand what a hole looks like, we will take a shortcut and show the simplest graph (which does not come from a rule) that contains a hole.

g=Graph[{Style[DirectedEdge["A","B"],Darker[Red]],Style[DirectedEdge["B","D"],Darker[Red]],DirectedEdge["A","E"],DirectedEdge["E","F"],DirectedEdge["F","D"]},VertexLabels->"Name",EdgeLabels->{DirectedEdge["A","B"]->"P1",DirectedEdge["A","E"]->"P2"},GraphLayout->"LayeredDigraphEmbedding"]

suppose we want to prove the theorem A⟹D, the are two proofs we could use to do so . P1 (the red path) and P2 (the blue path), we cannot convert the proof P1 to the proof P2 since they do not draw a diamond, they are different by two steps, so we could say that the theorem A  B has a hole.

Spreading the concept

Once we have defined what the meaning of a hole in a theorem means, we can search for holes in graphs by searching for every possible theorem in a graph and computing how many theorems have holes (and how many holes they have).

Interpretation and application

Pythagorean theorem

When we want to prove a theorem, we can do so by using many different ways and using different areas in mathematics, for instance, algebra, topology, real analysis, complex analysis... Suppose we want to prove the Pythagorean theorem, and we do it by using these proofs: 
Let  be right–angled at . Denote the legs by ,  and the hypotenuse by . Draw the altitude  to the hypotenuse, meeting  at ; set  and , so .

Proof, here are the steps that first and second proofs share:
STEP 1: The right triangle ABC is given.
STEP 2: Construct altitude CD to side AB, defining  as above.
STEP 3: Triangles ABC, ACD and CBD are pairwise similar (angle–angle criterion).
Combining the results of Step 4 and 5 yields 
STEP 6: Conclusion  Hence the Pythagorean theorem is proved.
For the third proof we have a very different proof.

Module[{a=4,b=3,A,B,C,D,triBase,triLeft,triRight,etiquetaLados,dibLados,dibAreas},C={0,0};
A={0,b};B={a,0};D=A+((C-A).(B-A)/Norm[B-A]^2) (B-A);
triBase=Polygon[{A,B,C}];triLeft=Polygon[{A,C,D}];triRight=Polygon[{B,C,D}];
(*Etiquetas de puntos y longitudes*)etiquetaLados={Text[Style["A",Bold],A,{-3,0}],Text[Style["B",Bold],B,{3,-3}],Text[Style["C",Bold],C,{-3,3}],Text[Style["D",Bold],D,{0,-1.5}],Text[Style["b",Italic],(A+C)/2+{-0.45,0}],Text[Style["a",Italic],(B+C)/2+{0,-0.35}],Text[Style["c",Italic],(A+B)/2+{0,0.35}]};
dibLados=Graphics[{LightGray,triBase,(*triángulo completo*)Thick,(*contornos resaltados*)Red,Line[{A,C}],(*lado AC (b)*)Blue,Line[{C,B}],(*lado BC (a)*)Black,Line[{A,B}],(*hipotenusa AB (c)*)Dashed,Line[{C,D}],(*altura CD*)etiquetaLados},ImageSize->300,Frame->False];
dibAreas=Graphics[{Opacity[0.25,LightBlue],triLeft,(*ΔACD*)Opacity[0.25,LightGreen],triRight,(*ΔCBD*)LightGray,EdgeForm[Directive[Black,Thick]],triBase,Dashed,Line[{C,D}],etiquetaLados},ImageSize->300,Frame->False];
(*Mostrar ambos dibujos juntos*)Graphics[dibLados]]

1st Proof of Pythagorean theorem (side ratios, geometry) P1

From triangle similarity we have step 4 and step 5:
STEP 4  ,   and
STEP 5        
STEP 6: Adding the two equalities gives

2nd Proof of Pythagorean theorem (area rearrangement, geometry) P2

By similarity, the areas satisfy step 4 and step 5:
STEP 4:  . 
STEP 5: Since ,
        STEP 6: dividing by  yields   .

3rd Proof of Pythagorean theorem (distance formula) P3

Place the triangle with vertices
STEP 2: 
 STEP 3: The legs lie along the coordinate axes, so their lengths are  and  .
 STEP 4: The hypotenuse is the segment ; its length is
.
STEP 5: Squaring both sides gives  .

Let’s see how pythagorean theorem is represented by using graphs. The proof space for the Pythagorean theorem is:

camino1=PathGraph[{"STEP1","STEP2","STEP3","STEP4P1","STEP5P1","STEP6"},DirectedEdges->True];
camino2=PathGraph[{"STEP3","STEP4P2","STEP5P2","STEP6"},DirectedEdges->True];
camino3=PathGraph[{"STEP1","STEP2P3","STEP3P3","STEP4P3","STEP5P3","STEP6"},DirectedEdges->True];
todosLosArcos=Union@@(EdgeList/@{camino1,camino2,camino3});
g=Graph[todosLosArcos,VertexLabels->"Name",GraphLayout->{"LayeredEmbedding","RootVertex"->"STEP1"},ImageSize->Large];
HighlightGraph[g,{Style[camino1,Thick],Style[camino2,Orange,Thick],Style[camino3,Brown,Thick]}]

Then, by using the algoritm we developed before, we have that the resulting graph is:

g=Graph[{"P1","P2","P3"},{},VertexLabels->"Name",VertexStyle->{"P2"->Orange,"P3"->Brown},GraphLayout->"CircularEmbedding",ImageSize->300]

We conclude that, if we only use these three proofs, the pythagorean theorem has 2 holes.

Main results and examples

difierenPorUnoQ[c1_,c2_]:=Module[{dif1,dif2},dif1=Complement[c1,c2];dif2=Complement[c2,c1]; Length[dif1]+Length[dif2]==2];
TwoWayRuleAnalysis[rules_, initialState_, evolutionSteps_, shapeQ_:True]:= Block[
{graph=({{"[◼]", "TwoWayRuleStringNestGraph" }})[rules,initialState,evolutionSteps,AspectRatio->1/2,ImageSize->Full, If[shapeQ, Nothing, VertexShapeFunction->Automatic]],
vertices, lastNodes, paths, pairs, aristasGPi, pathLabels},

vertices = VertexList[graph];
lastNodes= Select[vertices, VertexOutDegree[graph, #]==0&];
paths = Table[FindPath[graph,initialState,ToString[lastNodes[[i]]],All,All],{i,Length[lastNodes]}];
pairs = Table[Subsets[Range[Length[paths[[i]]]],{2}],{i,Length[paths]}];
aristasGPi =Table[Select[pairs[[i]],difierenPorUnoQ[paths[[i]][[#[[1]]]],paths[[i]][[#[[2]]]]]&],{i,Length[paths]}];
pathLabels = Table[Table["P"<>ToString[j],{j,Length[paths[[i]]]}],{i,Length[paths]}];

TwoWayRuleObject[<|
"InitialState"->initialState,
"Graph"->graph,
"Vertices"->vertices, 
"LastNodes"->lastNodes, 
"Paths"->paths,
"Pairs"->pairs,
"AristasGPi"->aristasGPi,
"PathLabels"->pathLabels|>]
];


TwoWayRuleObject[data_]["Graph"]:=data["Graph"];
TwoWayRuleObject[data_]["LastNodes"]:= data["LastNodes"];
TwoWayRuleObject[data_]["TheoremsManipulate",PathLabel_:True]:=Module[
{
paths = Lookup[data, "Paths"],
aristasGPi = Lookup[data, "AristasGPi"],
pathLabels = Lookup[data, "PathLabels"]
},

Function[{p, pl, agpi},
Animate[
  With[
{
verts=Range[Length[p[[i]]]],
labels=Thread[Range[Length[p[[i]]]]->pl[[i]]],
edges=UndirectedEdge@@@agpi[[i]]
},
Labeled[#,StringTemplate["Number of holes: `1`"][Length[ConnectedComponents[#]]-1]]&@
Graph[verts,edges,VertexLabels->If[PathLabel,labels,None]]
],
  {{i,1,"Theorem Index"},1,Length[agpi],1,Appearance->"Labeled"}]
][paths, pathLabels, aristasGPi]
]

Example of graphs whose theorems have no holes

Let’ s analyze a simple example: let the rule be {A->B, B -> AA} and let’s start the graph at A. Note that we have only two rules and the initial condition is just one letter, “A”. We apply the rules 7 times. Notice that the graph generates every possible theorem (there are 5 possible theorems) and every possible proof. Then, we apply the algorithm to determine how many holes each theorem has. In the end, we see that the number of holes in every theorem is zero. The “density” of the graph increases each time we apply the rules, so we will never find a hole.

Ru1={"A"->"B","B"->"AA"};
St1="A";
Dn1=7;
g1=({{"[◼]", "TwoWayRuleStringNestGraph" }})[Ru1,St1,Dn1,AspectRatio->1.5]
vertices1=VertexList[g1];
lastNodes1=Select[vertices1,VertexOutDegree[g1,#]==0&]; 
caminos1=Table[FindPath[g1,St1,ToString[lastNodes1[[i]]],All,All],{i,Length[lastNodes1]}];
pares1=Table[Subsets[Range[Length[caminos1[[i]]]],{2}],{i,Length[caminos1]}];
aristasGPi1=Table[Select[pares1[[i]],difierenPorUnoQ[caminos1[[i]][[#[[1]]]],caminos1[[i]][[#[[2]]]]]&],{i,Length[caminos1]}];
pathLabels1=Table[Table["P"<>ToString[j],{j,Length[caminos1[[i]]]}],{i,Length[caminos1]}];
A=Manipulate[With[{g1=({{"[◼]", "TwoWayRuleStringNestGraph" }})[Ru1,St1,Dn1,VertexShapeFunction->Automatic,EdgeStyle ->Directive[ Arrowheads[.1],Darker[ResourceFunction["WolframPhysicsProjectStyleData"]["StatesGraph", "EdgeStyle"]]],AspectRatio->1.5,ImageSize->100]},HighlightGraph[g1,Style[PathGraph[#,DirectedEdges->True],({{"[◼]", "MetamathematicsStyleData" }})["ProofPathStyle"],Thickness[0.03]]]&/@FindPath[g1,St1,ToString[lastNodes1[[i]]],All,All]],{i,Length[lastNodes1]},SaveDefinitions->True]
G1=Manipulate[With[{verts=Range[Length[caminos1[[i]]]],labels=Thread[Range[Length[caminos1[[i]]]]->pathLabels1[[i]]],edges=UndirectedEdge@@@aristasGPi1[[i]]},Graph[verts,edges,VertexLabels->labels]],{i,1,Length[aristasGPi1],1,Appearance->"Labeled"},SaveDefinitions->True]

In the next example we are giving again the same two rules but this time the initial conditions are two letter “AB”, and we are applying the rule 7 times, note again that the “density” of the graph becomes bigger very fast once again, so we are never going to find a hole.

TwoWayRuleAnalysis[{"A"->"B","B"->"AA"}, "AB", 6,False]["Graph"]

TwoWayRuleAnalysis[{"A"->"B","B"->"AA"}, "AB", 6,False]["TheoremsManipulate"];(*If you want to see dynamic content, download this notebook and uncomment this line of code.*)

These are the resulting graphs after applyng the algorithm

({{, , , , , , , , }})

Import["C:\\Users\\saull\\Downloads\\ABBAA.AB.6R.gif","AnimatedImage",ImageSize->Small(*change to Medium so you can see the plot*)]

Example of graphs whose theorems have holes

Let’s make a hole, we give two rules {A->BB, B -> AA} with initial condition “ABA”, note that holes begin to appear by applying the rule five times.

TwoWayRuleAnalysis[{"A"->"BB","B"->"AA"}, "ABA", 5,False]["Graph" ]

TwoWayRuleAnalysis[{"A"->"BB","B"->"AA"}, "ABA", 5,False]["TheoremsManipulate" ];(*If you want to see dynamic content (and prettier), download the notebook uncomment this line of code.*)

Import["C:\\Users\\saull\\Downloads\\ABBBAA.ABA.5R.gif","AnimatedImage",ImageSize->Small(*change to Medium so you can see the plot*)]

Now begin with three rules {A ->  BC, B ->  AA, C -> A} (we are adding a new letter) and initial condition of only one letter, let’s apply the rule seven times

TwoWayRuleAnalysis[{"A"->"BC","B"->"AA","C"->"A"}, "A", 7,False]["Graph" ]

TwoWayRuleAnalysis[{"A"->"BC","B"->"AA","C"->"A"}, "A", 7,False]["TheoremsManipulate" ];(*If you want to see dynamic content (and prettier), download the notebook uncomment this line of code.*)

Import["C:\\Users\\saull\\Downloads\\ABCBAACA.A7.gif","AnimatedImage",ImageSize->Small(*change to Medium so you can see the plot*)]

Now three rules but this time {A -> BC, B -> AA, C -> A}, the initial condition is one letter longer

TwoWayRuleAnalysis[{"A"->"BC","B"->"AA","C"->"A"}, "AB", 7,False]["Graph" ]

TwoWayRuleAnalysis[{"A"->"BC","B"->"AA","C"->"A"}, "AB", 7,False]["TheoremsManipulate" ];(*If you want to see dynamic content (and prettier), download the notebook uncomment this line of code.*)

Import["C:\\Users\\saull\\Downloads\\ABCBAACA.AB7.gif","AnimatedImage",ImageSize->Small(*change to Medium so you can see the plot*)]

Concluding Remarks

An important observation is that we can begin formulating metatheorems—statements about the structure of the proof space itself. For instance: given any set of two or more rewriting rules, there exist a natural number 𝑛 and an appropriate initial condition such that the resulting proof space contains holes.

Acknowledgments

Thank to Philip Maymin for his guidance during the WSS and I would like to thank also Hugo Suárez and Alejandra Ortiz for their support throughout the development of this notebook. I deeply appreciate their time. This notebook would not have been possible without their help.

References

S. Wolfram (2022), “The Physicalization of Metamathematics and Its Implications for the Foundations of Mathematics” Wolfram Science. https://www.wolframscience.com/metamathematics/.

Ž. Virk,  (2022), Introduction to Persistent Homology. University of Ljubljana.

Cite This Notebook

“Searching for holes in the proof space”
by Saúl Bernal González
Wolfram Community, 09/07/2025
https://community.wolfram.com/web/sauldurdenbateman