# 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 finite Galois theory in RCA0 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 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. 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.

-