Editing Laws of Form (section)

===Rules governing logical equivalence===
The sign '=' may link two logically equivalent expressions; the result is an [[equation]]. By "logically equivalent" is meant that the two expressions have the same simplification. [[Logical equivalence]] is an [[equivalence relation]] over the set of primary algebra formulas, governed by the rules R1 and R2. Let "C" and "D" be formulae each containing at least one instance of the subformula ''A'':
*'''R1''', ''Substitution of equals''. Replace ''one or more'' instances of ''A'' in ''C'' by ''B'', resulting in ''E''. If ''A''=''B'', then ''C''=''E''.
*'''R2''', ''Uniform replacement''. Replace ''all'' instances of ''A'' in ''C'' and ''D'' with ''B''. ''C'' becomes ''E'' and ''D'' becomes ''F''. If ''C''=''D'', then ''E''=''F''. Note that ''A''=''B'' is not required.
'''R2''' is employed very frequently in ''primary algebra'' demonstrations (see below), almost always silently. These rules are routinely invoked in [[logic]] and most of mathematics, nearly always unconsciously.

The ''primary algebra'' consists of [[equations]], i.e., pairs of formulae linked by an [[infix operator]] '='. '''R1''' and '''R2''' enable transforming one equation into another. Hence the ''primary algebra'' is an ''equational''  formal system, like the many [[algebraic structures]], including [[Boolean algebra (structure)|Boolean algebra]], that are [[variety (universal algebra)|varieties]]. Equational logic was common before ''Principia Mathematica'' (e.g. {{harvp|Johnson|1892}}), and has present-day advocates ({{harvp|Gries|Schneider|1993}}).

Conventional [[mathematical logic]] consists of [[Tautology (logic)|tautological]] formulae, signalled by a prefixed [[Turnstile (symbol)|turnstile]]. To denote that the ''primary algebra'' formula ''A'' is a [[Tautology (logic)|tautology]], simply write "''A'' =[[Image:Laws of Form - cross.gif]] ". If one replaces '=' in '''R1''' and '''R2''' with the [[biconditional]], the resulting rules hold in conventional logic. However, conventional logic relies mainly on the rule [[modus ponens]]; thus conventional logic is ''ponential''. The equational-ponential dichotomy distills much of what distinguishes mathematical logic from the rest of mathematics.