Restrictions on the use of universal generalization I am currently reading a book on natural deduction, and it states that for universal generalization or $\forall$-introduction, defined as:
$$\frac {\phi[t/x]} {\forall x \phi}$$
The following restrictions apply:


*

*The term $t$ cannot occur in any undischarged assumption of the derivation of $\phi[t/x]$

*The term $t$ cannot occur in $\phi$


The first of these restrictions is easy to understand, but for the second I just can't quite understand why it is needed?  In the process of going from the top formula to the bottom, you replace all instances of t with x, so therefore $\phi$ should have no $t$'s in it.  Therefore, what's the use of a restriction on a situation that can never occur?  Can someone give me a (realistic) example of where this restriction may be needed?
 A: Consider:
$$\begin{array} {r|ll}
%
(1) & Pt \iff Pt & \text{Provable} \\
%
(2) & \forall x ~ Px \iff Pt & \forall \text{ Intro of (1)} \\
%
(3) & \forall y \forall x ~ Px \iff Py & \forall \text{ Intro of (2)} \\
%
\end{array}$$
This is clearly an unsound derivation, and the $\forall \text{ intro}$ into step (2) violates restriction 2.  Your book is writing UI is a strange way, normally you'd write:
$$\frac{\phi}{\forall x~\phi[x/t]}$$
with only restriction 1.  Restriction 2 is trying to get across "you can't replace only some of the (free) $t$, you have to replace all of them".  Informally UI tries to capture the concept "if a variable (in this case $t$) has no assumptions made about it, then it could be anything".  But there is always the implicit assumption that a variable is itself, which is broken if you only replace some of them.
A: For the restriction 1., consider as $\phi$ the formula : $(x=0)$ :
1) $t=0$ --- assumption : is $\phi[t/x]$
2) $\forall x \ (x =0)$ --- from 1) by $\forall$I : wrong : $t$ is free in the one-line derivation of $\phi[t/x]$ , i.e. in $t=0$
3) $t=0 \to \forall x \ (x =0)$ --- from 1) and 2) by $\to$I
4) $\forall x \ [x=0 \to \forall x \ (x =0)]$ --- from 3) by $\forall$I : now there is no undischarged assumption; thus the rule is correctly applied

5) $0=0 \to \forall x \ (x =0)$ --- from 4) by $\forall$E.


The same apply for 2.
If we have a derivation $\mathcal D$ ending with e.g. $\phi(t)$, now this formula is not an assumption, but a similar counter-example shows that the proviso $t$ not occurring in $\phi$ is needed.
A quite "unnatural" example can be : $\phi$ is $(x \ne 0) \lor (x \ne 1)$.
In first-order arithmetic, we can prove, by $\lor$-intro : $(0 \ne 0) \lor (0 \ne 1)$.
Thus the following derivation as no undischarged assumptions.
1) $(0 \ne 0) \lor (0 \ne 1)$ --- considering the constant $0$ as $t$
2) $\forall x \ [(x \ne x) \lor (x \ne 1)]$
that is false.

The restrictions "formalize" the simple fact that the constant or variable $t$ must be "new".
See :


*

*Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 178.

A: If the variable $t$ is allowed to occur in $\phi$, you allow $\phi\equiv \forall x\exists t(x\ne t)$. Now what is $\phi[t/x]$?
