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

I am reading the Wikipedia article on Natural Deduction. In section 6, the presentation of intr and elim rules for the universal and existential quantifiers, it mentions a concept called eigenvariable/parameter without further discussion. What is it? What's the difference between the eigenvariable/parameter $a$ and the bound variable $x$ introduced by $\forall$ or $\exists$? What's it used for? The side conditions for the $\forall$ intr and $\exists$ elim rules also puzzled me. Could anyone explain a little bit more? Thanks.

• This is covered in standard undergrad logic textbooks and is off-topic for cstheory. Please read the FAQ if you haven't. Commented May 24, 2011 at 2:41

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 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

• Does this concept exist with another name in lambda calculus/type theory? Commented Aug 3, 2013 at 16:16

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.

• Thanks, Charles. Concerning your third paragraph, my question is it seems to me that in the intr or elim rule for a single universally quantified formula, these two kinds of variables don't occur at the same time, above the intr node no universally quantified variable but only what you called existentially quantified one, below vice versa. How do you explain this? Another question, your first sentence mentioned "the usual formalization", I suppose there are unusual ones? Could you point to me one? Thanks.
– day
Commented May 25, 2011 at 8:08
• @plmday - at the same time: You need the whole proof above the rule to determine this; subderivations will constrain how the various letters are related to each other. unusual ones: There are variable-free axiomatisations of predicate logic, such as combinatory logic. Commented May 25, 2011 at 8:27

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

*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 Q0, 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 R0, 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