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

-

## migrated from cstheory.stackexchange.comMay 24 '11 at 2:42

This question came from our site for theoretical computer scientists and researchers in related fields.

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

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 May 25 '11 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. – Charles Stewart May 25 '11 at 8:27

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.