Animated Logical Graphs • 42

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

Praeclarum Theorema Parse Graph

Now that our propositional formula is cast in the form of a graph its evaluation proceeds as a sequence of graphical transformations where each graph in turn belongs to the same formal equivalence class as its predecessor and thus of the first.  The sequence terminates in a canonical graph making it manifest whether the initial formula is identically true by virtue of its form or not.

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: CyberneticsOntolog • Peirce (1) (2) (3) (4) (5) (6) (7)Structural ModelingSystems

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 | Tagged , , , , , , , , , , , , , , , , , , , , , , , , , | 9 Comments

Pragmatic Semiotic Information • Discussion 20

Re: R.J. Lipton and K.W. ReganIBM Conference on the Informational Lens

A little bit of history recoded …

It may be worth noting the Information Revolution in our understanding of science began in the mid 1860s when C.S. Peirce laid down what he called the “Laws of Information” in his lectures on the “Logic of Science” at Harvard University and the Lowell Institute.  Peirce took up “the puzzle of the validity of scientific inference” and claimed it was “entirely removed by a consideration of the laws of information”.

Here’s a collection of excerpts and commentary I assembled on the subject.

Resource

cc: CyberneticsOntolog ForumPeirce ListStructural ModelingSystems Science

Posted in Abduction, Aristotle, C.S. Peirce, Comprehension, Deduction, Definition, Determination, Extension, Hypothesis, Induction, Inference, Information, Information = Comprehension × Extension, Inquiry, Intension, Intention, Logic, Logic of Science, Mathematics, Measurement, Observation, Peirce, Perception, Phenomenology, Physics, Pragmatic Semiotic Information, Pragmatism, Probability, Quantum Mechanics, Scientific Method, Semiotics, Sign Relations | Tagged , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , | 7 Comments

Animated Logical Graphs • 41

Re: Richard J. LiptonLogical 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: CyberneticsOntolog • Peirce (1) (2) (3) (4) (5) (6)Structural ModelingSystems

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 | Tagged , , , , , , , , , , , , , , , , , , , , , , , , , | 10 Comments

Animated Logical Graphs • 40

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

One way to see the difference between insight proofs and routine proofs is to pick a single example of a theorem in propositional calculus and prove it two ways, one more insightful and one more routine.

The praeclarum theorema, or splendid theorem, is a theorem of propositional calculus noted and named by G.W. Leibniz, who stated and proved it in the following manner.

If a is b and d is c, then ad will be bc.
This is a fine theorem, which is proved in this way:
a is b, therefore ad is bd (by what precedes),
d is c, therefore bd is bc (again by what precedes),
ad is bd, and bd is bc, therefore ad is bc.  Q.E.D.

— Leibniz • Logical Papers, p. 41.

Expressed in contemporary logical notation, the theorem may be written as follows.

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

Using teletype parentheses \texttt{(} ~ \texttt{)} for the logical negation \texttt{(} p \texttt{)} of a proposition p and simple concatenation pq for the logical conjunction of propositions p and q enables writing the theorem in the following in-line and lispish ways.

Inline

\texttt{(} \quad   \texttt{(} a \texttt{(} b \texttt{))}  \texttt{(} d \texttt{(} c \texttt{))} \quad  \texttt{(} \quad   \texttt{(} ad \texttt{(} bc \texttt{))} \quad  \texttt{))}

Lispish

\begin{array}{lc}  \texttt{(} &  \texttt{(} a \texttt{(} b \texttt{))}  \texttt{(} d \texttt{(} c \texttt{))} \\  \texttt{(} &   \texttt{(} ad \texttt{(} bc \texttt{))} \\  \texttt{))}\end{array}

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: CyberneticsOntolog • Peirce (1) (2) (3) (4) (5) (6)Structural ModelingSystems

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 | Tagged , , , , , , , , , , , , , , , , , , , , , , , , , | 11 Comments

Precursors Of Category Theory • Discussion 3

Take your place on The Great Mandala
As it moves through your brief moment of time.
Win or lose now you must choose now
And if you lose you’re only losing your life.

Peter Yarrow

Re: Ontolog ForumAlex Shkotin

AS:
I like Kant’s criticism of Aristotle versions of categories.

