RENAMING RULES IN CONVENTIONAL NOTATION

We are still using what is called an intelim (introduction and elimination) system of natural deduction. Most of the rules, such as A elim or O int, remain the same, only we use the appropriate symbols in place of the letters (& elim and v int). In a few cases it is simply more efficient to use traditional references:
DN (double negation) in place of N subs
DeM (for DeMorgan's laws) in place of AN subs and ON subs
UQ int/elim (universal quantifier introduction/elimination) in place of V int/elim
EQ int/elim (existential quantifier introduction/elimination) in place of W int/elim
QN (quantifier negation) in place of VW subs

Some rules familiar in other systems (such as the hypothetical syllogism) are not used in ours, and we use the rule of ~->subs that is normally not part of other systems. Many of our rules do have alternate names, for instance:
Modus ponens for -> elim
Modus tollens for a combined move of ->subs and ->elim
Disjunctive syllogism for v elim
Addition for v int
Material implication for ->v subs

Working with multiple quantifiers does involve certain procedures intended to preserve the consistency of an instantiated expression with its original formula. The key notion is that any inference rule (any introduction or elimination) must be applied to the so-called main connective (what would have been the final letter in a PLN string). For example, in the formula (x)(Ey)(z)(Fxy->Gyz), we would instantiate from the left or the outside in. In generalizing on a formula such as Fab->Gba we could start with a or with b and build from the inside out (and, yes, we could hold back an identical letter, such as the a in Gba, in order to build several distinct formulas. A key point, however, is that we cannot use UQ int for a name that is originally brought in by EQ elim or as a hyp (until after we reach the corresponding hyp elim, sometimes called discharging the assumption).

Three cautions, then:
(1) Avoid conflict with the new name rule; typically you will want to perform any legal EQ elim before a UQ elim.
(2) Be sure not to "cross connectives" in any instantiation or elimination. (x)Fx v (x)Gx cannot be rewritten Fa v Ga, and Gc v Hd cannot be rewritten as (x)Gx v (y)Hy.
(3) Make sure that the name for any UQ int is "free," meaning that it would have been just as true a statement if another name had been present.