Novel framework for consistency and completeness using multiway isomorphisms
by Kartik Tiwari
Department of Physics and Department of Philosophy, Ashoka University
by Kartik Tiwari
Department of Physics and Department of Philosophy, Ashoka University
A novel framework for discussing the completeness, consistency and decidability of Formal Systems is discussed with the help of Isomorphisms of Multiway systems. To introduce the framework, first, an abstract notion of negation is constructed by referring to entailment preserving subgraph isomorphisms. Further applicability of the introduced framework to study ternary or higher order negation is discussed towards the end of this notebook. The aim of this blog post is not only to contribute towards the development of Wolfram Metamathematics Project but also to create a more transparent method of teaching/understanding abstract formal systems.
“The perception of an isomorphism between two known structures is a significant advance in knowledge-and I claim that it is such perceptions of isomorphism which create meanings in the minds of people.”
― Douglas R. Hofstadter, Gödel, Escher, Bach: An Eternal Golden Braid
“The perception of an isomorphism between two known structures is a significant advance in knowledge-and I claim that it is such perceptions of isomorphism which create meanings in the minds of people.”
― Douglas R. Hofstadter, Gödel, Escher, Bach: An Eternal Golden Braid
Introducing Formal Systems and their Multiway Graphs
Introducing Formal Systems and their Multiway Graphs
Let’s look at the simple example of a string-substitution system. We start with the initial statement and the set of inference rules . Some strings (like ) are such that more than one rule can act on them (like and ). This is what is represented by the branching of the multiway graphs. Each node on the graph represents a theorem that can be proved by tracing the edges of the evolution graph from our initial string to that node. For some theorems, you can trace out multiple different paths back to . The multiplicity of the paths represents different ways to derive that theorem within the formal system. (If you hadn’t noticed already, this particular system demonstrates all the ways in which a randomly arranged string of As, Bs and Cs can be sorted into alphabetic order).
"BAABCA"
{"BA""AB","CB""BC","CA""AC"}
"ABABCA"
"CA""AC"
"BA""AB"
"BAABCA"
In[]:=
ResourceFunction["MultiwaySystem"][{"BA""AB","CB"->"BC","CA"->"AC"},"BAABCA",5,"EvolutionGraph"]
Out[]=
If two formal systems start with the same intial string but have different inference calculus, they may or may not generate the same theorems. In randomly generated formal systems, it is not unlikely that we will find some overlap between the set of theorems of both logics. In the following cell is one notable example. The two different colors represent the paths generated by the rules both acting on “A” (represented as the red node).
{"A""ABB"}and{"A""AB"}
In[]:=
(*tweaking the inbuilt graph union function a little bit*)graphUnion[gs___]:=GraphUnion[gs,EdgeStyleCatenate@MapThread[Thread[Rule[##],List,1]&,{EdgeList/@{gs},AnnotationValue[#,EdgeStyle]&/@{gs}}]]
In[]:=
ex1=ResourceFunction["MultiwaySystem"][{"A""ABB"},"A",7,"StatesGraphStructure",EdgeStyle->Blue];ex2=ResourceFunction["MultiwaySystem"][{"A""AB"},"A",7,"StatesGraphStructure",EdgeStyle->Red];Rotate[HighlightGraph[graphUnion@@{ex1,ex2},"A"],3.14/2]
Out[]=
In fact, for this case, the overlap ratio of the generated theorems is always half because one system only generates string of odd-numbered lengths while the other generates strings of both odd and even numbered string lengths. There can be other cases where the only overlap between the two formal systems is their initial string and from there branch off in opposite ‘directions’. One such example would be the following two systems.
In[]:=
ex3=ResourceFunction["MultiwaySystem"][{"A""BAB","AB""AAAB"},"A",4,"StatesGraphStructure",EdgeStyle->Red];ex4=ResourceFunction["MultiwaySystem"][{"A""AAB","AABB""AAAB"},"A",4,"StatesGraphStructure",EdgeStyle->Blue];HighlightGraph[graphUnion@@{ex3,ex4},"A",ImageSizeLarge]
Out[]=
These would never converge on any of the theorem that the initial string entails because one system generates strings in which the first and last letter of the string is the same (for example, “” or “”). On the other hand, the second system only generates those strings in which the last letter of the string does not match the first letter (for example, “” or “”).
ABBAABA
BBBABB
ABBAB
BBBABA
Negations and Isomorphism
Negations and Isomorphism
In the previous section, we applied different rules to the same intial conditions. Another thing that we can do is apply the same rules to a large subset of initial conditions. Most often, we find that the theorems entailed by the rules acting on some initial conditions converge with each other. There are some intial conditions on which the rules just do not apply at all. Finally, there might be some initial conditions for which the rules can only act finitely many times and then the graph evolution halts.
In[]:=
(* Generates all possible binary strings of a given length*)enumerateStrings[n_Integer] := enumerateStrings[n] = StringJoin /@ Tuples[{"A", "B"}, n]
In[]:=
choice={{"A""AAA","AA""BAAB"},{"A""ABA","AAAA""ABBB"}};initCon=Catenate[enumerateStrings[#]&/@Range[6]];MapIndexed[{rule,index}|->HighlightGraph[NestGraph[StringReplaceList[#,rule]&,initCon,3,EdgeStyleRandomColor[],ImageSizeMedium,VertexSizeTiny],initCon],choice]
Out[]=
On some (in my experience) rare occasions, one comes across a formal system and a group of initial conditions that creates exactly two ‘islands’. For example, consider the rules {} and the set of all possible binary strings up till the length 4 as the initial conditions. This is what the states graph for this system looks like and this is where the story of my project starts.
"A""AAA","AAA""BBB","AAA""ABB"
In[]:=
sys1={{"A""AAA","AAA""BBB","AAA""ABB"}}Rotate[HighlightGraph[graphUnion@@MapIndexed[{rule,index}|->NestGraph[StringReplaceList[#,rule]&,initCon,3,EdgeStyleBrown,AspectRatio->2/1,ImageSizeLarge],sys1],initCon],3.14/2]
Out[]=
{{AAAA,AAABBB,AAAABB}}
Out[]=
So, What is Negation?
So, What is Negation?
Entailment Preserving Negation
Entailment Preserving Negation
Consider the map between the graphs of two random systems. We can draw an injective map from the first system’s theorems to the second system’s theorems and sleep comfortably thinking that we have equipped the formal system with negation. There is, however, an important property that this map lacks which logicians prefer their negations to be served along. I call this property Entailment Preservation.
In[]:=
sys2={{"A""BAB","AAB""AA"},{"A""AB","AA""ABBB","ABA""B"}}{g1,g2}=MapIndexed[{rule,index}|->NestGraph[StringReplaceList[#,rule]&,"BAAB",6,ImageSizeLarge,AspectRatio->4/9],sys2]
Out[]=
{{ABAB,AABAA},{AAB,AAABBB,ABAB}}
Out[]=
,
Entailment Preservation is the constraint on the negation map that states - for any arbitrary theorem B that can be derived from A within a formal system, the string ~B should be derivable from ~A in its negation map. Or in other words, the Entailment Preserving Negation is a map between two isomorphic entailment structures. An example of this would be the rules considered in the previous subsection. We take one of the components of the graph and then map it, while preserving its entailment structure to the other disjunct component of the graph. The highlighted part in the figure below represents a Subgraph Isomorphism and its entailment structure is precisely that of the other component.
Now, we have an injective mapping from one disjunct formal system A to another subgraph isomorphic entailment structure B. For every theorem that can be derived in A, we can derive its negation ~A in the isomorphic subgraph.
Consistency, Completeness and Decidability in our Framework
Consistency, Completeness and Decidability in our Framework
Once we find that for a formal system, a subgraph isomorphism exists, we can unambiguously define negation in the usual sense with which the word is used in logic. This has, now, opened up the scope to investigate multiway systems equipped with entailment preserving negation (which, henceforth, I shall simply call negation) in terms of their completeness and consistency.
Consistency
Consistency
What does it mean for a formal system to be consistent in the framework that we have developed? Syntactic consistency of a formal system is the requirement that if P is a theorem of a system A, ~P should not be a theorem of A . If we construct our formal system such that the two islands of vertices (representing theorems) are disconnected (i.e. lacking any entailment links between each other), then the nodes of one island are out of the entailment reach of the other. Therefore, from a theorem on the map on whose subgraph we have defined negation, there is no proof that can be drawn towards the initial string of the disjunct graph. Considering what constraints on negation were within our formalism, Consistency got baked into our formalism. How do we recognize the consistent formal system from the rules and initial conditions that generate both the disjunct graph components? To do that, we just need extract initial conditions from which a smaller graph branches out. That is easy to find. Just run the formal system until all intial conditions have been acted upon and then find the intersection between the kernels from which the smaller graph is generated and the totality of the initial conditions.
Further, there is a variability in the robustness of subgraph isomorphisms. For the same consistent formal system considered in this subsection, if we vary the number of evolution steps and the number of initial strings to act the rules upon, the isomorphisms and number of graph components can also vary. In the grid below, the elements of the tuple on top of each item represent the maximum string length considered for initial strings and the evolution steps respectively. The graphs highlighted in light blue are the ones for which entailment preserving negation is well defined. The two hues – blue and brown – signify the two disjunct graphs components. Notice when the same rules are allowed to only act on the initial strings A and B, there is no subgraph isomorphism between the two systems. The vertical lines are the indicators for the total number of strings possible for a given string length. (More on this is discussed in the Completeness Subsection later.)
Decidability or Syntactic Meaninglessness
Decidability or Syntactic Meaninglessness
For some systems, one can find subgraph isomorphisms between two disconnect component graphs in order to define entailment preserving negation. However, there still remain smaller entailment islands scattered in the system that do not connect with either the entailment fabric in consideration or its mapped negation. Consider the example illustrated below. There exists a subgraph isomorphisms between two components that can be used to define entailment preserving negation. However, there still exists another island that cannot reached by either of two systems.
Completeness
Completeness
Keywords
Keywords
◼
Meta-Mathematics
◼
Formal Systems
◼
Completeness and Consistency
◼
Multiway Systems
◼
Logic and Meta-Logic
Acknowledgments
Acknowledgments
This project could not have been possible without the long conversations with James Boyd and the wizard like coding skills of Nikolay Murzin (after whom we propose this method be named). The initial version of this inquiry was suggested by Dr. Stephen Wolfram.
References
References
◼
Reichenbach, Hans (1947). Elements of Symbolic Logic. New York: Dover. ISBN 0-486-24004-5.
◼
Hofstadter, Douglas R. (1979). Gödel, Escher, Bach : an Eternal Golden Braid. New York :Basic Books.
◼
Yaqub, Aladdin M. (2014). An Introduction to Metalogic. Broadview Press.