Logic justification for the use of "Let $y = ...$" in Existential proof.

Question

Working on the book: Daniel J. Velleman. "HOW TO PROVE IT: A Structured Approach, Second Edition" (p. 127)

Theorem. For every real number x, if $x > 0$ then there is a real number $y$ such that $y(y + 1) = x$.

I will use the proof of this theorem to give context to my question. The skeleton of the proof is:

Let $x$ be an arbitrary real number, and suppose $x > 0$. Let $$ y = \frac{-1+\sqrt{1+4x}}{2} $$ which is defined since $x > 0$.

I often see that, in the middle of an Existential statement proof, the word "let" appears. I understand the justification for the statement "Let $x$ be an arbitrary real number, and suppose x > 0...", since the statement he is trying to prove has a Universal Quantifier. Variable $x$ needs to be arbitrary; otherwise, it wouldn't be possible to use Universal Introduction inference rule.

However, I have two questions:

• Is there some justification from a logic standpoint for the phrase "Let $ y = \frac{-1+\sqrt{1+4x}}{2} $...

• If using a Natural Deduction system with identity, it is possible to use Identity Introduction at any point of a proof to introduce, for example, "3=3". But, in the former case, does it count as an abbreviation ? Is there some inference rule that allows the introduction of some statement like "Let $y = ...$" in the middle of a proof ?

I appreciate any insight into this matter.

Answer 1

This kind if reasonning is known as "Analysis-Synthesis". I means that we begin by finding a necessay condition and we check that this condition is sufficient.

So, assuming that $ y $ exists, it will satisfy $$y^2+y-x=0$$

whose roots are $$y_1=\frac{-1+\sqrt{1+4x}}{2}$$ and $$y_2=\frac{-1-\sqrt{1+4x}}{2}$$

Now, you just need to check that $ y_1$ exists and works.