ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 2
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
The first theorem is known as the "Double Negation Theorem" (DNT).
o-----------------------------------------------------------o
| C1. Double Negation Theorem |
o-----------------------------------------------------------o
| |
| a |
| o |
| | |
| o |
| | a |
| @ = @ |
| |
o-----------------------------------------------------------o
| |
| ((a)) = a |
| |
o-----------------------------------------------------------o
| Reflect <---- | ----> Reflect |
o-----------------------------------------------------------o
The proof that follows it is derived from the one that was given
by George Spencer Brown in his book 'Laws of Form', and credited
to two of his students, John Dawes and D.A. Utting. This result
is annotated as "Consequence 1" (C1) or as "Reflection" in LOF.
o-----------------------------------------------------------o
| C1. Double Negation Theorem. Proof. |
o-----------------------------------------------------------o
| |
| a o |
| \ |
| \ |
| o |
| \ |
| \ |
| @ |
| |
o=============================< I2. Unfold "(())" >=========o
| |
| a o o |
| \ / |
| \ / |
| o o |
| \ / |
| \ / |
| @ |
| |
o=============================< J1. Insert "(a)" >==========o
| |
| a o |
| / |
| / |
| a o a o o |
| \ \ / |
| \ \ / |
| o o |
| \ / |
| \ / |
| @ |
| |
o=============================< J2. Distribute "((a))" >====o
| |
| a o a o |
| \ \ |
| \ \ |
| o o a o |
| \ \ / |
| \ \ / |
| a o o |
| \ / |
| \ / |
| o |
| / |
| / |
| @ |
| |
o=============================< J1. Delete "(a)" >==========o
| |
| a o |
| \ |
| \ |
| o o |
| \ \ |
| \ \ |
| a o o |
| \ / |
| \ / |
| o |
| / |
| / |
| @ |
| |
o=============================< J1. Insert "a" >============o
| |
| a o |
| \ |
| \ |
| o o a |
| \ \ |
| \ \ |
| a o o a |
| \ / |
| \ / |
| o |
| / |
| / |
| @ |
| |
o=============================< J2. Collect "a" >===========o
| |
| a o |
| \ |
| \ |
| o o a |
| \ \ |
| \ \ |
| o o |
| \ / |
| \ / |
| o |
| / |
| / |
| a @ |
| |
o=============================< J1. Delete "((a))" >========o
| |
| o |
| \ |
| \ |
| o |
| / |
| / |
| a @ |
| |
o=============================< I2. Refold "(())" >=========o
| |
| a |
| @ |
| |
o=============================< QED >=======================o
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o