**Mail folder:**SRKB Mail**Next message:**phayes@herodotus.cs.uiuc.edu: "Re:Peirce's rules of inference for existential graphs"**Previous message:**sowa@watson.ibm.com: "Theories, Axiomatizations, and Contexts"**Reply:**phayes@herodotus.cs.uiuc.edu: "Re:Peirce's rules of inference for existential graphs"

Message-id: <199208272319.AA26674@venera.isi.edu> Date: Thu, 27 Aug 92 19:17:18 EDT From: sowa@watson.ibm.com To: INTERLINGUA@ISI.EDU, SRKB@ISI.EDU, CG@CS.UMN.EDU Subject: Peirce's rules of inference for existential graphs

In a previous note, I said that Bertrand Russell had made a "dumb choice" in using the linear notation for predicate calculus, which was based on Charles Sanders Peirce's notation of 1883. Instead, he should have used Peirce's graph notation of 1896. That phrase "dumb choice" was not an email "flame", but a considered opinion, for which I would like to give the justification. First of all, Russell knew of Peirce's work. He was familiar with Schroeder's three volume _Vorlesungen ueber Algebra der Logik_ (1895), which used Peirce's notation of 1883 and gave him full credit for it. In the preface to the Principia Mathematica, Russell gave grandiloquent praise to Frege, who had invented the first system of first-order logic in 1879. Yet he didn't mention a word about Peirce, who had in 1883 independently developed the linear notation that was the direct ancestor of the notation that Russell actually used. Russell's omission was not an oversight, but more likely a deliberate slight, since there had been some quarrels between Peirce and Russell. Peirce tended to be irascible and would no doubt have been eloquent in letting Russell know that he was making a "dumb choice". Peirce defined the existential graphs and the rules of inference for them in 1896. Yet for essentially every theorem in the Principia Mathematica, which was published 14 years later, Peirce's rules give shorter and simpler proofs. As an example, following is Proposition 3.47 from Whitehead and Russell (1910), which Leibniz had called the Praeclarum Theorema (Splendid Theorem): ((p -> r) & (q -> s)) -> ((p & q) -> (r & s)). In the Principia, the proof of this theorem cites two other propositions, 3.22 and 3.26. The proofs of those two cite other propositions, axioms, and definitions. Altogether, the complete proof has 28 ancillary propositions with a total of 43 inference steps scattered over the first three chapters of the Principia Mathematica. By contrast, the proof of the equivalent graph in Peirce's system starts >From an empty sheet of paper and takes only 8 steps. Peirce's rules are actually a generalization of the system of natural deduction by Gentzen (1934), which was published 38 years later. For more detail about Peirce's system, I am appending an extract from a paper that I was writing. See also the book by Don Roberts, _The Existential Graphs of Charles S. Peirce_, Mouton, The Hague, 1973. John Sowa ________________________________________________________________________ Charles S. Peirce defined a complete set of inference rules for the first-order subset of existential graphs, with extensions to modal and higher-order logic. Since his graphs had no variables, his rules of inference are not based on substitutions for variables. Instead, they are all based on the primitive operations of copying and erasing graphs in various contexts. In the first-order subset, the only relation that may be attached to a context is negation. A context with no negations or nested inside an even number of negations is said to be positive, and a context nested inside an odd number of negations is said to be negative. Following are some examples: o ZERO NEGATIONS: The outermost context is what Peirce called the sheet of assertion. Any graph drawn on the sheet of assertion is in a positive context. o ONE NEGATION: Any graph nested in a context marked with the NEG relation or the ^ symbol is in a negative context. The antecedent or if-part of an implication is also a negative context, since (p -> q) is equivalent to ^[p ^[q]]. o TWO NEGATIONS: In Peirce's existential graphs, as in other systems of classical first-order logic, two negative contexts with nothing between the inner and outer contexts cancel each other out to make a positive context. The consequent of an implication is also a positive context, since q in ^[p ^[q]] is nested inside two negations. In the implication, the two negations cannot be erased, since the graph p occurs between them; but even when not erased, the double negation makes the context positive. o THREE OR MORE NEGATIONS: Larger numbers of nested negations can be reduced to combinations of implications and single negations. The nest ^[p ^[q ^[r ^[s]]]], for example, is equivalent to (p -> (q & (r -> s))). Given this basic representation for contexts and negations, Peirce defined five rules of inference and one axiom that provide a complete deductive system for propositional logic: o ERASURE: Any graph g may be erased in a positive context. o INSERTION: Any graph g may be inserted in a negative context. o ITERATION: If a graph g occurs in a context c, another copy of g may be inserted in the same context c or in any context nested in c. o DEITERATION: Any graph g that may have been derived by iteration may be erased; i.e. if g is identical to another graph in the same context or a containing context, g may be erased. o DOUBLE NEGATION: Two negations, ^[^[ ... ]] with nothing between the inner and outer negation, may be drawn around or erased from any set of graphs in any context. o AXIOM: The only axiom is the empty set; i.e. a blank sheet of assertion is the starting point for proving any theorem. To illustrate these rules, consider the rule of modus ponens, which derives q from the premises p and (p -> q). In Peirce's form, the starting premises would be p ^[p ^[q]]. By the rule of deiteration, the nested p may be erased, since it is identical to the outer p: p ^[ ^[q]]. Now there is a double negation with nothing between the inner and outer negations. Therefore, both negative contexts may be erased: p q. Now both p and q are in a positive context (no negations). Therefore, it is permissible to erase p and leave q by itself: q. All other rules of inference for propositional logic can be performed by combinations of Peirce's rules. Conversely, Peirce's rules can be shown to be derived rules of inference in any system of classical logic. For a complete system of first-order logic, Peirce's five rules are applied to coreference links: a coreference link may be erased in a positive context, inserted in a negative context, extended (i.e. iterated) into an inner context from an outer context, or retracted (i.e. deiterated) >From an inner context to an outer context; and double negations may cross coreference links when they are drawn around or erased from any collection of graphs. Peirce's system of deduction has a remarkable property that makes it ideally suited to reasoning about contexts: none of the rules are sensitive to the depth of nesting; they depend only on whether there is an odd number or even number of negations. Therefore, any proof that can be carried out directly on the sheet of assertion can also be carried out in a context nested two levels or even two thousand levels deep. This property allows a message to be imported into a context by iteration and then used in a proof inside that context. Proposition 3.47 of the Principia Mathematica, which Leibniz called the Praeclarum Theorema, occurs towards the end of Chapter 3 and uses almost all of the techniques of propositional logic that were developed by Whitehead and Russell. One of the early theorem provers in AI, the Logic Theorist (Newell, Shaw, & Simon 1957), attempted to mimic Whitehead and Russell's proof techniques directly; but it was barely able to prove some of the theorems in Chapter 2 and was never applied to the more difficult theorems in Chapter 3. More efficient techniques, such as resolution (Robinson 1965), could easily prove any of the propositional theorems in the first three chapters as well as most of the first-order theorems in later chapters. As an illustration, following is the statement of Proposition 3.47: ((p -> r) & (q -> s)) -> ((p & q) -> (r & s)). In a proof by resolution, the first step is to negate this formula and convert it to a list of formulas in clause form. Following is the collection of four clauses derived by that procedure: p, q, ^p|r, ^q|s, ^r|^s. Eleven steps are required to derive this set of clauses from the original formula, and four additional resolution steps are necessary to demonstrate a contradiction - thereby proving the nonnegated formula. Resolution theorem proving and its variants are widely used in AI, but one disadvantage is the need to convert a problem to clause form before the method can be applied. As this example illustrates, the set of clauses bears little resemblance to the original Proposition 3.47. For a collection of encapsulated objects, it would not be possible to do deductions by resolution without destroying the structure of the nest of contexts and the object descriptions in them. Unlike resolution, Peirce's rules do not disturb the structure of the encapsulated contexts. On the contrary, they are stated directly in terms of the contexts. Furthermore, they allow graphs to be imported into a small context where only the information relevant to a proof needs to be considered. Like resolution and every other sophisticated theorem proving technique, Peirce's rules are NP-complete; i.e. the amount of computation can grow exponentially. But since they allow large problems to be broken down into smaller contexts, they can keep the exponent small. With a small enough exponent, an exponential growth is easily manageable. *** At this point, Figure 14 shows Peirce's graphic notation, *** which is much prettier than the linear form that is *** expressible by email in the ASCII character set: ^[ ^[p ^[r]] ^[q ^[s]] ^[ ^[p q ^[r s]] ] ]. Figure 14 shows Proposition 3.47 in Peirce's original notation for existential graphs. In that form, he used an oval to enclose contexts, and the ^ symbol was implicit, since negation is the only context modifier needed for first-order logic. For the four implications, each -> symbol in the formula corresponds to a pair of ovals in Figure 14. To prove the theorem, it is necessary to derive Figure 14 from the axiom, namely, a blank sheet of paper. Since nothing can be erased from a blank sheet and there are no negative contexts in which anything can be inserted, the only rule of inference that can be applied is to draw a double negation around the empty set. In the linear notation with the ^ symbol, that would produce the following graph: ^[ ^[ ] ]. Now there is a negative context in which other graphs may be inserted by the rule of insertion. The first step is to insert the implication ^[p ^[r]]. The second step is to insert the other implication ^[q ^[s]]. The result is the following graph: ^[ ^[p ^[r]] ^[q ^[s]] ^[ ] ]. Now by iteration, it is possible to copy the graph ^[p ^[r]] into the empty context on the second line: ^[ ^[p ^[r]] ^[q ^[s]] ^[ ^[p ^[r]] ] ]. This graph is beginning to take a shape that looks similar to Figure 14. To make it identical to Figure 14, it is necessary to get a copy of q in the context with p on the second line and a copy of s in the context with r. Getting q into the context with p is easy, since it is a negative context (nested 3 levels deep) and q may be inserted by the rule of insertion: ^[ ^[p ^[r]] ^[q ^[s]] ^[ ^[p q ^[r]] ] ]. Since the context with r is positive, it is not possible to insert s directly. Instead, the first step is to iterate the graph ^[q ^[s]] >From the first line into the context with r on the second line: ^[ ^[p ^[r]] ^[q ^[s]] ^[ ^[p q ^[r ^[q ^[s]] ]] ] ]. Now by the rule of deiteration, the second q on the second line may be erased because it is identical to the first q on the second line: ^[ ^[p ^[r]] ^[q ^[s]] ^[ ^[p q ^[r ^[ ^[s]] ]] ] ]. Finally, the double negation around s on the second line may be erased. After 8 rule applications, the result is the linear representation of the graph in Figure 14: ^[ ^[p ^[r]] ^[q ^[s]] ^[ ^[p q ^[r s]] ] ]. This derivation should be compared to the 43 inference steps with 28 references to other propositions in the Principia. It should also be compared to the 15 steps needed to convert the formula to clause form and apply resolution. All of the steps in Peirce's rules consist of copying and erasing graphs in various contexts. There are no substitutions, no complex transformations, and no need to disturb the structure of nested contexts.