Local consistency of arithmetic with an ''attainability'' predicate (Q1075323)

Extensions of the first-order arithmetic with the predicate of feasibility had first been studied by \textit{R. Parikh} [J. Symb. Logic 36, 494-508 (1971; Zbl 0243.02037)]. By adding an axiom stating that there are natural numbers which are not attainable by successive additions of one starting from zero, one gets an inconsistent theory. However, it is still possible to show that proofs of reasonably small length yield only true arithmetical statements. The paper under review is concerned with arithmetical theories containing the attainability predicate D(x) with the meaning ''x is an attainable number'', e.g. with a theory \(PAD^+_ m(f_ 1,...,f_ k)\) whose axioms postulate: (i) D(x) determines an initial segment of the set of natural numbers closed under the successor function; (ii) the values of primitive recursive functions \(f_ 1,...,f_ k\) are attainable for any tuple of attainble arguments; (iii) m is not an attainable number. It is shown that every statement which does not include the predicate D and is provable in \(PAD^+_ m(f_ 1,...,f_ k)\) by a short proof (with respect to m) is a theorem of Peano arithmetic extended by the function symbols \(f_ i\). On the other hand, for every length l, there is a natural number m such that the statement ''the sum of any two attainable numbers is attainable'' is not provable in \(PAD^+_ m\) in l steps. A similar result is obtained for multiplication, and provability of statements in theories weaker than \(PAD^+_ m(f_ 1,...,f_ k)\) is characterized.