What is the so-called eigenvariable or parameter in natural deduction?

Solution 1:

The eigenvariable condition is used when want to introduce the forall connector.

If you want to introduce forall a, then you need to make sure that a is not free in the assumptions. Therefore you can be forced to rename a free a the assumption with new name.

In http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.94.9463&rep=rep1&type=pdf by Alwen Tiu you can read :

In proof search for a universal quantified formula, e.g., ∀x.Bx, the quantified variable x is replaced by a new constant c, and proof search is continued on Bc. Such constants are called eigenvariables, and in traditional intuitionistic or classical logic, they play the role of scoped constants as they are created dynamically as proof search progresses and are not instantiated during the proof search.

See page 2 for more details

Solution 2:

The usual formalisation of first-order logic needs to distinguish between letters that stand for things that can be substituted by any term and letters that are taken to be particular terms. The eigenvariables are the latter sort of letter, which cannot be substituted for in the forall-intro / exists-elim rules.

This is a very tricky concept when learning predicate logic and the move to natural deduction has the capacity to confuse things still further. To get a handle on the inference rules, most people find they need to be somewhat formalist about the distinction, viewing the distinction as a syntactic marker saying which are the leaves of a formula that can be substituted into. But at this formalist level, you do not really grasp the why of it.

The key is that the two kinds of letter can be seen to be variables that derive their meaning in the judgement expressed at that point in the derivation. The semantics of the variables has their being bound, with regular variables being universally quantified and eigenvariables being existentially quantified. The constants then are equivalent to the Skolem constants that arise from the Skolemisation of the formula expressing the judgement.

The above is tricky, and properly grasping it requires that you (i) are comfortable with the application of Skolemisation (see Wikipedia on Skolem normal forms for a decent discussion), and (ii) figure out how to apply it to express the judgement at each formula in a natural deduction proof. But then, this is no more than the complexity of variables and constants in first-order logic.

It would be nice to recommend a text that covers this ground, but none come to mind.

Solution 3:

The eigenvariable conditions preserve the scope of the variables, i.e., no binding of a variable is added or removed in the substitution process.
This is usually ensured by the condition that the variable doesn't occur in the set of hypotheses.
Creating new/fresh variables (which do not occur in the set of hypotheses) is one technique for satisfying this restriction:

where y is a variable not previously used in the proof

(p. 25 of http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf)

See also the eigenvariable conditions:

*Eigenvariable conditions:
∀I: provided x not free in the assumptions
∃E: provided x not free in B or in any assumption save A

(p. 19)

The general concept is valid in all mathematical logics, not only in natural deduction. See, for example, the higher-order logic Q₀, which is a Hilbert-style system based on type theory using lambda calculus (lambda notation).
For the introduction of the universal quantifier, cf. the Rule of Universal Generalization (Gen) (Theorem 5220 in [Andrews, 2002, p. 222]).
For the elimination of the existential quantifier, cf. Rule C (Theorem 5245 in [Andrews, 2002, p. 230]).
The restrictions in these rules have their origin in the substitution procedure of Rule R', which is valid only provided that it is not the case that "x is free in a member of [the set of hypotheses] H and free in [A = B]." [Andrews, 2002, p. 214].

This restriction on Rule R' is also implemented in the logic R₀, cf. pp. 386, 487 of http://www.owlofminerva.net/files/formulae.pdf.
The corresponding (derived) rules for ∀I and ∃E are A5220H (Gen) (pp. 76 ff.) and A5245 (Rule C) (pp. 122 ff.).

For the references, please see: http://doi.org/10.4444/100.111