3
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Now I'm even more confussed, I had in my head the idea (not sure where this idea came from) that a formula with free variables was equivalent to the result of generalizing over those variables, how do I realize if a formula like $\phi(x)$ (where x is free) refers to any $x$ of to a specific one? BTW thanks for the edit. $\endgroup$ – la flaca Jun 3 '16 at 15:41
  • 1
    $\begingroup$ @Eliana: In a Hilbert-like system (where you never have anything to the left of the $\vdash$) this is generally true. With natural deduction the best you can generally say is something like $\Gamma\vdash \phi$ when there are free variables is "morally" equivalent to $\forall x[\Gamma\vdash\phi]$ -- except that writing this is not even syntactically allowed! You can also, and correctly, say that $\vdash \phi$ (with an empty $\Gamma$) is equivalent to $\vdash \forall x\phi$. (...) $\endgroup$ – Henning Makholm Jun 3 '16 at 15:48
  • 1
    $\begingroup$ (...) But when a variable appears free on both sides of the $\vdash$, those instances are supposed to refer to the same thing, and you can't generalize some of them independently of the rest. This is why the generalization rule needs the side condition that $x$ cannot appear free in $\Gamma$. Does this help clear it up somewhat? $\endgroup$ – Henning Makholm Jun 3 '16 at 15:49
  • $\begingroup$ Yes Henning, that makes sense but I still need to think more about it, thanks for your help. $\endgroup$ – la flaca Jun 3 '16 at 15:56
  • $\begingroup$ I still have problems with the substitution part, I feel I should be allowed to infer $\Gamma \vdash \phi \lbrace y/x \rbrace$ from $\Gamma \vdash \phi$ if $y$ does not occur in $\Gamma, \phi$ but how do I justify this inference? $\endgroup$ – la flaca Jun 3 '16 at 16:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.