Peirce's rules of inference for existential graphs
sowa@watson.ibm.com
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.