It is clear that /Ao + exp b Ao-PHP, while the opposite is not true. Ao-PHP is a rii-statement; hence, it is preserved under initial segment. Let M be a nonstandard model of /Ao and a e M , and consider the initial segment
N o te 6.3. We recall that DOR denotes the theory of discretely ordered rings. Then
Clearly, / is Ao-definable. It is also an injective function from a + 1 into a. We have then a contradiction with Ao-PHP. This, together with Woods’ result, implies that DOR + A0-PHP proves the cofinality of primes.