About 100 years ago, one of the founders of modern formal logic, the American logician and philosopher of language Charles Sanders Peirce, expressed concerns regarding the traditional linear notation of formal logic. Thus, Peirce proposed an alternative system with a more graphical notation, called Existential Graphs (Peirce, 1933) .
Existential Graphs are a little-known diagrammatic representation that can be used for propositional, first-order, and modal logic. They hardly use any special symbols and contain only 4 rules of inferences but are sound and complete.
Alpha is the part of Existential Graphs (EG) corresponding to propositional logic (PL).
To assert some statement in EG, you put the symbolization of that statement on a sheet of paper, called the 'Sheet of Assertion' (SA) .
Notice that the location of the symbolization on the SA does not matter:
By drawing the symbolization of two statements on the SA, you are asserting the truth of both statements at once. Therefore, mere juxtaposition of two symbolizations on the SA can be interpreted as the assertion of a single conjunction.
This EG can be interpreted as the assertion of two statements: P, Q or as a conjunction: P ∧ Q
Since any number of symbolizations can be juxtaposed on the SA, juxtaposition becomes a kind of generalized conjunction. Since the location of each of the symbolizations on the SA does not matter, no particular order on these conjuncts is imposed. This coincides with our abstract understanding of conjunction which gives Existential Graphs an important advantage over the linear notation of traditional propositional logic.
For example by symbolizing P, Q on the SA, the EG can represent P , Q , P ∧ Q , and Q ∧ P all at once!
Asserting a negation can be done by drawing a cut around a symbol. A cut can be any enclosing figure. In Existential Graphs, an empty graph represents a tautology whereas an empty cut represents a contradiction.
This EG represents: ¬P
This EG represents a Tautology: ⊤
This EG represents a Contradiction: ⊥
Cuts can be nested, each nested symbol is one level above its parent.
In this EG P and Q is level 2, the cuts surrounding them are level 1, and the outermost cut is level 0
So far using these rules of symbolization can represent conjunction, negation, and simple letters for atomic statements, any compound or truth functional statement can be represented by an Existential Graph. Because conjunction and negation form an expressively complete set of operators, EG is also expressively complete.
Examples of EG to propositional logic
Insertion and Erasure are rules of inference while Double cut and Iteration/De-iteration are rules of Equivalence.
Insertion allows inserting a graph at any odd level.
Erasure allows erasing any graph from any even level.
Double Cut allows drawing or erasing a double cut around any subgraph. This is similar to a double negation in propositional logic.
Iteration/De-iteration allows placing or erasing a copy of any subgraph at any nested level.
A formal proof in Existential Graphs consists in the successive application of inference rules to transform one graph into another. Formal proofs in EG are used just as in traditional logic