Nested Quantifier: What is the right solution?

Question

Use quantifiers and logical connectives to express the fact that a quadratic polynomial with real number coefficients has at most two real roots

Solution:

$\forall a \forall b \forall c ((a \neq 0 \lor b \neq 0) \rightarrow \exists x(x = \frac {-b + \sqrt {b^2 - 4ac}}{2a} \lor x = \frac {-b - \sqrt {b^2 - 4ac}}{2a}) \land \forall y ((y = \frac {-b + \sqrt {b^2 - 4ac}}{2a} \lor y = \frac {-b - \sqrt {b^2 - 4ac}}{2a}) \rightarrow y =x))$

Why this solution is not right? Please explain.

Answer 1

You should write something like

$\forall f(X) \in \mathbb{R}[X]\forall a, b , c \in \mathbb{R}: ((\deg f = 2) \land (f(a)=f(b)=f(c)=0)) \Rightarrow ((b = c)\lor (a = b)\lor(a = c))$

or alternatively

$\forall a,b,c,x,y,z \in \mathbb{R}: ((a \neq 0) \land (ax^2+bx+c=ay^2+by+c=az^2+bz+c=0)) \Rightarrow ((x = y)\lor (x = z) \lor(z = y))$