Say we have a first order logic formula like this one:
$$ \forall x \forall y \forall z ( (R(x,y) \land R(y,z) \implies R(x,z)) \land \forall x (\lnot R(x,x) \land R(x,f(x))) $$
Is the variable $x$ in this case be double bound ? This concept doesnt make sense to me, because to me it seems that the $x$ in the $\forall x(R(x,z))$ is not the same than the "global" $x$.
Which means that I could substitute it with a better name.
Is my idea correct ?
On
A quantifier has two parts: the first introduces a new variable and the second is a single statement that operates in (the computer science / programming language equivalent of) a new scope, in which otherwise free variables of that name are bound to the one introduce by the quantifier. Within the new scope the introduced identifier is redefined, hiding any variables with the same name from outside the scope.
Since the quantifier construct only binds otherwise free variables for the statement in its scope, the construct allows for nesting and redefining the same variable name.
Sometimes, especially when using mechanical transformations that treat formulas like data, we have to rename variables that have the same name. See this question about the backward chaining algorithm, which treats formulas as data to be manipulated. A backward chaining algorithm might use CNF, which is a flattened form of logical statements.
By flattened, I mean that quantifiers are removed. That means that the separate scopes they introduce have to be removed, and, since after flattening scopes, all variables have to exist in the same scope, sometimes some of the variables will need to be renamed so they don't conflict/overlap with each other.
A quantifier only binds free occurrences of the quantified variable in its scope. So yes, you can replace the nested $x$ with a different variable, for example, your formula is equivalent to the following:
$$\forall x \forall y \forall z ( (R(x,y) \land R(y,z) \implies R(x,z)) \land \forall t (\lnot R(t,t) \land R(t,f(t)))$$