Is $f(x _2,x _0)$ free for $x _o $ in $\forall x _0 P(x _0, x _1 ) $?

Question

Is $f(x _2,x _0)$ free for $x _o $ in $\forall x _0 P(x _0, x _1 ) $?

I wonder if I can I substitute a term for a quantified variable. I am rereading the definition for substitution of variables in terms in Dalen's Logic and structure but I can't find if he tells wether we can substitute a term $t $ for $y $ in $\forall y \phi $ (ie change $\forall y \phi $ to $\forall t \phi $. For me this seems like a natural thing to do, but I don't know certainly...

Answer 1

I wonder if I can I substitute a term for a quantified variable.

No, you cannot.

The substitution operation is defined in Definition 3.3.10, page 61 :

$ϕ[t/x]$ is defined by: […] $(∀yϕ)[t/x] := ∀yϕ[t/x]$ if $x \neq y$, and $∀yϕ$ if $x = y$.

See Definition 3.3.12 : $t$ is free for $x$ in $ϕ$ if […] (iii) $ϕ := ∃yψ$ (or $ϕ := ∀yψ$) and if $x ∈ FV(ϕ)$, then $y \notin FV(t)$ and $t$ is free for $x$ in $ψ$.

---

The bound variable of a quantifier can be “renamed” ; see Theorem 3.5.6 (Change of Bound Variables), page 71.