What is known, and what is published, on the reverse mathematics of the nest of results called [Hilbert's Theorem 90](http://en.wikipedia.org/wiki/Hilbert%27s_Theorem_90)?



Reverse mathematics of Hilbert's Theorem 90
It is provable in RCA0 that if $K$ is a finite Galois extension of $F$ with Galois group $G$ then $H^1(G,L^\times)$ is trivial (every cocycle $a:G \to L^\times$ is a coboundary).


The finite Galois theory in RCA0 was discussed by Friedman, Simpson and Smith in [*Countable algebra and set existence axioms*](http://dx.doi.org/10.1016/0168-0072%2883%2990012-X) [APAL 25 (1983), 141–181; [MR0725732](http://www.ams.org/mathscinet-getitem?mr=725732)]. The executive summary is that finite Galois theory works fine in RCA0. 


The usual proof of Theorem 90 works in RCA0. The linear independence of characters is provable using only $\Sigma^0\_1$-induction since one can check linear dependence by testing at a fixed finite basis of $L$ over $K$. It follows that if $a:G \to L^\times$ is a cocycle then there is a $x \in L^\times$ such that $y = \sum\_{\sigma \in G} a(\sigma)\sigma(x)$ is nonzero. Standard algebraic manipulations then show that $a(\sigma) = y/\sigma(y)$, i.e. $a$ is a coboundary.


Infinite Galois extensions are more subtle as discussed in [my paper with Jeff Hirst and Paul Shafer](http://arxiv.org/abs/1209.4944). For Theorem 90, it seems that the issue is a definitional one more than anything else. 


If $K$ is an infinite Galois extension of $F$ such that $F$ is a subset of $K$ (as opposed to being merely embeddable in $K$) then the Galois group $G$ of $K$ over $F$ is a separably closed subgroup of permutations of $K$. Then $G$ can be represented as a complete separable metric space in the usual manner and one can make sense of the idea of a *continuous* cocycle $a:G \to L^\times$. In that scenario, RCA0 does prove that $H^1(G,L^\times)$ is trivial since every continuous cocycle is a lifting of a cocycle from a finite Galois subextension.


In the general case where $F$ is merely embeddable in $K$, several issues arise. Galois theory still makes sense over WKL0 but the Galois group $G$ is not necessarily separably closed. It is unclear what a continuous cocycle would be in that case. So the main issue is to define $H^1(G,L^\times)$ before proving anything about it. Note that this case is impossible in ACA0 since we can always comprehend the range of an embedding. So, assuming ACA0, $H^1(G,L^\times)$ is always well defined and always trivial.


