Re: Richard J. Lipton • Logical Complexity Of Proofs

Dear Dick,

You asked, “Is this measure, the logical flow of a proof, of any interest?”

I was not sure how you define the measure of flow in a proof — it seemed to have something to do with the number of implication arrows in the argument structure?

But this does bring up interesting issues of “proof style” …

Propositional calculus as a formal language and boolean functions as an object domain form an instructive microcosm for many issues of logic writ large.  The relation between proof theory and model theory is one of those issues, the status of propositional logic as a special case notwithstanding.

Folks who pursue the CSP–GSB line of development in graphical syntax for propositional calculus are especially likely to notice the following dimensions of proof style.

Formal Duality

This goes back to Peirce’s discovery of the “amphecks” as sole sufficient primitives for propositional calculus and the duality between Both Not (nnor) and Not Both (nand).  The same duality is present in Peirce’s graphical systems for propositional calculus.  It is analogous to the duality in projective geometry and it means we are always proving two theorems for the price of one.  That’s a reduction in complexity — it raises the question of how many such group-theoretic reductions we can find.

To be continued …

Resources

• Logic Syllabus
• Logical Graphs
• Cactus Language
• Futures Of Logical Graphs
• Minimal Negation Operators
• Survey of Theme One Program
• Survey of Animated Logical Graphs
• Propositional Equation Reasoning Systems

Applications

• Applications of a Propositional Calculator • Constraint Satisfaction Problems
• Exploratory Qualitative Analysis of Sequential Observation Data

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