Editing Propositional formula (section)

=== Substitution versus replacement ===
'''Substitution''': The variable or sub-formula to be substituted with another variable, constant, or sub-formula must be replaced in all instances throughout the overall formula.
: Example: (c & d) &or; (p & ~(c & ~d)), but  (q1 & ~q2) ≡ d. Now wherever variable "d" occurs, substitute (q<sub>1</sub> & ~q<sub>2</sub>):
:: (c & (q<sub>1</sub> & ~q<sub>2</sub>)) &or; (p & ~(c & ~(q<sub>1</sub> & ~q<sub>2</sub>)))

'''Replacement''': (i) the formula to be replaced must be within a tautology, i.e. ''logically equivalent'' ( connected by ≡ or ↔) to the formula that replaces it, and (ii) unlike substitution its permissible for the replacement to occur only in one place (i.e. for one formula).
: Example: Use this set of formula schemas/equivalences: 
:# ( (a &or; 0) ≡ a ). 
:# ( (a & ~a) ≡ 0 ). 
:# ( (~a &or; b) =<sub>Df</sub> (a → b) ). 
:# <li value="6"> ( ~(~a) ≡ a )</li>
:{{ordered list|list-style-type=lower-alpha
| start with "a": a
| Use 1 to replace "a" with (a &or; 0): (a &or; 0)
| Use the notion of "schema" to substitute b for a in 2: ( (a & ~a) ≡ 0 )
| Use 2 to replace 0 with (b & ~b): ( a &or; (b & ~b) )
| (see below for how to distribute "a &or;" over (b & ~b), etc.)
}}