Animated Logical Graphs • 41

Posted on September 29, 2020 by Jon Awbrey

Re: Richard J. Lipton • Logical Complexity Of Proofs
Re: Animated Logical Graphs • (35) (36) (37) (38) (39) (40)

Last time we looked at a formula of propositional logic Leibniz called a Praeclarum Theorema (PT).  We don’t concur it’s a theorem, of course, until there’s a proof it’s identically true and Leibniz gave an argument to demonstrate that.  Written out in one of our more current formalisms, PT takes the following form.

((a \Rightarrow b) \land (d \Rightarrow c)) \Rightarrow ((a \land d) \Rightarrow (b \land c))

Somewhat in the spirit of Reduced Instruction Set Computing, we reformulated PT in a propositional calculus using just two primitive operations, writing the logical negation of a proposition p as \texttt{(} p \texttt{)} and the logical conjunction of two propositions p, q as pq.  That gave us a text string in teletype parentheses and proposition letters, formatted two ways below.

Praeclarum Theorema Text Strings

Our next transformation of the theorem’s expression exploits a standard correspondence in combinatorics and computer science between parenthesized symbol strings and trees with symbols attached to the nodes.

Praeclarum Theorema Parse Graph

We can see the correspondence between text and tree in the case of PT by starting at the root of the tree and reading off the characters of the text string as we traverse the edges and nodes of the tree in the following manner.  The initial ``\texttt{(}" tells us to ascend the first edge, the next ``\texttt{(}" tells us to ascend the next edge on the left, where we find the letter ``a" from the string checks with the letter ``a" attached to the node of the tree where we are.  Another ``\texttt{(}" takes us up another edge, where we find the letter ``b" from the string checks with the letter ``b" on the current tree node.  Reading the first ``\texttt{)}" on the string entitles us to descend an edge and reading another ``\texttt{)}" gives us licence to descend another.  The way of things is most likely clear by this point — at any rate, I leave the exercise to the reader.

On the scene of the general correspondence between formulas and graphs the action may be summed up as follows.  The tree, called a parse tree or parse graph, is constructed in the process of checking whether the text string is syntactically well-formed, in other words, whether it satisfies the prescriptions of the associated formal grammar and is therefore a member in good standing of the prescribed formal language.  If the text string checks out, grammatically speaking, we call it a traversal string of the corresponding parse graph, because it can be reconstructed from the graph by a process like that illustrated above called traversing the graph.

To be continued …

Reference

  • Leibniz, Gottfried W. (1679–1686?), “Addenda to the Specimen of the Universal Calculus”, pp. 40–46 in G.H.R. Parkinson (ed., trans., 1966), Leibniz : Logical Papers, Oxford University Press, London, UK.

Praeclarum Theorema

Resources

Applications

cc: Cybernetics • Ontolog • Peirce (1) (2) (3) (4) (5) (6) • Structural Modeling • Systems

This entry was posted in Amphecks, Animata, Boolean Algebra, Boolean Functions, C.S. Peirce, Cactus Graphs, Constraint Satisfaction Problems, Deduction, Diagrammatic Reasoning, Duality, Equational Inference, Graph Theory, Laws of Form, Logic, Logical Graphs, Mathematics, Minimal Negation Operators, Model Theory, Painted Cacti, Peirce, Proof Theory, Propositional Calculus, Propositional Equation Reasoning Systems, Spencer Brown, Theorem Proving, Visualization and tagged , , , , , , , , , , , , , , , , , , , , , , , , , . Bookmark the permalink.