Remark on Kreisel's conjecture

At the end of the 60's, Kreisel conjectured that formal arithmetics admit infinite induction rules if the lengths of proofs of their premises are uniformly bounded by the same number. By the length of a proof we mean the number of applications of axioms and rules of inference. In this article we construct a theory R ^* with a finite number of specific axioms. The language of R ^* contains a constant 0, a unary function symbol, equality, and ternary predicates for addition and multiplication. It is proved that for any consistent axiomatizable extensionR^* it is possible to find a formula A(a) that satisfies the following conditions: a) xA(x) cannot be derived in; b) for any n the length of the proof of the formula A(0⁽ⁿ⁾) is no greater than c₁log₂ (n+1)]+c₂, where the constants c₁ and c₂ are independent of n. Here the expression 0⁽ⁿ⁾ indicates 0 with n primes.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Institua im. V. A. Steklova Akademii Nauk SSSR, Vol. 176, pp. 118–126, 1989.