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
- $a$ does not occur in an indischarged assumption
- $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.