# What is a relatively bound variable?

edit: Interestingly, the authors also state at one point that the choice of introduction rule is determined by the structure of the previous goal and the list of introduction rules; but at another point, that the choice of introduction rule is determined by the structure of the current goal and the list of introduction rules. I believe the latter is correct, but I'll have to be more careful implementing the paper's algorithm than I previously thought.

In any case, I believe the "no variable can relatively bind itself" restriction intends to preclude abstraction on a variable using that variable, but I could be wrong. If anything rests on whether or not this is correct, I'll attempt to contact the authors.

original: In a paper on natural deduction proof search, the authors write that the free variables $\gamma_1,\ldots,\gamma_n$ occurring in the formulae $\forall \alpha.\phi(\alpha,\gamma_1,\ldots,\gamma_n)$ and $\exists \alpha . \phi(\alpha,\gamma_1,\ldots,\gamma_n)$ in the conclusions of the quantifier introduction rules $$\frac{\phi(\alpha/\beta,\gamma_1,\ldots,\gamma_n)}{\forall \alpha . \phi(\alpha,\gamma_1,\ldots,\gamma_n)} \quad (\forall\text{-in})$$ and $$\frac{\phi(\alpha/t)}{\exists \alpha . \phi (\alpha,\gamma_1,\ldots,\gamma_n)}\quad(\exists\text{-in})$$ are relatively flagged or bound. Presumably, then, a variable is relatively bound if and only if it occurs free in the conclusion of a quantifier introduction rule. However, in defining a natural deduction derivation and presenting algorithms, they remark that no variable may relatively bind itself. For instance, they require that unification not produce substitutions causing variables to relatively bind themselves.

I searched through several logic books I had lying around, especially ones focusing on automated reasoning, but couldn't find a definition of relatively bound variables. Has anyone encountered this term before? If so, what does it mean?

-
I apologize if this seems too obvious of a thing to do, but... since they provided it, have you e-mailed any of the authors with this question? –  Doug Spoonwood Oct 17 '11 at 1:43
If anything ends up resting on the definition of the term, I'll contact the authors. I assume, however, that spending more time with the paper should allow me to deduce its meaning. Thanks for the suggestion, however. –  danportin Oct 18 '11 at 3:17