Changes

The first theorem goes under the names of ''Consequence&nbsp;1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.

The first theorem goes under the names of ''Consequence&nbsp;1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.

{| align="center" border="0" cellpadding="10" cellspacing="0"

{| align="center" cellpadding="10"

| [[Image:Logical_Graph_Figure_24.jpg|500px]] || (24)

| [[Image:Logical_Graph_Figure_24.jpg|500px]] || (24)

|}

|}

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.

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.

{| align="center" border="0" cellpadding="10" cellspacing="0"

{| align="center" cellpadding="10"

| [[Image:Logical_Graph_Figure_25.jpg|500px]] || (25)

| [[Image:Logical_Graph_Figure_25.jpg|500px]] || (25)

|}

|}

{| align="center" border="0" cellpadding="10" cellspacing="0"

{| align="center" cellpadding="10"

| [[Image:Logical_Graph_Figure_26.jpg|500px]] || (26)

| [[Image:Logical_Graph_Figure_26.jpg|500px]] || (26)

|}

|}

One theorem of frequent use goes under the nickname of the ''weed and seed theorem'' (WAST).  The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader.  What the WAST says is that a label can be freely distributed or freely erased anywhere in a subtree whose root is labeled with that label.  The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem.  In LOF, it goes by the names of ''Consequence&nbsp;2'' <math>(C_2)\!</math> or ''Generation''.

One theorem of frequent use goes under the nickname of the ''weed and seed theorem'' (WAST).  The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader.  What the WAST says is that a label can be freely distributed or freely erased anywhere in a subtree whose root is labeled with that label.  The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem.  In LOF, it goes by the names of ''Consequence&nbsp;2'' <math>(C_2)\!</math> or ''Generation''.

{| align="center" border="0" cellpadding="10" cellspacing="0"

{| align="center" cellpadding="10"

| [[Image:Logical_Graph_Figure_27.jpg|500px]] || (27)

| [[Image:Logical_Graph_Figure_27.jpg|500px]] || (27)

|}

|}

Here is a proof of the Generation Theorem.

Here is a proof of the Generation Theorem.

{| align="center" border="0" cellpadding="10" cellspacing="0"

{| align="center" cellpadding="10"

| [[Image:Logical_Graph_Figure_28.jpg|500px]] || (28)

| [[Image:Logical_Graph_Figure_28.jpg|500px]] || (28)

|}

|}

The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as ''Consequence&nbsp;3'' <math>(C_3)\!</math> or ''Integration''.  A better mnemonic might be ''dominance and recession theorem'' (DART), but perhaps the brevity of ''dominant form theorem'' (DFT) is sufficient reminder of its double-edged role in proofs.

The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as ''Consequence&nbsp;3'' <math>(C_3)\!</math> or ''Integration''.  A better mnemonic might be ''dominance and recession theorem'' (DART), but perhaps the brevity of ''dominant form theorem'' (DFT) is sufficient reminder of its double-edged role in proofs.

{| align="center" border="0" cellpadding="10" cellspacing="0"

{| align="center" cellpadding="10"

| [[Image:Logical_Graph_Figure_29.jpg|500px]] || (29)

| [[Image:Logical_Graph_Figure_29.jpg|500px]] || (29)

|}

|}

Here is a proof of the Dominant Form Theorem.

Here is a proof of the Dominant Form Theorem.

{| align="center" border="0" cellpadding="10" cellspacing="0"

{| align="center" cellpadding="10"

| [[Image:Logical_Graph_Figure_30.jpg|500px]] || (30)

| [[Image:Logical_Graph_Figure_30.jpg|500px]] || (30)

|}

|}