Changes

Line 582: Line 582:  
By way of gaining a minimal experience with how equational proofs look in the present forms of syntax, I will lay out the proofs of a few essential theorems in the primary algebra.
 
By way of gaining a minimal experience with how equational proofs look in the present forms of syntax, I will lay out the proofs of a few essential theorems in the primary algebra.
   −
The first theorem is known as the ''Double Negation Theorem'' (DNT).
+
The first theorem goes under the names of ''Consequence&nbsp;1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.
   −
<pre>
+
{| align="center" cellpadding="10"
o-----------------------------------------------------------o
+
| [[Image:Logical_Graph_Figure_24.jpg|500px]]
| C_1.` Double Negation Theorem ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
+
|}
o-----------------------------------------------------------o
  −
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` a ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` a ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
o-----------------------------------------------------------o
  −
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ((a)) ` ` ` = ` ` ` ` a ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
o-----------------------------------------------------------o
  −
| ` ` ` ` ` ` ` Reflect <---- | ----> Reflect ` ` ` ` ` ` ` |
  −
o-----------------------------------------------------------o
  −
</pre>
     −
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&nbsp;1'' (''C''<sub>1</sub>) or as ''Reflection'' in LOF.
+
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.
   −
<pre>
+
{| align="center" cellpadding="10"
o-----------------------------------------------------------o
+
| [[Image:Logical_Graph_Figure_25.jpg|500px]]
| C_1.` Double Negation Theorem.` Proof.` ` ` ` ` ` ` ` ` ` |
+
|}
o-----------------------------------------------------------o
+
 
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
+
{| align="center" cellpadding="10"
| ` ` ` ` ` a o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
+
| [[Image:Logical_Graph_Figure_26.jpg|500px]]
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
+
|}
| ` ` ` ` ` ` ` \ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
  −
| ` ` ` ` ` ` ` `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
  −
</pre>
      
==Weed and seed theorem==
 
==Weed and seed theorem==
12,080

edits