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?
Solution 1:
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.