“Finding these basic concepts — such a proposal was worthy of such an astute thinker like Aristotle.  But since he did not have any principle, he picked them up as they came across to him, and first typed ten concepts, which he called categories (predicates).  Then it seemed to him that he found five more such concepts, which he added to the previous ones under the name of post-predicate.  However, his table was still insufficient.”  (Kant, Critique of Pure Reason, §10.  About Pure Rational Concepts, or Categories).

Dear Alex,

My sketch on Precursors Of Category Theory shows a big ellipsis under the heading for Kant.  I meant to get back to him, as I used to do every half-decade or so, but it’s been a long time since I kept to that schedule.  Kant is a lodestar in the Peircean constellation — Peirce’s “New List of Categories” invokes his guidance on the function of concepts just as he tries his own hand at the wheel.  I quoted that passage in my selections from Peirce.

Selection 1

§1.  This paper is based upon the theory already established, that the function of conceptions is to reduce the manifold of sensuous impressions to unity, and that the validity of a conception consists in the impossibility of reducing the content of consciousness to unity without the introduction of it.  (CP 1.545).

§2.  This theory gives rise to a conception of gradation among those conceptions which are universal.  For one such conception may unite the manifold of sense and yet another may be required to unite the conception and the manifold to which it is applied;  and so on.  (CP 1.546).

C.S. Peirce, “On a New List of Categories” (1867)

To be continued …

References

Resources

cc: CyberneticsOntolog ForumPeirce ListStructural ModelingSystems Science

Posted in Abstraction, Ackermann, Aristotle, C.S. Peirce, Carnap, Category Theory, Hilbert, Kant, Logic, Logic of Relatives, Mathematics, Peirce, Peirce's Categories, Relation Theory, Saunders Mac Lane, Sign Relations, Type Theory | Tagged , , , , , , , , , , , , , , , , | 6 Comments

Precursors Of Category Theory • Discussion 2

Re: Ontolog ForumAlex Shkotin

AS:
Looking at “categories, or types” in Precursors Of Category Theory • Hilbert and Ackermann what do you think of to say “Precursors Of Type Theory” as Category Theory is a math discipline?   […]   It seems you collect for three topics:  phil‑cat, type theory, math cat‑theory.

Dear Alex,

When it comes to math, computer science, and their applications to logic and linguistics I see categories and types as pretty much the same things.  No doubt the words are used differently in other contexts but I am concerned with the above contexts at the moment.

The diversity of categorical systems across different disciplines and theorists is obvious to all observers.  But when we examine how systems of categories operate in grammatical, logical, or more generally semiotic frameworks we can detect a common function all the more useful systems share.  The semiotic framework is already well marked in Aristotle’s founding text on interpretation and the function of category references as go-betweens from unruly language to the rule of logic is clearly delineated in his treatise on categories.  It is that order of function which is preserved from Aristotle’s categories to our current mathematical variety.

References

Resources

cc: CyberneticsOntolog ForumPeirce ListStructural ModelingSystems Science

Posted in Abstraction, Ackermann, Aristotle, C.S. Peirce, Carnap, Category Theory, Hilbert, Kant, Logic, Logic of Relatives, Mathematics, Peirce, Peirce's Categories, Relation Theory, Saunders Mac Lane, Sign Relations, Type Theory | Tagged , , , , , , , , , , , , , , , , | 6 Comments

Survey of Precursors Of Category Theory • 2

A few years ago I began a sketch on the “Precursors of Category Theory”, tracing the continuities of the category concept from Aristotle, to Kant and Peirce, through Hilbert and Ackermann, to contemporary mathematical practice.  A Survey of resources on the topic is given below, still very rough and incomplete, but perhaps a few will find it of use.

Background

Blog Series

  • Notes On Categories • (1)
  • Precursors Of Category Theory • (1)(2)(3)

Categories à la Peirce

cc: CyberneticsOntolog ForumPeirce ListStructural ModelingSystems Science

Posted in Abstraction, Ackermann, Analogy, Aristotle, C.S. Peirce, Carnap, Category Theory, Diagrams, Foundations of Mathematics, Functional Logic, Hilbert, History of Mathematics, Hypostatic Abstraction, Kant, Logic, Mathematics, Peirce, Propositions As Types Analogy, Relation Theory, Saunders Mac Lane, Semiotics, Type Theory, Universals | Tagged , , , , , , , , , , , , , , , , , , , , , , | 7 Comments

