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.