In symbolic logic, existence statements are normally written as $\exists x P$ where $P$ is some smaller statement. The $x$ is bound by the existential quantifier and the scope of $x$ is $P$. When working in a formal system, the inference rules dictate how to manipulate such a statement (e.g. existential instantiation). But do we have similar strict rules in natural language proofs?
Suppose I have a theorem stating (in english) “there exists an $n$ such that $P$”. What is the proper way to introduce such an $n$ into my argument? Can I take $n$ to be “in scope” outside the theorem? For example, can I simply make an argument like “Let $m$ = $n^2 + 1$. Since we know that $P$, we also know that $R$”. Similarly for a conditional statement “if $P$, then there exists an $n$ such that $Q$” where I know $P$. What is the proper way to “get” the $n$ out of the existential statement for further deduction? Should I use a different name for the variable?
I see my question as being more about proper style than the concept of existential quantification, which I feel quite comfortable with. I need help figuring out how to write mathematics well, so I appreciate any references to or examples of proofs that use similar deductions.
Just introduce a "fresh" variable (to avoid overloading) and be explicit about what you're doing.
For example, suppose I've proved
Next I have some argument. If along the way I want to introduce an object with property $\varphi$, I'll just write "by the Lemma, let $y$ be such that $\varphi(y)$" where $y$ is an as-yet-unused variable symbol. This exactly parallels how existential instantiation works formally. Note that $y$ might not be the variable $x$ of the statement of the lemma - that's fine!