Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question

migrated from cstheory.stackexchange.com May 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
add comment

2 Answers 2

up vote 1 down vote accepted

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.

share|improve this answer
    
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
add comment

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

share|improve this answer
    
Does this concept exist with another name in lambda calculus/type theory? –  Blaisorblade Aug 3 '13 at 16:16
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.