Restrictions on the use of universal generalization

Question

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:

1. The term $t$ cannot occur in any undischarged assumption of the derivation of $\phi[t/x]$
2. 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?

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

Answer 2

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.

Answer 3

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]$?