In our course of logic we've been given th following rules of inferences for introducing and eliminating quantifiers:
$$ \frac{\Gamma \vdash \phi} {\Gamma \vdash \forall x\phi} \; x\not\in FV(\Gamma) \qquad\qquad \frac{\Gamma \vdash \forall x \phi} {\Gamma \vdash \phi \lbrace t/x \rbrace}$$
$$ \frac{\Gamma \vdash \phi \lbrace t/x \rbrace} {\Gamma \vdash \exists x \phi} \qquad\qquad \frac{\Gamma \vdash \exists x \phi \quad \Gamma, \phi \vdash \psi} {\Gamma \vdash \psi} \; x \not\in FV(\Gamma,\psi)$$
Here $\phi \lbrace t/x \rbrace$ denotes the substitution of $x$ by $t$ in $\phi$ and $FV(\Gamma)$ is the collection of free variables in $\Gamma$
Now, according to theese rules I can't infere $\phi \vdash \forall x \phi$ directly from $\phi \vdash \phi$ if $x$ is free in $\phi$ but it seems to me that I should be able to do that inference so I thought that maybe I'm missing something about substitution. I think if I had an inference rule like this one:
$$ \frac{\Gamma \vdash \phi} {\Gamma \vdash \phi \lbrace y/x \rbrace} \;y\text{ is a variable that does not occur in }\Gamma,\phi $$
my problem would be solved, but that rule was not given to me and it is not explicit said, in the recursive definition of substitution, that I can do that, althought it seems coherent to me. So I don't really understand when I am allowed to do a substitution, can I simply decide to change a variable for a new one in a formula and assume it is still the same formula, or does that substitution require some special inference steps?
Thanks
You shouldn't be able to infer $\phi\vdash\forall x\phi$ when $x$ is free in $\phi$.
If you could do that, you could let $\phi$ be $x=0$, and infer $$ x=0 \vdash \forall x(x=0) $$ and then immediately generalize with $t\equiv 1$ to $$ x=0 \vdash 1=0 $$ and then for good measure derive $$ \vdash x=0 \to 1=0 $$ and generalize to $$ \vdash \forall x\bigl[x=0 \to 1=0\bigr] $$ But this sentence is very much not logically valid -- it is certainly not the case that just because you can find some $x$ that equals $0$, you can conclude $1=0$.