Checking an answer from How To Prove It

Question

I am not sure whether my answer to the following question is correct or not. The question is,

Theorem. Suppose that $b^2 \gt 4ac$. Then the quadratic equation $ax^2 + bx + c = 0$ has exactly two real solutions.

To give an instance of the theorem, you must specify values for $a$, $b$ and $c$, but not $x$. Why?

I found some answers online but they used math I haven't seen yet. My answer is,

The sentence 'the quadratic equation $ax^2 + bx + c = 0$ has exactly two solutions' transcribed to logic is,

$\exists x_1,x_2 \in \mathbb R (ax_1^2 + bx_1 + c = 0 \ \land \ ax_2^2 + bx_2 + c = 0 \ \land \ \forall y((y \neq x_1 \lor y \neq x_2) \rightarrow ay^2 + by + c \neq 0) $

You do not need to give a value for $x$ because it doesn't occur freely.

Is this right? And also is the transcription right?

Answer 1

Because the theorem says :

for every $a,b,c$ (real numbers) the equation $ax^2+bx+c=0$ has exactly two real solutions iff $b^2 > 4ac$.

Thus, an instance of the above equation will be obtained instantiating the leading universal quantifiers with three individual real numbers, says : $a=1, b=3, c=2$.

The result will be the individual equation :

$x^2+3x+2=0$

whose roots are : $-1,-2$.

The roots must not be "specified" because they must be computed from the individual equation.

---

In fully symbolic form the theorem will be :

$\forall a,b,c \ \exists x_1,x_2 [x_1 \ne x_2 \land \ldots \land \forall z (az^2+bz+c=0 \to z=x_1 \lor z=x_2)]$.

Answer 2

It is almost correct. You forgot to add that $x_1\neq x_2$.