In textbook First-Order Mathematical Logic, author Angelo Margaris stated:
The rule of generalization is
$$\large\dfrac{P}{\forall vP}\space\space\space\space \text{ provided $v$ is not restricted}$$
The only interesting applications of this rule occur when $v$ is free in $P$. The idea is that if $P$ is true for $v$, and $v$ is not restricted (i.e., stands for an arbitrary element of the domain), then $P$ is true for every element of the domain.
The rule of existential elimination is
$$\large\dfrac{\exists vP}{P(u|v)}\space\space\space\space \text{ where $u$ is a variable that is not restricted}$$
The idea is that if $P$ is true for some $v$, then we can choose some object $u$ for which $P$ is true.
My questions:
I would like to confirm that $$P \iff \forall vP \space\space\space\space \text{ provided $v$ is not restricted}$$ or it's just $$P \implies \forall vP \space\space\space\space \text{ provided $v$ is not restricted}$$
Similarly, it's $$\exists vP \iff P(u|v)\space\space\space\space \text{ where $u$ is a variable that is not restricted}$$ or it's just $$\exists vP \implies P(u|v)\space\space\space\space \text{ where $u$ is a variable that is not restricted}$$
I'm not sure what does it mean when the author said $v$ is not restricted (i.e., stands for an arbitrary element of the domain). Does it mean that $v$ has not appeared anywhere in $P$, or that $v$ is free in $P$ (I infer this from The only interesting applications of this rule occur when $v$ is free in $P$)?
Since I've just got into first-order logic from this textbook a couple of hours ago (to solve my previous question here), my questions seem quite silly. I'm sorry for that!
Thank you for your help!
When you write $P\iff \forall x P$ you are writing a sentence. The generalization rule is not a sentence, it is an inference rule, which says if you have derived $P,$ you can infer $\forall x P.$ This is similar in character to an implication, but it's important to maintain the distinction between things said in the formal language and things said outside it.
But if you're asking if you can generally infer $P$ from $\forall x P,$ yes, this is an admissible rule in first order logic (called universal instantiation). In fact you can generally infer $P$ with any term substituted for all free occurrences of $x.$ Whether this is a primitive inference rule, handled as an axiom, or otherwise varies from treatment to treatment.
As for the part about restriction, the intuitive idea of generalization assumes that $x$ is an arbitrary element of the domain, in other words not one that we've made any special assumptions about. Only then can we say "since it holds for (an arbitrary) $x,$ it holds for all $x.$"
Usually, in practice, we are proving something in a particular context, in other words we have made some set of assumptions. Oftentimes the assumptions are represented as a set of formulae $\Gamma$ that we are assume, and we express derivability from the assumptions $\Gamma$ as $\Gamma \vdash P.$ What $x$ being "unrestricted" means here is that the variable $x$ does not appear free in any of the formulae the context $\Gamma$. Informally speaking, we haven't made any assumptions about it. If this condition holds then we can infer $\Gamma \vdash \forall x P$ from $\Gamma \vdash P.$
I'm not sure how things are handled precisely in your book, but as the author says, you can read ahead to chapter two to see the precise way the restriction is defined