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

Question

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.

Answer 1

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.

Answer 2

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