# How Can One Legitimately Use the Rules of Substitution and Repalcement in a Non-Mechanical Fashion?

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.

-
Would you please define (or at least explain) the terms rule of substitution, rule of replacement, category, and equiuniform, so I can understand the question? –  Quinn Culver Aug 29 '11 at 14:49
Perhaps the parentheses are never part of the formulas themselves, and are just written in the presentation of results to help clarify what formula is being written. Each book will have a particular definition of formulas, which determines once and for all where the parentheses go, if anywhere. –  Carl Mummert Aug 29 '11 at 15:23
You have a great skill in setting storms in teacups! –  Mariano Suárez-Alvarez Aug 29 '11 at 16:12
Once again you are confusing syntax and semantics. Substitution and replacement rules don't apply to unparsed strings but, rather, to terms parsed into some (equational) language. So the rules may be interpreted as rewriting not strings but trees (representing parsed well-formed algebraic expressions). –  Bill Dubuque Aug 29 '11 at 16:13
@Doug Of course you can attempt to "simulate" this in some lower-level string language. But you have to do it faithfully - which you are not. Your problems occur only because your are not faithfully preserving the higher-level structure when you represent it in your string language. –  Bill Dubuque Aug 29 '11 at 16:46

We commonly drop parentheses in the natural-language presentations about formal logic. So, assuming that your formal definition of well formed formulas includes parentheses, the first thing you have to do when reading a natural-language presentation is to determine which well formed formula the authors refer to when they write something like "$x \to y$".
For example, an author might write something like "the result of substituting $y$ with $y \to x$ in $x \to y$ is $x \to (y \to x)$." Even if none of the expressions inside the quotes is actually a well-formed formula, it is still completely clear what they mean. We just have to look up the formal definition of a well-formed formula and then translate the natural-language text using that definition.
The avoidance of parentheses is made easier by conventions that give some operations precedence over others. For example $\lnot A \to B$ means $(\lnot A) \to B$.
Humans read proofs in natural language, and we do a good job at checking them (in my opinion). If someone wants to run a proof through a formal proof checker, that's a different matter - the proofs in math textbooks are not intended to be formally verified, they are intended for humans. Most authors assume that if they say "Replace all the 5s in the number $17^8$ with 6s", the reader will not respond that "$17^8$ does not have any 5s in it". The same goes for formulas in logic. –  Carl Mummert Aug 29 '11 at 23:02