The situation
I have to transfer statements from the "recursive world" into the "$\color{red}{\text{syntactical world}}$", in the context of binumerability of primitive recursive predicates into the theory $\newcommand{PA}{\color{red}{\text{PA}}} \PA$.
We have, as the main theorem:
Say $P(\cdot)$ is a primitive recursive relation. Then there exists a formula $\color{red}{\overline{P}}$ such that for every $x\in\mathbb{N}$, where $\color{red}{\overline{x}}$ is a corresponding closed term, i.e. $\color{red}{s ( s ( s ( \ldots 0 \ldots ) ) )}$,
(1) $P(x)\Leftrightarrow \color{red}{\PA\vdash\overline{P}(\overline{x})}$
(2) $\neg P(x)\Leftrightarrow \color{red}{\PA\vdash\neg\overline{P}(\overline{x})}$.
This means, one can transfer from one world to another as long as one is talking about closed terms.
The question
Coming from this question, I'm in the need to prove then the following:
$$\forall n \in \mathbb{N} : \color{red}{\PA \vdash \exists x_1 w + x_1 = \overline{n}} \Rightarrow \exists k \in\mathbb{N} : \color{red}{\PA\vdash w = \overline{k}}$$
or in other words: if one assumes a closed term bound on a variable, one can then derive that it has to be a closed term also.
Thanks for any help.