Write a formal proof of the statement

Question

Write a formal proof of the statement "for all rational numbers $b, c$ if the equation $x^2 + bx + c = 0$ has a rational solution $r$, then any other solution $s$ of this equation is a rational number". We can use the two following predicates:

1. Let $Q(x)$ be the predicate "$x$ is a rational number"
2. $S(x)$ be the predicate "$x$ is a solution of the equation $x^2+bx+c = 0$"

Assume the domain for both predicates is the set $\mathbb{R}$ of real numbers. We can use without proof the following fact: if $r, s$ are roots of the equation $x^2 + bx + c$, then the following holds: $b = −(r + s) ∧ c = rs)$.

Answer 1

The precise details will depend on the particularities of the presentation of formal logic you are working in but you need to do something like the following.

First, determine the formal statement you want to prove. It should be something along the lines of $$\forall b \ \forall c \ (Q(b) \land Q(c) \to (\exists r \ (Q(r) \land S(r)) \to \forall s \ ((S(s) \land s \ne r) \to Q(s)))$$ or, if you use Prenex normal form (https://en.wikipedia.org/wiki/Prenex_normal_form), $$\forall b \ \forall c \ \forall r \ \forall s \ (Q(b) \land Q(c) \to ((Q(r) \land S(r)) \to ((S(s) \land s \ne r) \to Q(s))).$$ Working with the latter you would need to assume $Q(b) \land Q(c), \ Q(r) \land S(r),$ and $S(s) \land s \ne r$ and derive $Q(s)$. Deduction rules would then let you build up the three implications one step at a time and then then finally add your quantifiers.

Note that you will have to use various facts about rational numbers, such as those explicitly given to you in the problem, but also, for example, $\forall x \ \forall y ((Q(x) \land Q(y)) \to Q(x+y)).$ It may help to work out an informal proof first and translate it into a formal one.