# Reverse mathematics of Hilbert's Theorem 90

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

• What is "reverse mathematics"? – Igor Rivin Jul 17 '13 at 23:48
• @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. – Jason Rute Jul 18 '13 at 0:11
• 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 – Jason Rute Jul 18 '13 at 0:18
• 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? – François G. Dorais Jul 18 '13 at 3:29
• I am interested in it as a n example of cohomology pretty directly interpretable in PA. – Colin McLarty Jul 18 '13 at 9:01

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 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.
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.