Finite dimensional real division algebras A celebrated theorem of Milnor and Kervaire asserts that any finite dimensional (not necessarily associative, unital) division algebra over the real numbers has dimension 1,2,4 or 8. This result is established using methods from algebraic topology, such as K-Theory.
Now  for any given natural number $n$ the existence of such an algebra of dimension $n$ is expressible as an assertion $\phi_n$ in the first-order language of field theory. Since the theory $RCF$ of real closed fields is complete, it follows from the theorem  above that  $RCF \vdash   \neg \phi_n$ for all $n\not\in$ {1,2,4,8}. Here the universal quantifier on $n$ is in the meta-theory: we might  say that for  each $n$ there is an elementary  proof of $\phi_n$.
Given such a theorem scheme, one might wonder whether there might be a  uniform elementary proof. Informally this could mean a proof  by induction on the relevant complexity parameter: for example,  $$RCF \vdash  \mbox{ any degree } d  \mbox{  polynomial has at most  }  d  \mbox{ roots}.$$
I would like to imagine that  there  is some first  order-theory  which suitably contains both  RCF and Peano Arithmetic (in particular,  so  as to enable  discussion of  finite sequences of field elements) in which the assertion $$\forall n \;\phi_n\leftrightarrow(n=1 \vee n=2  \vee n=4 \vee  n=8)$$ can  be  legfitimately formalized. Are there standard  constructions for supporting finite sequences? If so, it should follow from completeness of RCF that this assertion  is  equivalent (within such a larger theory)  to  a sentence $\Phi$ in the language of arithmetic. As noted  above, via difficult results from topology, $\Phi$ is true in the standard model  of  Peano Arithmetic. Consequently, it makes sense to ask whether $\Phi$ is provable within Peano Arithmetic.
Some questions:

(1) Can such a recipe be formalized, and does it reasonably capture the notion of  "uniform elementary proof" or  "purely algebraic" proof for such theorem schemes? Here I am not necessarily claiming that these conjectural notions are the same.
(2) In the given example of the 1,2,4,8 theorem, do we expect $\Phi$ to be provable in Peano Arithmetic?

Perhaps I have been looking in the wrong places, but all I have managed  to find are a few comments by Kreisel about "unwinding", on pages 67-68 of this note: http://elib.mi.sanu.ac.rs/files/journals/zr/10/n010p063.pdf
The situation could be compared with what is known in the special cases of commutative division
algebras (dimensions 1,2) and associative division algebras (dimensions 1,2,4). Hopf's proof of the (1,2) theorem also uses some topology, namely that the $n$-dimensional sphere and $n$-dimensional projective space are not homeomorphic when $n>1$; in fact it suffices to show that a specific map   between these spaces is not a homeomorphism.  Perhaps there is an elementary way to formulate
this consideration?  On the other hand,  there is a different and
"purely algebraic" proof, via Bezout's Theorem. I don't have the reference at hand,  but it there is a citation  (froom the 1950s, as I recall) in the Springer-Verlag  book Numbers (Ebbinghaus et. al.). I've seen this proof dismissed as unreadable or unenlightening,
but when I examined it years ago it seemed like it might qualify.
The Frobenius proof of the (1,2,4) theorem is quite evidently purely
algebraic, as is the later extension (1,2,4,8) to alternative division
algebras.
 A: If you ask for a purely algebraic proof, algebraic K-theory is (almost) OK. Indeed for a compact Hausdorff space $X$, it's topological K-theory $K(X)$ is the same as algebraic K-theory  $K_0(C(X;\mathbb{C}))$. So rewrite the proof of Bott-Milnor-Kervaire we will get a (almost) purely algebraic proof. 
EDIT(More detail):
The method topologists solve this problem (according to my knowledge) is constructing an complex line bundle $\xi$ over real projective space $\mathbb{R}\mathbb{P}^{n-1}$, and claim that $n(\xi-\varepsilon)=0$ in $K(\mathbb{R}\mathbb{P}^{n-1})$, where $\varepsilon$ is the (complexification of) trivial  line bundle over $\mathbb{R}\mathbb{P}^{n-1}$. Since we can compute $K(\mathbb{R}\mathbb{P}^{n-1})=\mathbb{Z}/2^{[\frac{n-1}{2}]}\mathbb{Z}$ with a generator $\xi-\varepsilon$, we must have $2^{[\frac{n-1}{2}]}|n$, and thus $n=1,2,4,8$.
Now let $A=C(\mathbb{R}\mathbb{P}^{n-1};\mathbb{C})$, the ring of continuous functions from $\mathbb{R}\mathbb{P}^{n-1}$ to $\mathbb{C}$. As above we can construct a finite generated projective module $\Gamma(\xi)$ over $A$ and so on. The idea of topological proof now becomes purely algebraic except that the concept of continuous.
