The prime number theorem and fragments of PA (Q1337499)

Let \(I\Delta_ 0\) denote the subsystem of Peano arithmetic obtained by allowing induction for bounded formulas only. Let exp denote the axiom \(\forall x,y \exists z (z= x^ y)\), where \(z= x^ y\) is a \(\Delta_ 0\) formula defining the graph of the exponential function in \(\mathbb{N}\) and having, provably in \(I\Delta_ 0\), all the usual properties of exponentiation. The system \(I\Delta_ 0+ \exp\) is a strong fragment of Peano arithmetic. The author proves in this system the following version of the prime number theorem: \(\pi(x)\sim x/\log x\), where \(\pi(x)\) is the number of primes less than or equal to \(x\).