Insolvability of quintic says that no analogue of quadratic formula is available for quintic equations. For quadratic equations, the formula $x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}$ gives you all the roots of $ax^2 + bx + c = 0$ for any choice of $a$, $b$, $c$. Let us work on a field $F$ with algebraic closure $\overline{F}$.
Formulas like $x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}$ can be interpreted in two ways. First way, one interpret $\sqrt \cdot$ as a fixed function $\sqrt \cdot \colon \overline{F} \to \overline{F}$. In this case, $\pm$ is necessary. Second way, one interpret $\sqrt \cdot$ as a multivalued function $\sqrt \cdot \colon \overline{F} \to \mathcal{P}(\overline{F})$. In this case, $\pm$ is unnecessary and one formula $x = \frac{-b + \sqrt{b^2 - 4ac}}{2a}$ gives you all the roots.
For the first interpretation one can formulate the insolvability of quintic like this: There doesn't exist a function $f\colon F^5 \to \overline{F}$ which
- can be expressed with $+$, $-$, $\times$, $\div$, and for any $n$ any function $\sqrt[n]{\cdot}\colon \overline{F} \to \overline{F}$ satisfying $(\sqrt[n]{x})^n = x$ for every $x \in \overline{F}$
- and $x = f(a, b, c, d, e)$ is a root of polynomial equation $x^5 + ax^4 + bx^3 + cx^2 + dx + e = 0$.
How could one connect this formulation to the usual Galois theoretic proof of insolvability of quintic? For quadratic equations $x^2 + ax + b = 0$, we know that $f(a, b) := \frac{-a + \sqrt{a^2 - 4b}}{2}$ satisfies the condition for any choice of $\sqrt \cdot$. Now one can find an analouge $f^\bullet \in \overline{F(a, b)}$ corresponding to $f$. Preciesly, one can pick a square root of $a^2 - 4b$ in the algebraic closure of $F(a, b)$ where $a$ and $b$ are indeterminates, and consider $f^\bullet := \frac{-a + \sqrt{a^2 - 4b}}{2}$. We know that $f^\bullet$ is a solution of the polynomial equation $x^2 + ax + b = 0$. In this setting one can apply Galois theoretic approaches about field extensions of $F(a, b)$.
The key is, in this case not only $f$ is numerically correct (gives a correct root for any choice of $a, b$), but it is also symbolically correct (the analogue $f^\bullet$ is a solution of the euqation). So I think if one can prove that any numerically correct formula is also symbolically correct, the formulation above can be proven by the usual Galois theoretic proof.
Are my thoughts correct? If correct, then how could one prove that any numerically correct formula is also symbolically correct?
Edit: Some attempt by my acquaintance: Let $f$ be a numerically correct formula for $n$th degree polynomial equation and $f^\bullet$ be the analogue in $\overline{F(a_0, \ldots, a_{n - 1})}$. Let $A := F[a_0, \ldots, a_{n - 1}]$ and $K$ be a finite extension of $F(a_0, \ldots, a_{n - 1})$ containing $f^\bullet$. Let $p \in A[x]$ be the polynomial $x^n + a_{n - 1}x^{n - 1} + \ldots + a_0$. Now let $B$ be the integral closure of $A$ in $K$. Then $B$ is a finite $A$-module, thus finitely generated over $F$. Localize $B$ by an appropriate element $g \in A$ so that $f^\bullet \in B_g$, and $B_g$ is still finitely generated over $F$. Since $J(B_g) = 0$, it suffices to prove that $p(f^\bullet) \in M$ for every maximal ideal $M$ of $B_g$. $B_g/M$ embeds into $\overline{F}$, and $f^\bullet$ seems to be mapped to an evaluation of the function $f$ at a point $b_0, \ldots, b_{n - 1} \in \overline{F}$. If one can prove the last sentence, we are done for algebraically closed fields. Actually there are some additional difficulties here, since $f$ chooses arbitrary branch when extracting $n$-th root.
Edit 2: Giving a particular insolvable polynomial wouldn't work when $F$ is algebraically closed. Here I am referring to the Galois theoretic proof of insolvability of general polynomial. Also, if $F$ is a finite field, there would be trivially a numerically correct solution, so I think this question would be interesting when there are some restriction on $F$, for example algebraically closed.
Clarification: The usual Galois theoretic proof I'm referring to is that for indeterminates $a$, $b$, $c$, $d$, $e$, $x^5 + ax^4 + bx^3 + cx^2 + dx + e = 0$ is not solvable by radicals in $F(a, b, c, d, e)$ since the splitting field has Galois group $S_5$.
Edit 3: The problem here is that $f^\bullet$ is not a function, in contrast to $f$. This is like the distinction between a formal polynomial and a polynomial function. In contrast to polynomials, there isn't such a thing as evaluation homomorphism $\overline{F(a_0, a_1, \ldots, a_{n - 1})} \to \overline{F}$, because it would be an embedding, which is impossible (nevertheless the idea in Edit 1 is an attempt to evaluate such things). By the usual Galois theoretic proof, nonexistance of $f^\bullet$ can be established, but it doesn't directly imply nonexistance of $f$. As I said eariler, when $F$ is finite, this is not the case. There must be a distinction between numerical correctness and symbolical correctness. One should require some condition on $F$ (e.g. algebraically closed) to prove that there exists no function satisfying given conditions. This is not a statement about elements of $\overline{F(a_0, a_1, \ldots, a_{n - 1})}$. This is the reason I asked how could one prove that any numerically correct formula is also symbolically correct?. For example, when $F$ is infinite, two polynomials are equal iff the related polynomial functions are equal. This is an example of connection between numerical correctness and symbolical correctness. As suggested in the comments, I should read some original proofs rather than the proof I'm referring to.
The trouble is, how do you define "can be expressed with"?
The Galois-theoretic theorem and proof states the problem precisely as:
The precise statement of field extensions by adjoining radicals captures the idea of a "formula involving only radicals". For in the above situation, all the roots of $f$ would lie in $F_n$ and every element of $F_n$ can be obtained through applying field operations and (nested) radicals to elements of $F$. If a quintic formula existed, say, for $F=\Bbb Q$, that would in particular imply every quintic over $\Bbb Q$ has a splitting field extension of the above form. The Galois-theoretic proof of the unsolvability of the quintic is, more precisely, a proof that there are quintic (and higher) polynomials over $\Bbb Q$ whose splitting field extension cannot be broken down into a tower of radical extensions.
In particular, a "general formula" would imply every quintic has some kind of associated canonical series of extensions as described above, but there are polynomials for which no such tower exists, canonical or otherwise.