Contents: (Math. Log. Quart. 2/2020)
Mathematical logic quarterly · 2020
Orders on computable ringsThe Artin-Schreier theorem says that every formally real field has orders.Friedman, Simpson, and Smith (1983) showed that the Artin-Schreier theorem is equivalent to WKL 0 over RCA 0 .We first prove that the generalization of the Artin-Schreier theorem to noncommutative rings is equivalent to WKL 0 over RCA 0 .In the theory of orderings on rings, following an idea of Serre, we often show the existence of orders on formally real rings by extending pre-orders to orders, where Zorn's lemma is used.We then prove that "pre-orders on rings not necessarily commutative extend to orders" is equivalent to WKL 0 .