3
$\begingroup$

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?

  • 0
    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.2011-10-18

1 Answers 1

1

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.