The problem of Free Variables in natural deduction rules ($\forall$, $\exists$, =). 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


*

*Is my deduction valid as it is?

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

*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 [...])
 A: 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}$
A: *

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


*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).


*The $=$ rule you show does not need any side conditions.
A: 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.

*

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


*∀x((x=b & Pb)⊃Pb)⊃(∃x(x=b & Pb)⊃Pb)       (∃ Elim)


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


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