# Syntactically speaking, when can you introduce a universal such that no logical inconsistencies are introduced?

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?

-
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

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

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