Logic – Introduction to Universal Quantifier and Existential Quantifier Elimination

Question

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents.

Definition. If $\phi_1,\dots, \phi_n,\phi$ are formulas, then $\phi_1\dots\phi_n\vdash\phi$, often abbreviated by $\Gamma\vdash\phi$, is called a sequent.

Can somebody please explain to me the following two inference rules?

1. Introduction of the universal quantifier.

$$
\begin{array}{c}
\Gamma\vdash\phi\\
\hline
\Gamma\vdash\forall x(\phi)
\end{array}\text{, where $x$ does not occur as a free variable in $\Gamma$.}
$$

2. Elimination of the existential quantifier.

$$
\begin{array}{c}
\Gamma\vdash\exists x(A)\qquad \Gamma, A\vdash B\\
\hline
\Gamma\vdash B
\end{array}
\text{, where $x$ does neither occur as a free variable in $\Gamma$ nor as a free variable in $B$.}
$$

I am especially interested in what the restriction that $x$ is not allowed to occur as a free variable in $\Gamma$ (and also not in $B$) is all about. I have heard the following explanation for the necessity of this restriction:

Otherwise we could derive $\exists x (A(x))\rightarrow \forall x (A(x))$. But this is not a logically valid formula; and we want to have a correct calculus.

Although I can reconstruct this argument, I do not really understand the two rules given above. I have no intuition why $x$ should not be a free variable in $B$ or in $\Gamma$, for example. Could you please explain the intuition behind these inference rules?

EDIT: Another question, but a related question: Can you give an example of a proof which uses the rule of existential quantifier eliminination where there is some free variable occuring in $B$?

Answer 1

Example

Let $\Gamma$ the set of first-order Peano axioms: no variables free.

1) $\Gamma \vdash \exists x (x = 0)$ --- easily provable

2) $\Gamma, x=0 \vdash x=0$ --- obvious

3) $\Gamma \vdash x=0$ --- from 1) and 2) by $\exists$-elim : wrong !

4) $\Gamma \vdash \forall x (x=0)$ --- from 3) by $\forall$-intro,

---

1) $\Gamma, x=0 \vdash x = 0$

2) $\Gamma, x=0 \vdash \forall x (x=0)$ --- by $\forall$-intro: wrong !

3) $\Gamma \vdash x=0 \to \forall x (x=0)$ --- from 2) by $\to$-intro

4) $\Gamma \vdash \forall x [x=0 \to \forall x (x=0)]$ --- from 3) by $\forall$-intro

5) $\Gamma \vdash 0=0 \to \forall x (x=0)$ --- from 4) by $\forall$-elim.

---

---

The ground for the restriction on $\forall$-intro are linked to the "generalization principle":

what holds for any, holds for all.

Thus, in order to formalize this principle with a rule of inference, we read it as:

if something holds for an "arbitrary object", then it holds for all objects.

We have to capture the informal concept of “arbitrary object” by way of a syntactic criterion.

Consider now a variable $x$ in the context of a derivation: we shall call $x$ arbitrary if nothing has been assumed concerning $x$. In other words, $x$ is arbitrary at its particular occurrence in a derivation if the part of the derivation above it contains no hypotheses containing $x$ free.