Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
    
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

1 Answer 1

up vote 0 down vote accepted

The paper actually says "relatively bounded", not "bound", but since it also says "relatively binds itself", not "relatively bounds itself", this seems to be a mistake. A definition of these terms is found in Section 3.3 of this paper, which is by mostly the same authors and contains the same apparent mistake.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.