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.

As far as I know, there are only 2 restrictions for the universal introduction rule of inference which are the following:

P[a/x] can become forall x.P if:
1. x is not mentioned in P
2. a is not mentioned in a premise

But these don't prevent the problem mentioned here:
Does existential elimination affect whether you can do a universal introduction?

So is the list of restrictions incomplete or is there something I'm missing here?

share|improve this question
    
Never mind, I realized that I'm mixing different versions of the rules of inference. The need for extra restrictions only arises when using the rules of inference in the linked post and not the ones I mentioned here. –  mtanti Jun 7 '11 at 21:36

1 Answer 1

From post above:

As far as I know, there are only 2 restrictions for the universal introduction rule of inference which are the following:

P[a/x] can become forall x.P if:
1. x is not mentioned in P
2. a is not mentioned in a premise

from linked post:

1   ∀y:(∃x:(R(x,y)))    Premise
2   ∃x:(R(x,q))         ∀Elim, line 1
3   R(p,q)              ∃Elim, line 2
4   ∀y:(R(p,y))         ∀Intro, line 3

My understanding of the rule of Universal Introduction is as follows:

Universal Introduction ($\forall I$)
$\:\;|\;\;P(a/x)$
$\;\;|$
$\;\therefore\;\;(\forall x) P$

provided that

  1. $a$ does not occur in an indischarged assumption
  2. $a$ does not occur in $(\forall x) P$.

In the example given above, we see that in generalizing from $R(p, q)$ to $(\forall y: (R(p, y))$, $p$ occurs in the universal quantified conclusion, violating the second condition above.

So I'm wondering if the first condition in your list should state what the second condition states in the definition here (replacing your $x$ with "$a$")?


As for being careful with $\forall I$, the following characterization of generalizing from an arbitrary member of a domain:

If we choose an arbitrary member of the domain, and show that the sentence holds for it, that is sufficient (for $\forall I$). But, what do we mean by arbitrary?

In short, it means that we have no control over what element is picked, or equivalently, that the proof must hold regardless of what element is picked. More precisely, a variable is arbitrary unless:

  • A variable is not arbitrary if it is free in (an enclosing) premise.
  • A variable is not arbitrary if it is free after applying Elim — either as the introduced witness, or if it is free anywhere else in the formula.
share|improve this answer
    
Before you invest a lot more effort into this post: did you see the OP's comment to this question and what happened on this MO-thread? –  t.b. Jun 7 '11 at 23:44

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.