Reverse mathematics and local rings

In this paper, we study local rings from the perspective of reverse mathematics. We define local rings in a first-order way by using Pi 20 properties of invertible elements, where for a ring R possibly not commutative, R is left (resp. right) local if for any non-left (resp. non-right) invertible elements x, y is an element of R, x + y is not left (resp. right) invertible; R is local if for any non-invertible elements x, y is an element of R, x + y is not invertible. Firstly, we solve a question of Sato on characterizations of commutative local rings in his PhD thesis (Question 6.22 in Sato (2016)) and prove that the statement "a commutative ring is local if and only if it has at most one maximal ideal" is equivalent to ACA0 over RCA0. We also obtain a nice corollary in computable mathematics, i.e., there is a computable non-local ring with exactly two maximal ideals such that each of them Turing computes the Halting set K. Secondly, we study the equivalence among left local rings, right local rings, and local rings, showing that these three kinds of first-order local rings are equivalent over the weak basis theory RCA0. Finally, we extend the results of reverse mathematics on commutative local rings to noncommutative rings.