Propositional Equation Reasoning Systems

Note. The MathJax parser is not rendering this page properly.
Until it can be fixed please see the InterSciWiki version.

This article develops elementary facts about a family of formal calculi described as propositional equation reasoning systems (PERS). This work follows on the alpha graphs that Charles Sanders Peirce devised as a graphical syntax for propositional calculus and also on the calculus of indications that George Spencer Brown presented in his Laws of Form.

Formal development

The first order of business is to give the exact forms of the axioms that we use, devolving from Peirce's “Logical Graphs” via Spencer-Brown's Laws of Form (LOF). In formal proofs, we use a variation of the annotation scheme from LOF 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, \(I_1\!\) and \(I_2,\!\) and the algebraic initials, \(J_1\!\) and \(J_2.\!\)

	(1)
	(2)
	(3)
	(4)

One way of assigning logical meaning to the initial equations is known as the entitative interpretation \((\mathrm{En}).\!\) Under \(\mathrm{En},\!\) the axioms read as follows:

\(\begin{matrix} I_1 & : & \mathrm{true} ~\mathrm{or}~ \mathrm{true} & = & \mathrm{true} \\ I_2 & : & \mathrm{not}~ \mathrm{true} & = & \mathrm{false} \\ J_1 & : & a ~\mathrm{or}~ \mathrm{not}~ a & = & \mathrm{true} \\ J_2 & : & (a ~\mathrm{or}~ b) ~\mathrm{and}~ (a ~\mathrm{or}~ c) & = & a ~\mathrm{or}~ (b ~\mathrm{and}~ c) \end{matrix}\)

Another way of assigning logical meaning to the initial equations is known as the existential interpretation \((\mathrm{Ex}).\!\) Under \(\mathrm{Ex},\!\) the axioms read as follows:

\(\begin{matrix} I_1 & : & \mathrm{false} ~\mathrm{and}~ \mathrm{false} & = & \mathrm{false} \\ I_2 & : & \mathrm{not}~ \mathrm{false} & = & \mathrm{true} \\ J_1 & : & a ~\mathrm{and}~ \mathrm{not}~ a & = & \mathrm{false} \\ J_2 & : & (a ~\mathrm{and}~ b) ~\mathrm{or}~ (a ~\mathrm{and}~ c) & = & a ~\mathrm{and}~ (b ~\mathrm{or}~ c) \end{matrix}\)

All of the axioms in this set have the form of equations. This means that all of the inference licensed by them are reversible. The proof annotation scheme employed below makes use of a double bar ═════ to mark this fact, but it will often be left to the reader to decide which of the two possible ways of applying the axiom is the one that is called for in a particular case.

Peirce introduced these formal equations at a level of abstraction that is one step higher than their customary interpretations as propositional calculi, which two readings he called the Entitative and the Existential interpretations, here referred to as \(\mathrm{En}\!\) and \(\mathrm{Ex},\!\) respectively. The early CSP, as in his essay on “Qualitative Logic”, and also GSB, emphasized the \(\mathrm{En}\!\) interpretation, while the later CSP developed mostly the \(\mathrm{Ex}\!\) interpretation.

Frequently used theorems

C₁. Double negation

The first theorem goes under the names of Consequence 1 \((C_1),\!\) the double negation theorem (DNT), or Reflection.

(5)

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.

(6)

The steps of this proof are replayed in the following animation.

(7)

C₂. 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 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 names of Consequence 2 \((C_2)\!\) or Generation.

(8)

Here is a proof of the Generation Theorem.

(9)

The steps of this proof are replayed in the following animation.

(10)

C₃. Dominant form theorem

The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as Consequence 3 \((C_3)\!\) 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.

(11)

Here is a proof of the Dominant Form Theorem.

(12)

The following animation provides an instant re*play.

(13)

Exemplary proofs

Based on the axioms given at the outest, and aided by the theorems recorded so far, it is possible to prove a multitude of much more complex theorems. A couple of all-time favorites are given next.