Natural Deduction: Universal Introduction rule concerning free variables in Van Dalen's "Logic and Structure" The $\forall I$ rule (forall introduction) in Dirk van Dalen's Logic and Structure (4th ed) is:
$${\forall I}\, \frac{\varphi}{\forall x\, \varphi} $$
where the intended restriction is: the variable $x$ may not occur free in any hypothesis on which
$\varphi$ depends, i.e. an uncancelled hypothesis in the derivation of $\varphi$.
I have two question concerning this:


*

*¿ Can we derive $P(x) \vdash \forall x\, P(x)$ ?
If i write the following derivation:
$${\forall I}\, \frac{P(x)}{\forall x\, P(x)} $$
then im not sure if the restriction is fulfilled. Considering that $P(x)$ by 
itself does not depend on any hypothesis (and it is a premise), im tempted 
to say yes...
But, from the defined semantics of the same author (which admits free variables, see Definition 2.8.1 (ii)), we have:
$$P(x) \not\vDash \forall x\, P(x)$$ 
In the same book soundness & completeness is proved, in the general form:
$$\Gamma \vdash \varphi \ \ \text{ iff } \ \ \Gamma \vDash\varphi $$ 
So i think my first derivation can't be right.
A related topic of discussion could be what is the meaning of free variables on premises?. At least from the semantical point of view, i think of free variables as arbitrary individuals (some authors like Enderton define a kind of "context" formalized as a valuation function). Anyway, i don't see Van Dalen rejecting the occurrence of free variables in premises of natural deduction (as others do).

*Lets compare Van Dalen's $\forall I$ rule with the following more (i 
think...) frecuently seen variant:
$${\forall I}\, \frac{\varphi[t/x]}{\forall x\, \varphi(x)} $$
where $t$ is allowed to be a variable (or even a constant?) with no free occurrence 
in $\varphi$ 
or any hypothesis on which $\varphi$ depends (again, this really means 
uncancelled hypothesis in the derivation of $\varphi$), AND provided 
that $t$ is substitutable for $x$ in $\varphi$.
I can see this variant have two restrictions, not only one as in Van Dalen's version. But this rule not forces you to use the same variable as the bounded/quantified and also as the arbitrary individual (sometimes called "parameter") in the derivation. I say this because is common reasoning practice that to prove $\varphi$ is true for every element $x$, we write: Let $c$ be an element...
Also, this rule subsumes Van Dalen's if im not mistaken, just take $t=x$ and
then we have $[x/x]=x$.
An similar situation occurs for the $\exists E$ rule, we could introduce another variable (or constant) as an unknown individual. But also for this rule in the mentioned book we cant.
So the second question is, what is the rationale to reuse the same var in the $\forall I$ rule as given in Van Dalen's book?. I don't really care conventions, im more interested in what is more general in some way.
 A: *

*No, because $x$ is free in assumption $P(x)$ and we have that it depends on itself.

See counter-example page 87 : without proviso, we can derive the invalid : $x=0 \to \forall x (x=0)$.
We can check it with the formal definition of derivation [page 33] : a derivation is a tree where the root is the conclusion and the Leaves are the assumptions :

Definition 2.4.1 The set of derivations is the smallest set $X$ such that

(1) The one-element tree $\varphi$ belongs to $X$ for all $\varphi \in \text {PROP}$. [...]


Thus, a single node tree is a derivation where the formula is both the conclusion and the (undischarged) assumption of the derivation.
Compare with : Sara Negri & Jan von Plato, Structural Proof Theory (Cambridge UP, 2001), page 64 :

Usually rule $\forall \text I$ is written as $\frac{A}{\forall x A}$ and the restriction is that $x$ is not free in any of the assumptions that $A$ depends on, where one must keep in mind that if $A$ is an assumption it depends on itself.


About free variables :

what is the meaning of free variables on premises? At least from the semantical point of view, i think of free variables as arbitrary individuals (some authors like Enderton define a kind of "context" formalized as a valuation function).

A free variable acts as a pronoun in natural Language; compare "$x$ is red" with "it is red". Its meaning (and truth value) depends on the context where we assert it.
(One of) The way to formalize a "semantical context" is through a variable assignment function.



*In the alternative formulation, we have the same proviso :


$t$ does not have free occurrences in $\varphi$ or any hypothesis on which $\varphi$ depends.

$t$ is a term and thus, as you say, it may be also a variable. But, being not free in $\varphi$, it cannot be $x$ itself, if $x$ occur free in $\varphi$.
