Changes

MyWikiBiz, Author Your Legacy — Monday November 25, 2024
Jump to navigationJump to search
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

Navigation menu