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 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 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== |