Charles Stewart said I might ask the following as a question here.
If an author doesn't use parentheses for logical expressions like x->y, say in propositional calculus, I don't see how the introduction of parentheses comes as justified when using the rule of uniform substitution, or the rule of replacement on those expression. In other words, when taking unparenthesized expressions like x->y, parenthesizing them, and uniformly substituting or replacing the parenthesized expression for a variable or expression respectively, I don't see how one could do this without implicitly referring to the meaning of the unparenthesized expression like x->y. How is the unparenthesized statement of the same category as the parenthesized statement, especially if the unparenthesized statement is not a wff, while the parenthesized statement is a wff? If we insert parentheses when replacing a statement p by statement q, how is the parenthesized statement q' equiform with q? Doesn't the rule of replacement, to get used correctly, require mechanical replacement? Doesn't the rule of uniform substitution also require mechanical substitution?
"Equiformity" just means "equal in terms of form". This includes the order of the symbols in the string, and we can't rotate, twist, reflect, etc. or change the symbols... "p" is not equiform with "q" even though one is a reflection of the other. Only "p" is equiform with "p", though that isn't quite precise, since other "p"s exist equiform.
The rule of substitution basically says (this might not quite work as a precise definition) that if, for any thesis of the logical system with variable "x", we uniformly substitute all instances of "x" by any wff, then we may infer the resulting expression also as a thesis of the system. For example, if (q&(p*q)) is a thesis of some logical system, and also if (p!q) is a wff, then we may infer ((p!q)&(p*(p!q)) as a thesis of the logical system, since if one starts with "(q&(p*q))" and we substitute each instance of q with (p!q), one obtains ((p!q)&(p*(p!q)). The removed wff need not come as logically equivalent to the inserted wff.
The rule of replacement more-or-less says that we may replace any given wff x with any other logically equivalent wff y freely, as opposed to uniformly, within any wff z whatsoever without changing z in any "significant" way (this is not a formal definition, this gets tricky to make precise). In other words, if we apply the rule of replacement, it will simply not happen that "z" changes from a theorem to a contradiction, a contradiction to a theorem, a contingency to a theorem, a theorem to a contingency, a contradiction to a contingency, or a contingency to a contradiction. So, if we replace an instance of x with y within z obtain z', and if we have z as a theorem, we may infer z' as a theorem also (except "theorem" could get uniformly substituted by "contingency" or "contradiction"). For example, if we have ((p^q)&r)==((p@q)!s), and we have ((r@((p^q)&r))@((p^q)&r)) as either a theorem, or a contingency, or a contradiction, then we may infer ((r@((p@q)!s))@((p^q)&r)) as a theorem, contingency, or contradiction respectively. In contradistinction to the example above, the left instance of ((p^q)&r) has gotten replaced by ((p@q)!s), while the right instance has not.
By theorem I mean a formally provable wff.
By contradiction I mean that the negation of the contradiction comes as a theorem.
By contingency I mean a wff which for which the wff can't get proven, nor can its negation get proven. I hope the explanations help.