Proposed Restriction on Universal Instantiation (Natural Deduction) 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.
 A: You can always add some tautology as an assumption (say $x \rightarrow x$) and then later discharge it, so it seems like your restriction is valid.
Check "Structural Proof Theory", a book by von Plato and Negri, which discusses such issues; it also sponsors a proof editor PESCA by Aarne Ranta.
A: Follow-up
Much to my chagrin at the time (happy ending though!), I discovered that restricting Universal Instantiation alone was not enough to avoid problems with dependent variables. By indirect methods you could still use UI to introduce new free variables as follows:


*

*Ax P(x)         (Premise)

*~P(y)             (Premise)

*P(y)               (UI, 1)

*P(y) & ~P(y) (Join 2,3)

*~~P(y)          (Conclusion, 2)

*P(y)               (Remove ~~)  


I managed to close off this possibility, however, by formalizing what mathematicians habitually seem to do when writing proofs: 
When you want to prove something is true in general, you introduce an assumption with one or more new free variables in it, say P(x). Then you prove, say Q(x). Then, if Q(x) is not a contradiction, you can then generalize Ax (P(x) => Q(x)). In this case, you must ensure that no free variables introduced in the interim occur free in Q(x). If Q(x) is a contradiction, then Ax ~P(x).
By implementing this rule in my program, the conclusion on line 5 becomes:
Ax ~~P(x) (Conclusion, 2)
My new conclusion rule will automatically generalize on variables introduced in the corresponding premise (line 2 in this case). There is now no other way introduce universal quantifiers. It just doesn't seem to be necessary. 
In addition to automatically doing universal generalizations, the new conclusion rule will also automatically do existential generalizations if necessary so that no new free variables show up in the conclusion. See the example at: 
http://www.dcproof.com/EA-AE.html 
This HTML document was generated using my program. Comments are in a blue font.
My DC Proof program may not serve everyone's need, but if students want to write mathematical proofs in, say, number theory, algebra or analysis, it can serve as an excellent introduction to the rules that mathematicians actually use when writing proofs. In my opinion, there is simply no need to burden such students with esoterica about dependent variables that never seem to come up outside of rarefied philosophical discussions.
You can download Version 2.0 of my program at my website http://www.dcproof.com
Dan
