The article and section linked below introduce the Double Negation Theorem (DNT) in the manner described as Consequence 1 or Reflection by Spencer Brown.

• Logical Graphs • Double Negation

Converting the planar figures used by Peirce and Spencer Brown to the graph-theoretic structures commonly used in mathematics and computer science, the double negation theorem takes the following form.

The formal system of logical graphs is defined by a foursome of formal equations, called initials when regarded purely formally, in abstraction from potential interpretations, and called axioms when interpreted as logical equivalences.  There are two arithmetic initials and two algebraic initials, as shown below.

Arithmetic Initials

Algebraic Initials

Using these equations as transformation rules permits the development of formal consequences which may be interpreted as logical theorems.  The double negation theorem is one such consequence.  The proof of the double negation theorem I give next time is adapted from the one Spencer Brown presents in his Laws of Form and credits to two of his students, John Dawes and D.A. Utting.

Resources

• Logic Syllabus
• Logical Graphs • Informal Introduction • Formal Development

cc: Cybernetics • Laws of Form • FB | Logical Graphs • Ontolog Forum • Peirce List
• Structural Modeling • Systems Science