Existential graphs — Peirce, Praeclarum Theorema, Sowa’s rules

A whole research direction in computer science deals with so-called “conceptual graphs”. These graphs are Peirce’s existential graphs [Sowa2017a]; see also Gandon [Gand2002] on mapping between Conceptual Graphs (CG) and RDF graphs.

The Praeclarum Theorema of Leibniz has the form:
((p → r) ∧ (q → s)) → ((p ∧ q) → (r ∧ s))
The OntoGraph in Figure praeclarum-theorema shows the representation with the formula reificator ~Praeclarum. By nesting expressions, no brackets are needed to model the theorem.

Fig. poeschl-examples — Examples of existential graphs (canonical assets on taoke.de).

Rules in Sowa (EG tutorial): where (i) stands for insertion rule and (e) stands for erase rule:

• 1.(i) In a negative (shaded) area, one or more nodes may be inserted.
• 1.(e) In a positive (unshaded) area, one or more nodes may be erased.
• 2.(i) One or more nodes in any area a may be iterated (copied) in the same area a or into any area nested in a.
• 2.(e) Any node that could have been derived by rule 2i may be erased.
• 3.(i) A double negation may be drawn around any collection of zero or more nodes in any area.
• 3.(e) Any double negation in any area may be erased.

Pöschel (2004) gives the corresponding German formulations; see the canonical page for the full parallel list. Pöschel shows that the Praeclarum theorem can be proved in only 7 steps using Peirce’s existential graphs; Whitehead and Russell (1910) needed many more steps and non-trivial axioms [Sowa2018a].

Fig. proof-prclm-thrm — Proof of the Praeclarum Theorema.

“After only four steps, the graph looks almost like the desired conclusion, except for a missing copy of s in the innermost area. Since that area is positive, the only way to get s in there is by iterating some graph that contains s and erasing the parts that are not needed. This proof illustrates the usual pattern for deriving a theorem by Peirce’s rules…” — Sowa