What is known, and what is published, on the reverse mathematics of the nest of results called Hilbert's Theorem 90?

2$\begingroup$ What is "reverse mathematics"? $\endgroup$ – Igor Rivin Jul 17 '13 at 23:48

3$\begingroup$ @IgorRivin, reverse mathematics (en.wikipedia.org/wiki/Reverse_mathematics) is an area of logic which measures the strength of theorems by comparing their logical strength over a weak base theory. $\endgroup$ – Jason Rute Jul 18 '13 at 0:11

2$\begingroup$ From Cris Conidis' research statement: "In the future I will examine and classify [in the setting of reverse mathematics] the number theoretic consequences of theorems from the (largely unexamined) number theoretic literature, such as Galois’ Theorem and Hilbert’s Theorem 90." His website: math.vanderbilt.edu/~conidis/Chris_J._Conidis/Home.html $\endgroup$ – Jason Rute Jul 18 '13 at 0:18

1$\begingroup$ Theorem 90 is about finite cyclic extensions, so it's provable in $RCA_0$ (modulo some induction, which I don't expect). Kummer theorey might be much more interesting. Why are you interested in Theorem 90? $\endgroup$ – François G. Dorais♦ Jul 18 '13 at 3:29

1$\begingroup$ I am interested in it as a n example of cohomology pretty directly interpretable in PA. $\endgroup$ – Colin McLarty Jul 18 '13 at 9:01
It is provable in RCA_{0} 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 RCA_{0} was discussed by Friedman, Simpson and Smith in Countable algebra and set existence axioms [APAL 25 (1983), 141–181; MR0725732]. The executive summary is that finite Galois theory works fine in RCA_{0}.
The usual proof of Theorem 90 works in RCA_{0}. 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. 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, RCA_{0} 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 WKL_{0} 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 ACA_{0} since we can always comprehend the range of an embedding. So, assuming ACA_{0}, $H^1(G,L^\times)$ is always well defined and always trivial.