Editing Laws of Form (section)

===Initials===
An ''initial'' is a ''primary algebra'' equation verifiable by a [[decision procedure]] and as such is ''not'' an [[axiom]]. ''LoF'' lays down the initials:

{|
|-
| 
*J1:
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
|
{|
|-
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| A
|}
| A
|}
|}
| = .
|}
The absence of anything to the right of the "=" above, is deliberate.

{|
|-
| 
*J2:
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
|
{|
|-
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| A
|}
|
{|style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| B
|}
|}
|}
| C
| =
|
{|style="border-top: 2px solid black; border-right: 2px solid black;"
|-
|
{|
|-
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| A C
|}
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| B C
|}
|}
|}
|.
|}

'''J2''' is the familiar [[distributive law]] of [[sentential logic]] and [[Boolean algebra (structure)|Boolean algebra]].

Another set of initials, friendlier to calculations, is:

{|
|-
| 
*J0:
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
|
{|
|-
|
|}
|}
|}
| A
| =
| A.
|}

{|
|-
|
*J1a:
|
{|
|-
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| A
|}
| A
|}
| =
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
|
{|
|-
|
|}
|}
|.
|}

{|
|-
| 
*C2:
| A
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| A B
|}
| = 
| A
|
{| style="border-top: 2px solid black; border-right: 2px solid black;"
|-
| B
|}
|.
|}

It is thanks to '''C2''' that the ''primary algebra'' is a [[lattice (order)|lattice]]. By virtue of '''J1a''', it is a [[complemented lattice]] whose upper bound is [[Image:Laws_of_Form_-_cross.gif]]. By '''J0''', [[Image:Laws_of_Form_-_double_cross.gif]] is the corresponding lower bound and [[identity element]]. '''J0''' is also an algebraic version of '''A2''' and makes clear the sense in which [[Image:Laws_of_Form_-_double_cross.gif]] aliases with the blank page.

T13 in ''LoF'' generalizes '''C2''' as follows. Any ''primary algebra'' (or sentential logic) formula ''B'' can be viewed as an [[ordered tree]] with ''branches''. Then:

'''T13''': A [[formula|subformula]] ''A'' can be copied at will into any depth of ''B'' greater than that of ''A'', as long as ''A'' and its copy are in the same branch of ''B''. Also, given multiple instances of ''A'' in the same branch of ''B'', all instances but the shallowest are redundant.

While a proof of T13 would require [[mathematical induction|induction]], the intuition underlying it should be clear.

'''C2''' or its equivalent is named:
*"Generation" in ''LoF'';
*"Exclusion" in Johnson (1892);
*"Pervasion" in the work of William Bricken.
Perhaps the first instance of an axiom or rule with the power of '''C2''' was the "Rule of (De)Iteration", combining T13 and ''AA=A'', of [[Charles Sanders Peirce|C. S. Peirce]]'s [[existential graph]]s.

''LoF'' asserts that concatenation can be read as [[commutativity|commuting]] and [[associativity|associating]] by default and hence need not be explicitly assumed or demonstrated. (Peirce made a similar assertion about his [[existential graph]]s.) Let a period be a temporary notation to establish grouping. That concatenation commutes and associates may then be demonstrated from the:
* Initial ''AC.D''=''CD.A'' and the consequence ''AA''=''A''.{{sfnp|Byrne|1946}} This result holds for all [[lattice (order)|lattices]], because ''AA''=''A'' is an easy consequence of the [[absorption law]], which holds for all lattices;
* Initials ''AC.D''=''AD.C'' and '''J0'''. Since '''J0''' holds only for lattices with a lower bound, this method holds only for [[bounded lattice]]s (which include the ''primary algebra'' and '''2'''). Commutativity is trivial; just set ''A''=[[Image:Laws_of_Form_-_double_cross.gif]]. Associativity: ''AC.D'' = ''CA.D'' = ''CD.A'' = ''A.CD''.
Having demonstrated associativity, the period can be discarded.

The initials in {{harvp|Meguire|2011}} are ''AC.D''=''CD.A'', called '''B1'''; '''B2''', J0 above; '''B3''', J1a above; and '''B4''', C2. By design, these initials are very similar to the axioms for an [[abelian group]], '''G1-G3''' below.