Precursors Of Category Theory • Discussion 1

Re: FB | Medieval LogicEBJAJAEBJAEBJAJAEB

JA:  In the logic of Aristotle categories are adjuncts to reasoning designed to resolve ambiguities and thus to prepare equivocal signs, otherwise recalcitrant to being ruled by logic, for the application of logical laws.  The example of ζωον illustrates that we don’t need categories to make generalizations so much as we need them to control generalizations, to reign in abstractions and analogies that are stretched too far.

EB:  Aristotelian categories are “adjuncts to reasoning”?

I’ve been exploring a particular type of commonality or continuity in the way categorical references function in various systems of categories from Aristotle, through Kant and Peirce, to contemporary mathematical category theory.  The following posts give the background on that.

  • Precursors Of Category Theory • (1) (2) (3)

Viewing the discussion of Excluded Middle and Non-Contradiction in the light of Peirce’s observations about their relation to the General and the Vague, the upshot is that elements of natural language, indeed, all species of representation in the wild, do not as a rule obey the usual laws of logic, but violate them in various ways.  It is only after signs and symbols have been categorized, their equivocations “driven down” or “reduced” by reference to the appropriate category, that they become subject to logical laws.

References

Resources

cc: CyberneticsOntolog ForumPeirce ListStructural ModelingSystems Science

Posted in Abstraction, Ackermann, Aristotle, C.S. Peirce, Carnap, Category Theory, Hilbert, Kant, Logic, Logic of Relatives, Mathematics, Peirce, Peirce's Categories, Relation Theory, Saunders Mac Lane, Sign Relations, Type Theory | Tagged , , , , , , , , , , , , , , , , | 6 Comments

Animated Logical Graphs • 39

Re: Richard J. LiptonLogical Complexity Of Proofs

Happy Peirce’s Birthday, Everyone ❢

We’ve been discussing aspects of proof style arising in connection with the complexity of proofs.  In previous posts we took up (1) the aspect of formal duality, reflecting in passing on the prospect of higher symmetries, and (2) the spectrum ranging from information-reducing to information-preserving inference rules.  Here’s a quick recap —

A third aspect of proof style arising in this connection is the degree of insight demanded and demonstrated in the performance of a proof.  Generally speaking, the same endpoint can be reached in many different ways from given starting points, by paths ranging from those exhibiting appreciable insight to those exercising little more than persistence in sticking to a set routine.

A modicum of insight suffices to suggest the quality of “insight” resists pinning down in a succinct definition but we do tend to recognize it when we see it, so let me inch forward by highlighting its salient features in a graded series of examples.

To be continued …

Resources

Applications

cc: CyberneticsOntolog • Peirce (1) (2) (3) (4) (5) (6)Structural ModelingSystems

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 | Tagged , , , , , , , , , , , , , , , , , , , , , , , , , | 12 Comments

Survey of Definition and Determination • 1

In the early 1990s, “in the middle of life’s journey” as the saying goes, I returned to grad school in a systems engineering program with the idea of taking a more systems-theoretic approach to my development of Peircean themes, from signs and scientific inquiry to logic and information theory.

Two of the first questions calling for fresh examination were the closely related concepts of definition and determination, not only as Peirce used them in his logic and semiotics but as researchers in areas as diverse as computer science, cybernetics, physics, and systems science would find themselves forced to reconsider the concepts in later years.  That led me to collect a sample of texts where Peirce and a few other writers discuss the issues of definition and determination.  There are copies of those selections at the following sites.

What follows is a Survey of blog and wiki posts on Definition and Determination, with a focus on the part they play in Peirce’s interlinked theories of signs, information, and inquiry.  In classical logical traditions the concepts of definition and determination are closely related and their bond acquires all the more force when we view the overarching concept of constraint from an information-theoretic point of view, as Peirce did beginning in the 1860s.

Blog Dialogs

cc: CyberneticsOntolog ForumPeirce ListStructural ModelingSystems Science

Posted in C.S. Peirce, Comprehension, Constraint, Definition, Determination, Extension, Form, Indication, Information = Comprehension × Extension, Inquiry, Intension, Logic, Logic of Science, Mathematics, Peirce, Semiotics, Structure | Tagged , , , , , , , , , , , , , , , , | 9 Comments