Local behaviour of the Chebyshev theorem in models of I⊿₀

Extract

Let I⊿₀ denote the fragment of Peano arithmetic where induction is restricted only to bounded formulas (⊿₀-formulas), i.e. formulas where all the quantifiers are bounded. We will examine the behaviour in I⊿₀ of Chebyshev's classical result on the distribution of primes. Chebyshev showed that each of the following functions on N is bounded by a polynomial in each of the others:

In his proof he used, as auxiliaries, factorials and binomial coefficients.

When we work in a weak system like I⊿₀ we have to deal with two problems:

(i) There is not an immediate meaning for symbols like x^y, Π_p≤xp, and x!.

(ii) Some basic functions like exponentiation, factorial, and product of primes up to a certain element, are in general only partially definable.

The first problem is equivalent to finding ⊿₀-formulas representing the relations z = x^y, y = Π_p≤xp, and y = x!. While we can easily express that y is the product of all primes less than or equal to x in a ⊿₀-way, it requires a subtle argument to define z = x^y by a ⊿₀-formula. The most natural way of expressing it is via the formalization of the Chinese remainder theorem coding the recursion procedure used in the definition of x^y. But this can be expressed only via a Σ₁-formula. ⊿₀-definitions of exponentiation were given by Paris and Bennett (see [GD] and [B]), and all sensible definitions of this type are equivalent (see Remark 1). Later we will examine properties of such a definition E₀(x, y, z). The ⊿₀0-definition of y = Π_p≤xp is much more straightforward, since both the relation of being a prime and the divisibility relation are ⊿₀-definable. We will give an explicit definition of it and denote it by Ψ(x, y). In this way, by a ⊿₀-induction, we will be able to prove the uniqueness of the elements y and z satisfying Ψ(x, y) and E₀(x, y, z), respectively.