2
$\begingroup$

In first order logic we have the following inference rule :

(∀I)
 Γ ⇒ F(v)
 Γ ⇒ ∀vF(v)

where v is not a free variable of any formula in Γ. I understand that there is a condition F(v) and variable v satisfies this condition. However how come all the v's can satisfy this condition ? What is the logic behind this inference ?

$\endgroup$
1
  • $\begingroup$ If the "name" $v$ is "generic" (i.e. nothing is known or suppoesd about it : this is the reason for the proviso : $v$ not free in $\Gamma$) then if $F$ holds of it, then $F$ holds for all. $\endgroup$ – Mauro ALLEGRANZA Dec 28 '16 at 13:23
0
$\begingroup$

Maybe it will be helpful if you think about it from a semantic point of view. Suppse that if $\Gamma\models\varphi$, and a model ($\mathcal{M},v)\models\Gamma$. Then we have $(\mathcal{M},v)\models\varphi$. Our goal is to show $(\mathcal{M},v)\models\forall_x\varphi$. We also know that $\varphi$ is a axiom, or an elemnent of $\Gamma$, or got from $MP$ from a syntactic point of view.

Suppose is $\varphi$ is an axiom, of course, $(\mathcal{M},v)\models\forall_x\varphi$.

Suppose is $\varphi$ an elemnent of $\Gamma$, or got from MP, then we also have $\mathcal({M},v)\models\forall_x\varphi$. Because we can prove that: if x is not a free variable of $\varphi$, $(\mathcal{M},v)\models\varphi\leftrightarrow(\mathcal{M},v)\models\forall_x\varphi$ by induction on the compexity of $\varphi$.

$\endgroup$

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.