The problem of Free Variables in natural deduction rules ($\forall$, $\exists$, =).

Question

I am in need of some clarification relating to the rules mentioned. I am doing two different courses on Logic (Philosophy / Computer Science departments) and unforunately they use slightly different vocab for different words.

I was working on the proof for $\exists x\,(x=b\;\land\; P(x))\vdash P(b)$, where $b$ is understood to be some term and $x$ is some "variable". I first wrote the following proof

$\begin{array}{ccc} 1 & &\exists x\,(x=b\;\land\; P(x)) &\text{Premise}\\ 2 &|& b=b\land P(b) &\text{Assumption}\\ 3 &|& P(b) &\land\text{-elimination (2)}\\ 4&&P(b) &\exists\text{-elimination (2-3)} \end{array}$

I understand the $\exists$-elimination rule comes with the side condition that the variable you "assume" exists must be free - but I'm not sure the precise condition. The definitions for this course are:

A variable $x$ is free in $\phi$ if it is not within the scope of a quantifier.

A term $t$ is free for $x$ in $\phi$ if nowhere in $\phi$ does an $x$ variable occur within the scope of any variable that occurs in $t$.

$$ \frac{\begin{array}{ccc} &&\phi[x_0/x]\\ &&\vdots\\ \exists x\phi&&\psi \end{array}}{\psi}\exists\text{-elim} $$ I thought the condition was that we needed $b$ to be free for $x$ in $\phi$, but this seems too easy? The philosophy department only put requirements on $x$ not being a free variable in $\psi$ and the assumptions needed "along the way" in the $\vdots$-bit, and even says that $x$ can be a free variable in $\phi$, totally contradictory to the computer science department...!

---

My questions are

1. Is my deduction valid as it is?

2. What are the precise side conditions of the $\exists$-elim and $\forall$-intro rules, using the definitions I mention?

3. Are there any side conditions on the $=$ rules? My lecture notes don't mention any but I thought they did? Specifically this one:

   $$\frac{t_1=t_2\quad \phi[t_1/x]}{\phi[t_2/x]}=\text{-elim}$$ for $t_1,t_2$ terms, $x$ a variable.

Thanks!

(edit, I meant to say: the Term* you "assume" exists [...])

Answer 1

Comments

Term is a more general syntactical object than variable : a term is a variable or a constant or a "complex" term built-up from "simpler" terms with a function symbol, like $x+1$ in arithmetic, where $x$ is a variable, $1$ is a constant and $+$ is a (binary) fucntion symbol.

---

Free and free for are two different concepts :

• an occurrence of a variable is free in a formula if it is not in the scope of a quantifier : in the formula $\exists y(y=x+1)$ we have that the occurrence of $y$ into $(y=x+1)$ is bounded by the leading quantifier $\exists y$ while the occurrence of $x$ is free;

• a variable $z$ (or a term $t$) is free for $x$ in $\phi$ if there are free occurrences of $x$ in $\phi$ and if the replacement of all occurrences of $x$ in $\phi$ with $z$ (or with $t$) will cause no "capturing" of $z$ (or of variables occurring in $t$) by some quantifier already present into $\phi$. I.e. if we consider again the formula $\exists y(y=x+1)$, we have that $z$ is free for $x$ in it, because the result of the replacement is $\exists y(y=z+1)$ and we have no "capturing", but the $y$ is not for $x$ in it, because the result will be : $\exists y(y=y+1)$ that does not have the same "meaning".

---

In the $\exists$-elimination rule :

$$ \frac{\begin{array}{ccc} &&\phi[x_0/x]\\ &&\vdots\\ \exists x\phi&&\psi \end{array}}{\psi}\exists\text{-elim} $$

the proviso is :

$x_0$ does not occur in $\psi$, $\phi$ or any undischarged assumption of the subderivation of $\psi$, except $\phi[x_0/x]$.

Of course, if you use a constant $c$ in place of $x_0$, the proviso is the same.

---

In the $\forall$-introduction rule :

$$ \frac{\phi(x)}{\forall x\phi(x)}\forall\text{-intro} $$

the proviso is :

the variable $x$ may not occur free in any hypothesis on which $\phi(x)$ depends.

---

Here is an example showing the need for the proviso :

1) $x=0$ --- assumed

2) $\forall x(x=0)$ --- $\forall$-intro : illegal !

3) $x=0 \to \forall x(x=0)$ --- $\to$-intro, discharging 1)

4) $\forall x[x=0 \to \forall x(x=0)]$ --- $\forall$-intro : correct ! there are no assumptions left

5) $0=0 \to \forall x(x=0)$ --- $\forall$-elim.

The conclusion is clearly false in $\mathbb N$.

---

Here is an example showing the need for the proviso in the $\exists$-elim rule :

1) $\exists x(x=0)$ --- assumed

2) $(x=0)$ --- assumed for $\exists$-elim

3) $x=0$ --- from 2) and 1) by $\exists$-elim, discharging 2) : illegal ! $x=0$ is "the $\psi$" and we have the variable $x$ used in the $\exists$-elim application free in it

4) $\forall x(x=0)$ --- $\forall$-intro : correct ; there are no free occurrence of $x$ in the only assumption left, i.e. into 1)

5) $\exists x(x=0) \to \forall x(x=0)$ --- $\to$-intro.

The conclusion is clearly false in $\mathbb N$.

---

---

Regarding your proof, it can be easily "restored" :

$\begin{array}{ccc} 1 & &\exists x\,(x=b\;\land\; P(x)) &\text{Premise}\\ 2 &|& y=b\land P(y) &\text{Assumption for } \exists\text{-elimination : y new}\\ 3 &|& P(y) &\land\text{-elimination (2)}\\ 4 &|& y=b &\land\text{-elimination (2)}\\ 5&&P(b) &=\text{-elimination (3-4)}\\ 6&&P(b) &\exists\text{-elimination (2-5) : y not occurring in it} \end{array}$

Answer 2

1. No, that is not valid. In the $\exists$-elimination rule, $x_0$ cannot be an arbitrary term, but must be a new variable that is not free in $\psi$. That means you cannot use $b$ as $x_0$ -- first, $b$ might not even be a variable (it could be a constant symbol or even a term containing function symbol); second, even if $b$ is a variable it is not free in $\psi$ which is $P(b)$ in your attempted application.

2. You need side conditions that prevent $x_0$ from occurring free in either $\phi$ or $\psi$. If you allow $\phi$ to contain $x_0$ you can derive nonsense by first proving (from whatever set of axioms you're using) that $\exists x.x\ne x_0$, then use $\exists$-elimination to assume $x_0\ne x_0$, derive a contradiction and hence any nonsense you want as $\psi$.

   On the other hand it is right that $x$ (but not $x_0$) can be free in $\phi$ (if it didn't the rule would not be much fun at all).

3. The $=$ rule you show does not need any side conditions.

Answer 3

The key here is to derive a universal that implies the desired result. I’ll prove it as an implication since it’s a bit cleaner. Note I’m using a Hilbert-style system, so instead of using the Existential Elim rule, I’m using the axiomatic version.

1. (x=b & Pb)⊃Pb (& Elim. Right)

2. ∀x((x=b & Pb)⊃Pb)⊃(∃x(x=b & Pb)⊃Pb) (∃ Elim)

3. ∀x((x=b & Pb)⊃Pb) (1, Gen.)

4. ∃x(x=b & Pb)⊃Pb (2,3 MP)