I propose the following restriction on universal instantiation: UI may not be used to introduce new variables. The variable specified should be an "old" variable, i.e. it must already have been introduced by either an active premise or by existential instantiation (E-elimination). (An active premise is one that has not been closed-off or discharged by what I call a conclusion statement.)
The primary benefit of this restriction is to eliminate the need to consider dependencies among variables that are created with existential instantiation. Such considerations never seem to come up in "real mathematics." The restriction I propose seems to be implicit even in the most rigorous mathematical proofs, if not in standard formal logic.
With this restriction in place, dependencies among variables need not be considered because the only variables on which you could then make universal generalizations are those introduced in a premise that has subsequently been closed-off or discharged by what I call a conclusion statement. The conclusion statement and subsequent statements that are derived from it and also refer to these variables can always be universally generalized regardless of the presence of any other variables that were introduced by E-elimination.
I have implemented this restriction in my proof checker/editor (available free at http://www.dcproof.com). Play around with it. Try to "break it" if you can. Work through the brief tutorial to learn the system.
Another benefit, from a pedagogical perspective, has been the elimination from my program of several what must have been confusing warning messages about dependencies among variables. It also simplifies the requirements for universal generalizations (A-introduction).
Following is a summary of the rules of inference I use in my system that are relevant to the handling of free variables:
Free variables may be introduced only by means of a premise (assumption) or by existential specification (E-elimination).
Existential specification (E-elimination) allows an unused free variable to be specified for any active, existentially quantified statement.
Universal specification (A-elimination) allows any free variable introduced by an active premise or any algebraic expression in such free variables to be specified for any active, universally quantified statement.
Existential generalization (E-introduction) may be applied to any free variable or any algebraic expression in one or more free-variables that is found in any active statement.
Universal generalizations (A-introduction) may be applied to any free variable that (a) is found in an active statement, and (b) is not referred to by any active premise, and (c) was not introduced by existential specification (E-elimination). (There are no considerations given for any dependencies among variables.)
Free variables introduced after a premise statement and before the corresponding conclusion statement may not appear in that conclusion statement.
In my program, I use color-coding for free variables. Green indicates that a Universal Generalization is possible. Red indicates that a Universal Generalization is not possible. When first introduced, all free variables are red. A free variable that was introduced by a premise is changed to green when that premise is closed-off (or discharged) by a conclusion statement. It is effectively reintroduced, changing back to red if it is referred to in subsequent premise.
Your comments would be appreciated.