Difference between revisions of "Logical graph"
Jon Awbrey (talk | contribs) (→Computational representation: sub [the following/this], ins [then]) |
Jon Awbrey (talk | contribs) (→Duality : logical and topological: del clutter) |
||
| Line 24: | Line 24: | ||
==Duality : logical and topological== | ==Duality : logical and topological== | ||
| − | There are two types of [[duality (mathematics)|duality]] that have to be kept separately mind in the use of logical graphs | + | There are two types of [[duality (mathematics)|duality]] that have to be kept separately mind in the use of logical graphs — [[De Morgan's laws|logical duality]] and [[topology|topological]] [[dual graph|duality]]. |
There is a standard way that graphs of the order that Peirce considered, those embedded in a continuous [[manifold]] like that commonly represented by a plane sheet of paper — with or without the paper bridges that Peirce used to augment its [[genus (mathematics)|topological genus]] — can be represented in linear text as what are called ''[[parsing|parse string]]s'' or ''[[tree traversal|traversal string]]s'' and parsed into ''[[data structure|pointer structure]]s'' in computer memory. | There is a standard way that graphs of the order that Peirce considered, those embedded in a continuous [[manifold]] like that commonly represented by a plane sheet of paper — with or without the paper bridges that Peirce used to augment its [[genus (mathematics)|topological genus]] — can be represented in linear text as what are called ''[[parsing|parse string]]s'' or ''[[tree traversal|traversal string]]s'' and parsed into ''[[data structure|pointer structure]]s'' in computer memory. | ||
| Line 48: | Line 48: | ||
Though it's not really there in the most abstract topology of the matter, for all sorts of pragmatic reasons we find ourselves compelled to single out the outermost region of the plane in a distinctive way and to mark it as the ''[[root node]]'' of the corresponding [[dual graph]]. In the present style of Figure the root nodes are marked by horizontal strike-throughs. | Though it's not really there in the most abstract topology of the matter, for all sorts of pragmatic reasons we find ourselves compelled to single out the outermost region of the plane in a distinctive way and to mark it as the ''[[root node]]'' of the corresponding [[dual graph]]. In the present style of Figure the root nodes are marked by horizontal strike-throughs. | ||
| − | Extracting the dual | + | Extracting the dual graphs from their composite matrices, we get this picture: |
<p>[[Image:Logical_Graph_Figure_5.jpg|center]]</p> | <p>[[Image:Logical_Graph_Figure_5.jpg|center]]</p> | ||
| Line 58: | Line 58: | ||
<p>[[Image:Logical_Graph_Figure_6.jpg|center]]</p> | <p>[[Image:Logical_Graph_Figure_6.jpg|center]]</p> | ||
| − | This ritual is called ''[[tree traversal|traversing]]'' the tree, and the string read off is | + | This ritual is called ''[[tree traversal|traversing]]'' the tree, and the string read off is called the ''[[traversal string]]'' of the tree. The reverse ritual, that passes from the string to the tree, is called ''[[parsing]]'' the string, and the tree constructed is called the ''[[parse tree|parse graph]]'' of the string. The speakers thereof tend to be a bit loose in this language, often using ''[[parse string]]'' to mean the string that gets parsed into the associated graph. |
We have now treated in some detail various forms of the axiom or initial equation that is formulated in string form as " <math>((~))~=</math> ". For the sake of comparison, let's record the planar and dual forms of the axiom that is formulated in string form as "<math>(~)(~)~=~(~)</math>". | We have now treated in some detail various forms of the axiom or initial equation that is formulated in string form as " <math>((~))~=</math> ". For the sake of comparison, let's record the planar and dual forms of the axiom that is formulated in string form as "<math>(~)(~)~=~(~)</math>". | ||
Revision as of 15:26, 16 August 2008
A logical graph is a special type of graph-theoretic structure in any one of several systems of graphical syntax that Charles Sanders Peirce developed for logic.
In his papers on qualitative logic, entitative graphs, and existential graphs, Peirce developed several versions of a graphical formalism, or a graph-theoretic formal language, designed to be interpreted for logic.
In the century since Peirce initiated this line of development, a variety of formal systems have branched out from what is abstractly the same formal base of graph-theoretic structures. This article examines the common basis of these formal systems from a bird's eye view, focusing on those aspects of form that are shared by the entire family of algebras, calculi, or languages, however they happen to be viewed in a given application.
Abstract point of view
- Wollust ward dem Wurm gegeben …
- (Friedrich Schiller, An die Freude)
The bird's eye view in question is more formally known as the perspective of formal equivalence, from which remove one cannot see many distinctions that appear momentous from lower levels of abstraction. In particular, expressions of different formalisms whose syntactic structures are isomorphic from the standpoint of algebra or topology are not recognized as being different from each other in any significant sense. Though we may note in passing such historical details as the circumstance that Charles Sanders Peirce used a streamer-cross symbol where George Spencer Brown used a carpenter's square marker, the theme of principal interest at the abstract level of form is neutral with regard to variations of that order.
In lieu of a beginning
In medias res, as always, we nevertheless need a quantum of formal matter to keep the topical momentum going. A game try at supplying that least bit of motivation may be found in this duo of transformations between the indicated forms of enclosure:
In lieu of better names, and in hope of a better reason to come in good time, we may for the moment refer to these two forms of transformation as axioms or initials.
Duality : logical and topological
There are two types of duality that have to be kept separately mind in the use of logical graphs — logical duality and topological duality.
There is a standard way that graphs of the order that Peirce considered, those embedded in a continuous manifold like that commonly represented by a plane sheet of paper — with or without the paper bridges that Peirce used to augment its topological genus — can be represented in linear text as what are called parse strings or traversal strings and parsed into pointer structures in computer memory.
A blank sheet of paper can be represented in linear text as a blank space, but that way of doing it tends to be confusing unless the logical expression under consideration is set off in a separate display.
For example, consider the axiom or initial equation that is shown below:
This can be written inline as “ \((~(~)~)~=\) ” or set off in a text display:
\((~(~)~)~=\)
When we turn to representing the corresponding expressions in computer memory, where they can be manipulated with utmost facility, we begin by transforming the planar graphs into their topological duals. The planar regions of the original graph correspond to nodes (or points) of the dual graph, and the boundaries between planar regions in the original graph correspond to edges (or lines) between the nodes of the dual graph.
For example, overlaying the corresponding dual graphs on the plane-embedded graphs shown above, we get the following composite picture:
Though it's not really there in the most abstract topology of the matter, for all sorts of pragmatic reasons we find ourselves compelled to single out the outermost region of the plane in a distinctive way and to mark it as the root node of the corresponding dual graph. In the present style of Figure the root nodes are marked by horizontal strike-throughs.
Extracting the dual graphs from their composite matrices, we get this picture:
It is easy to see the relationship between the parenthetical expressions of Peirce's logical graphs, that somewhat clippedly picture the ordered containments of their formal contents, and the associated dual graphs, that constitute the species of rooted trees here to be described.
In the case of our last example, a moment's contemplation of the following picture will lead us to see that we can get the corresponding parenthesis string by starting at the root of the tree, climbing up the left side of the tree until we reach the top, then climbing back down the right side of the tree until we return to the root, all the while reading off the symbols, in this case either "\((\!\)" or "\()\!\)", that we happen to encounter in our travels.
This ritual is called traversing the tree, and the string read off is called the traversal string of the tree. The reverse ritual, that passes from the string to the tree, is called parsing the string, and the tree constructed is called the parse graph of the string. The speakers thereof tend to be a bit loose in this language, often using parse string to mean the string that gets parsed into the associated graph.
We have now treated in some detail various forms of the axiom or initial equation that is formulated in string form as " \(((~))~=\) ". For the sake of comparison, let's record the planar and dual forms of the axiom that is formulated in string form as "\((~)(~)~=~(~)\)".
First the plane-embedded maps:
Next the plane maps and their dual trees superimposed:
Finally the dual trees by themselves:
And here are the parse trees with their traversal strings indicated:
We have at this point enough material to begin thinking about the forms of analogy, iconicity, metaphor, morphism, whatever you want to call them, that are pertinent to the use of logical graphs in their various logical interpretations, for instance, those that Peirce described as entitative graphs and existential graphs.
Computational representation
The parse graphs that we've been looking at so far bring us one step closer to the pointer graphs that it takes to make these maps and trees live in computer memory, but they are still a couple of steps too abstract to detail the concrete species of dynamic data structures that we need. The time has come to flesh out the skeletons that we've drawn up to this point.
Nodes in a graph represent records in computer memory. A record is a collection of data that can be conceived to reside at a specific address. The address of a record is analogous to a demonstrative pronoun, on which account programmers commonly describe it as a pointer and semioticians recognize it as a type of sign called an index.
At the next level of concreteness, a pointer→record data structure can be represented as follows:
This portrays \(index_0\!\) as the address of a record that contains the following data:
\(datum_1, datum_2, datum_3, \ldots,\!\) and so on.
What makes it possible to represent graph-theoretical structures as data structures in computer memory is the fact that an address is just another datum, and so we may have a state of affairs like the following:
Returning to the abstract level, it takes three nodes to represent the three data records illustrated above: one root node connected to a couple of adjacent nodes. The items of data that do not point any further up the tree are then treated as labels on the record-nodes where they reside, as shown below:
Notice that drawing the arrows is optional with rooted trees like these, since singling out a unique node as the root induces a unique orientation on all the edges of the tree, with up being the same direction as away from the root.
Quick tour of the neighborhood
This much preparation allows us to present the two most basic axioms of logical graphs, shown in graph and string forms below, along with handy names for referring to the two different directions of applying the axioms.
o-----------------------------------------------------------o | | | o o o | | \ / | | | @ = @ | | | o-----------------------------------------------------------o | | | ( ) ( ) = ( ) | | | o-----------------------------------------------------------o | Axiom I_1. Distract <--- | ---> Condense | o-----------------------------------------------------------o
o-----------------------------------------------------------o | | | o | | | | | o | | | | | @ = @ | | | o-----------------------------------------------------------o | | | (( )) = | | | o-----------------------------------------------------------o | Axiom I_2. Unfold <--- | ---> Refold | o-----------------------------------------------------------o
Primary arithmetic as semiotic system
Though it may not seem too exciting, logically speaking, there are many good reasons for getting comfortable with the system of forms that is represented indifferently, topologically speaking, by rooted trees, by well-formed strings of parentheses, and by finite sets of non-intersecting simple closed curves in the plane.
- One reason is that it gives us a respectable example of a sign domain to cut our semiotic teeth on, non-trivial in the sense that it contains a countable infinity of signs.
- Another reason is that it allows us to study a simple form of computation that is recognizable as a species of semiosis, or semiotic process.
This space of forms, along with the two axioms that induce its partition into exactly two equivalence classes, is what George Spencer Brown called the primary arithmetic.
Here are the axioms of the primary arithmetic:
o-----------------------------------------------------------o | | | o o o | | \ / | | | @ = @ | | | o-----------------------------------------------------------o | | | ( ) ( ) = ( ) | | | o-----------------------------------------------------------o | Axiom I_1. Distract <--- | ---> Condense | o-----------------------------------------------------------o
o-----------------------------------------------------------o | | | o | | | | | o | | | | | @ = @ | | | o-----------------------------------------------------------o | | | (( )) = | | | o-----------------------------------------------------------o | Axiom I_2. Unfold <--- | ---> Refold | o-----------------------------------------------------------o
Taking S to be the set of rooted trees and S0 to be the set that has the root node and the rooted edge as its only two elements, writing these facts more briefly as S = {rooted trees} and S0 = {O, |}, simple intuition, or a simple inductive proof, will assure us that any rooted tree can be reduced by means of the axioms of the primary arithmetic either to a root node "@" or else to a rooted edge "|".
For example, consider the reduction that proceeds as follows:
o-----------------------------------------------------------o | | | o o o | | \| | | | o o o | | \|/ | | @ | | | o===========================================================o | | | o o | | | | | | o o o | | \|/ | | @ | | | o===========================================================o | | | o | | | | | o o | | |/ | | @ | | | o===========================================================o | | | o | | / | | @ | | | o-----------------------------------------------------------o
Regarded as a semiotic process, this amounts to a sequence of signs, every one after the first being the interpretant of its predecessor, ending in a sign that we may regard as the canonical sign for their common object, in the upshot, the result of the computation process. Simple as it is, this exhibits the main features of all computation, specifically, a semiotic process that proceeds from an obscure sign to a clear sign of the same object, in its aim and effect, an action on behalf of clarification.
Primary algebra as pattern calculus
Experience teaches that complex objects are best approached in a gradual, laminar, modular fashion, one step, one layer, one piece at a time, and it's just as much the case when the complexity of the object is irreducible, that is, when the articulations of the representation are necessarily at joints that are cloven disjointedly from nature, with some assembly required in the synthetic integrity of the intuition.
That's one good reason for spending so much time on the first half of zeroth order logic, represented here by the primary arithmetic, a level of formal structure that C.S. Peirce verged on intuiting at numerous points and times in his work on logical graphs, and that Spencer Brown named and brought more completely to life.
There is one other reason for lingering a while longer in these primitive forests, and this is that an acquaintance with "bare trees", those as yet unadorned with literal or numerical labels, will provide a firm basis for understanding what's really at issue in such problems as the "ontological status of variables".
It is probably best to illustrate this theme in the setting of a concrete case, which we can do by revisiting the previous example of reductive evaluation:
o-----------------------------------------------------------o | | | o o o | | \| | | | o o o | | \|/ | | @ | | | o===========================================================o | | | o o | | | | | | o o o | | \|/ | | @ | | | o===========================================================o | | | o | | | | | o o | | |/ | | @ | | | o===========================================================o | | | o | | / | | @ | | | o-----------------------------------------------------------o
The observation of several semioses of roughly this shape will most probably lead an observer with any observational facility whatever to notice that it doesn't really matter what sorts of branches happen to sprout from the side of the root aside from the lone edge that also grows there — the end will all be one.
Our observer might think to summarize the results of many such observations by introducing a label or variable to signify any shape of branch whatever, writing something like the following:
o-----------------------------------------------------------o | | | o | | a / | | @ | | | o===========================================================o | | | o | | / | | @ | | | o-----------------------------------------------------------o
Observations like that, made about an arithmetic of any variety, germinated by their summarizations, are the root of all algebra.
Speaking of algebra, and having encountered already one example of an algebraic law, we might as well introduce the axioms of the primary algebra, once again deriving their substance and their name from the works of Charles Sanders Peirce and George Spencer Brown, respectively.
o-----------------------------------------------------------o | | | a o o | | | | | | a @ = @ | | | o-----------------------------------------------------------o | | | a(a) = ( ) | | | o-----------------------------------------------------------o | Axiom J_1. Insert <--- | ---> Delete | o-----------------------------------------------------------o
o-----------------------------------------------------------o | | | ab ac b c | | o o o o | | \ / \ / | | o o | | | | | | @ = a @ | | | o-----------------------------------------------------------o | | | ((ab)(ac)) = a((b)(c)) | | | o-----------------------------------------------------------o | Axiom J_2. Distribute <--- | ---> Collect | o-----------------------------------------------------------o
The choice of axioms for any formal system is to some degree a matter of aesthetics, as it is commonly the case that many different selections of formal rules will serve as axioms to derive all the rest as theorems. As it happens, the example of an algebraic law that we noticed first, a( ) = ( ), as simple as it appears, proves to be provable as a theorem on the grounds of the foregoing axioms.
We might also notice at this point a subtle difference between the primary arithmetic and the primary algebra with respect to the grounds of justification that we have naturally if tacitly adopted for their respective sets of axioms.
The arithmetic axioms were introduced by fiat, in a quasi-apriori fashion, though of course it is only long prior experience with the practical uses of comparably developed generations of formal systems that would actually induce us to such a quasi-primal move. The algebraic axioms, in contrast, can be seen to derive their motive and their justice from the observation and summarization of patterns that are visible in the arithmetic spectrum.
Formal development
What precedes this point is intended as an informal introduction to the axioms of the primary arithmetic and primary algebra, and hopefully provides the reader with an intuitive sense of their motivation and rationale.
The next order of business is to give the exact forms of the axioms that are used in the following more formal development, devolving from Peirce's various systems of logical graphs via Spencer-Brown's Laws of Form (LOF). In formal proofs, a variation of the annotation scheme from LOF will be used to mark each step of the proof according to which axiom, or 'initial', is being invoked to justify the corresponding step of syntactic transformation, whether it applies to graphs or to strings.
Axioms
The axioms are just four in number, divided into the arithmetic initials I1 and I2, and the algebraic initials J1 and J2.
o-----------------------------------------------------------o | | | o o o | | \ / | | | @ = @ | | | o-----------------------------------------------------------o | | | ( ) ( ) = ( ) | | | o-----------------------------------------------------------o | Axiom I_1. Distract <--- | ---> Condense | o-----------------------------------------------------------o
o-----------------------------------------------------------o | | | o | | | | | o | | | | | @ = @ | | | o-----------------------------------------------------------o | | | (( )) = | | | o-----------------------------------------------------------o | Axiom I_2. Unfold <--- | ---> Refold | o-----------------------------------------------------------o
o-----------------------------------------------------------o | | | a o o | | | | | | a @ = @ | | | o-----------------------------------------------------------o | | | a(a) = ( ) | | | o-----------------------------------------------------------o | Axiom J_1. Insert <--- | ---> Delete | o-----------------------------------------------------------o
o-----------------------------------------------------------o | | | ab ac b c | | o o o o | | \ / \ / | | o o | | | | | | @ = a @ | | | o-----------------------------------------------------------o | | | ((ab)(ac)) = a((b)(c)) | | | o-----------------------------------------------------------o | Axiom J_2. Distribute <--- | ---> Collect | o-----------------------------------------------------------o
Here is one way of reading the axioms under the entitative interpretation:
| I1 | true or true | = | true |
| I2 | not true | = | false |
| J1 | a or not a | = | true |
| J2. | [a or b] and [a or c] | = | a or [b and c] |
Here is one way of reading the axioms under the existential interpretation:
| I1 | false and false | = | false |
| I2 | not false | = | true |
| J1 | a and not a | = | false |
| J2 | [a and b] or [a and c] | = | a and [b or c] |
All of the axioms in this set have the form of equations. This means that all of the inference steps that they allow are reversible. The proof annotation scheme employed below makes use of a double bar "=====" to mark this fact, although it will often be left to the reader to decide which of the two possible directions is the one required for applying the indicated axiom.
Frequently used theorems
The actual business of proof is a far more strategic affair than the simple cranking of inference rules might suggest. Part of the reason for this lies in the circumstance that the usual brands of inference rules combine the moving forward of a state of inquiry with the losing of information along the way that doesn't appear to be immediately relevant, at least, not as viewed in the local focus and the short run of the moment to moment proceedings of the proof in question. Over the long haul, this has the pernicious side-effect that one is forever strategically required to reconstruct much of the information that one had strategically thought to forget in earlier stages of the proof, if 'before the proof started' can also be counted as an earlier stage of the proof in view.
This is just one of the reasons that it can be very instructive to study equational inference rules of the sort that our axioms have just provided. Although equational forms of reasoning are paramount in mathematics, they are less familiar to the student of the usual logic textbooks, who may find a few surprises here.
By way of gaining a minimal experience with how equational proofs look in the present forms of syntax, let us examine the proofs of a few essential theorems in the primary algebra.
C1. Double negation theorem
The first theorem goes under the names of Consequence 1 (C1), the double negation theorem (DNT), or Reflection.
o-----------------------------------------------------------o | C_1. Double Negation Theorem | o-----------------------------------------------------------o | | | a | | o | | | | | o | | | a | | @ = @ | | | o-----------------------------------------------------------o | | | ((a)) = a | | | o-----------------------------------------------------------o | Reflect <---- | ----> Reflect | o-----------------------------------------------------------o
The proof that follows is adapted from the one that was given by George Spencer Brown in his book Laws of Form (LOF), and credited to two of his students, John Dawes and D.A. Utting.
o-----------------------------------------------------------o | C_1. Double Negation Theorem. Proof. | o-----------------------------------------------------------o | | | a o | | \ | | \ | | o | | \ | | \ | | @ | | | o=============================< I2. Unfold "(())" >=========o | | | a o o | | \ / | | \ / | | o o | | \ / | | \ / | | @ | | | o=============================< J1. Insert "(a)" >==========o | | | a o | | / | | / | | a o a o o | | \ \ / | | \ \ / | | o o | | \ / | | \ / | | @ | | | o=============================< J2. Distribute "((a))" >====o | | | a o a o | | \ \ | | \ \ | | o o a o | | \ \ / | | \ \ / | | a o o | | \ / | | \ / | | o | | / | | / | | @ | | | o=============================< J1. Delete "(a)" >==========o | | | a o | | \ | | \ | | o o | | \ \ | | \ \ | | a o o | | \ / | | \ / | | o | | / | | / | | @ | | | o=============================< J1. Insert "a" >============o | | | a o | | \ | | \ | | o o a | | \ \ | | \ \ | | a o o a | | \ / | | \ / | | o | | / | | / | | @ | | | o=============================< J2. Collect "a" >===========o | | | a o | | \ | | \ | | o o a | | \ \ | | \ \ | | o o | | \ / | | \ / | | o | | / | | / | | a @ | | | o=============================< J1. Delete "((a))" >========o | | | o | | \ | | \ | | o | | / | | / | | a @ | | | o=============================< I2. Refold "(())" >=========o | | | a | | @ | | | o=============================< QED >=======================o
C2. Generation theorem
One theorem of frequent use goes under the nickname of the weed and seed theorem (WAST). The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader. What the WAST says is that a label can be freely distributed or freely erased (retracted or withdrawn) anywhere in a subtree whose root is labeled with that label. The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem. In LOF, it goes by the name of Consequence 2 (C2), or Generation.
o-----------------------------------------------------------o | C_2. Generation Theorem | o-----------------------------------------------------------o | | | b o a o b | | | | | | a @ = a @ | | | o-----------------------------------------------------------o | | | a(b) = a(ab) | | | o-----------------------------------------------------------o | Degenerate <---- | ----> Regenerate | o-----------------------------------------------------------o
Here is a proof of the Generation Theorem.
o-----------------------------------------------------------o | C_2. Generation Theorem. Proof. | o-----------------------------------------------------------o | | | b o | | | | | a @ | | | o=============================< C1. Reflect "a(b)" >========o | | | b o | | | | | a o | | | | | o | | | | | @ | | | o=============================< I2. Unfold "(())" >=========o | | | b o o | | | / | | a o o | | |/ | | o | | | | | @ | | | o=============================< J1. Insert "a" >============o | | | b o o a | | | / | | a o o a | | |/ | | o | | | | | @ | | | o=============================< J2. Collect "a" >===========o | | | b o o a | | | / | | o o | | |/ | | o | | | | | a @ | | | o=============================< C1. Reflect "a", "b" >======o | | | a o b | | | | | a @ | | | o=============================< QED >=======================o
C3. Dominant form theorem
The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as Consequence 3 (C3), or Integration. A better mnemonic might be dominance and recession theorem (DART), but perhaps the brevity of dominant form theorem (DFT) is sufficient reminder of its double-edged role in proofs.
o-----------------------------------------------------------o | C_3. Dominant Form Theorem | o-----------------------------------------------------------o | | | o o | | | | | | a @ = @ | | | o-----------------------------------------------------------o | | | a( ) = ( ) | | | o-----------------------------------------------------------o | Remark <---- | ----> Recess | o-----------------------------------------------------------o
Here is a proof of the Dominant Form Theorem.
o-----------------------------------------------------------o | C_3. Dominant Form Theorem. Proof. | o-----------------------------------------------------------o | | | o | | | | | a @ | | | o=============================< C2. Regenerate "a" >========o | | | a o | | | | | a @ | | | o=============================< J1. Delete "a" >============o | | | o | | | | | @ | | | o=============================< QED >=======================o
Exemplary proofs
With the meagre means afforded by the axioms and theorems given so far, it is already possible to prove a multitude of much more complex theorems. A couple of all-time favorites are given next.
Peirce's law
This section presents a proof of Peirce's law, commonly written:
- [[p ⇒ q] ⇒ p] ⇒ p
The first order of business is present the statement as it appears in the so-called existential interpretation of Peirce's own logical graphs. Here is the statement of Peirce's law, as rendered under the existential interpretation into (the topological dual forms of) Peirce's logical graphs:
o-----------------------------------------------------------o | Peirce's Law | o-----------------------------------------------------------o | | | p o---o q | | | | | o---o p | | | | | o---o p | | | | | @ = @ | | | o-----------------------------------------------------------o | | | (((p (q)) (p)) (p))) = | | | o-----------------------------------------------------------o
Finally, here's the promised proof of Peirce's law:
o-----------------------------------------------------------o | Peirce's Law. Proof | o-----------------------------------------------------------o | | | p o---o q | | | | | o---o p | | | | | o---o p | | | | | @ | | | o==================================< Collect >==============o | | | o---o q | | | | | o---o | | | | | p o---o p | | | | | @ | | | o==================================< Recess >===============o | | | o---o | | | | | p o---o p | | | | | @ | | | o==================================< Refold >===============o | | | p o---o p | | | | | @ | | | o==================================< Delete >===============o | | | o---o | | | | | @ | | | o==================================< Refold >===============o | | | @ | | | o==================================< QED >==================o
Praeclarum theorema
An illustrious example of a propositional theorem is the praeclarum theorema, the admirable, shining, or splendid theorem of Leibniz.
- 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).
Under the existential interpretation, the praeclarum theorema is represented by means of the following logical graph.
o-----------------------------------------------------------o | Praeclarum Theorema (Leibniz) | o-----------------------------------------------------------o | | | b o o c o bc | | | | | | | a o o d o ad | | \ / | | | o---------o | | | | | | | | @ = @ | | | o-----------------------------------------------------------o | | | ((a(b))(d(c))((ad(bc)))) = | | | o-----------------------------------------------------------o
And here's a neat proof of that nice theorem.
o-----------------------------------------------------------o | Praeclarum Theorema (Leibniz). Proof. | o-----------------------------------------------------------o | | | b o o c o bc | | | | | | | a o o d o ad | | \ / | | | o---------o | | | | | | | | @ | | | o=============================< C1. Reflect "ad(bc)" >======o | | | b o o c | | | | | | a o o d | | \ / | | ad o---------o bc | | | | | | | | @ | | | o=============================< Weed "a", "d" >=============o | | | b o o c | | | | | | o o | | \ / | | ad o---------o bc | | | | | | | | @ | | | o=============================< C1. Reflect "b", "c" >======o | | | abcd o---------o bc | | | | | | | | @ | | | o=============================< Weed "bc" >=================o | | | abcd o---------o | | | | | | | | @ | | | o=============================< C3. Recess "abcd" >=========o | | | o---------o | | | | | | | | @ | | | o=============================< I2. Refold "(())" >=========o | | | @ | | | o=============================< QED >=======================o
Bibliography
- Leibniz, G.W. (1679–1686 ?), "Addenda to the Specimen of the Universal Calculus", pp. 40–46 in G.H.R. Parkinson (ed. and trans., 1966), Leibniz: Logical Papers, Oxford University Press, London, UK.
- Peirce, C.S. (1931–1935, 1958), Collected Papers of Charles Sanders Peirce, vols. 1–6, Charles Hartshorne and Paul Weiss (eds.), vols. 7–8, Arthur W. Burks (ed.), Harvard University Press, Cambridge, MA. Cited as (CP volume.paragraph).
- Peirce, C.S. (1981–), Writings of Charles S. Peirce: A Chronological Edition, Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianopolis, IN. Cited as (CE volume, page).
- Peirce, C.S. (1885), "On the Algebra of Logic: A Contribution to the Philosophy of Notation", American Journal of Mathematics 7 (1885), 180–202. Reprinted as CP 3.359–403 and CE 5, 162–190.
- Peirce, C.S. (c. 1886), "Qualitative Logic", MS 736. Published as pp. 101–115 in Carolyn Eisele (ed., 1976), The New Elements of Mathematics by Charles S. Peirce, Volume 4, Mathematical Philosophy, Mouton, The Hague.
- Peirce, C.S. (1886 a), "Qualitative Logic", MS 582. Published as pp. 323–371 in Writings of Charles S. Peirce: A Chronological Edition, Volume 5, 1884–1886, Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.
- Peirce, C.S. (1886 b), "The Logic of Relatives: Qualitative and Quantitative", MS 584. Published as pp. 372–378 in Writings of Charles S. Peirce: A Chronological Edition, Volume 5, 1884–1886, Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.
- Spencer Brown, George (1969), Laws of Form, George Allen and Unwin, London, UK.
See also
Related articles
Related topics
External links
- Laws of Form web site
- Spencer-Brown's talks at Esalen 1973 — Self-referential forms are introduced in the section entitled "Degree of Equations and the Theory of Types"
- Louis H. Kauffman — Box Algebra, Boundary Mathematics, Logic, and Laws of Form
Aficionados
- See Talk:Logical graph for discussions/comments regarding this article.
- See Logical graph/Aficionados for those who have listed Logical graph as an interest.
- See Talk:Logical graph/Aficionados for discussions regarding this interest.
<sharethis />
