No label defined (Q3972528)

[For the entire collection see Zbl 0709.00021.] According to \textit{R. Parikh} [J. Symb. Log. 36, 494-508 (1971; Zbl 0243.02037)], arithmetic of feasible numbers \(T[t]\) is an augmentation of any extension \(T\) of Peano arithmetic by a new predicate \(F\) and axioms which say that \(F\) is closed under \(0\), \('\), \(+\), \(*\), \(<\) and also the axiom \(F(t)\) for some closed term \(t\). Typical results for such contradictory (in the classical sense!) arithmetic \(T[t]\) are about lower complexity bounds (relative to the value of \(t\)) for derivations \(P\) in \(T[t]\) of formulas \(A\) which are free of \(F\) and not provable in the original theory \(T\) (e.g., for \(A:=(0=1))\). Or, equivalently, one can consider upper bounds (with respect to complexity of derivations in \(T[t]\), say, of \(0=1\)) of the value of \(t\). The latter bounds are usually formulated in terms of an exponential tower with a large (exponential!) number of stages. The author takes \(t\) and \(T\) just in the language \(0\), \('\), \(+\), \(*\), \(<\), \(=\) and considers Hilbert-type formalization of \(T[t]\) in the linear (i.e. non-tree) form. The first result of the paper uses as the complexity measure of derivations of \(A\) in \(T[t]\) only the number of different formulas involving \(F\). The second result for the case \(T=PA\) uses simultaneously the following measures: (1) the maximal number of occurrences of the main variable in any induction axiom, predicate axiom, and equality axiom in the derivation, (2) the total number of formulas in the derivation, and (3) the maximal depth of terms in \(A\). In this case the above mentioned exponential tower proves to be unusually low, in fact, of a fixed number of stages. Unfortunately, the author gives no comment on the reason for this phenomenon. No proofs, except some lemmas, are presented. In comparison, \textit{R. Parikh} [loc. cit.] considered arithmetic in the richer language of primitive recursive functions and used simultaneously the following measures: (1) the number of axioms \(B(t)\to E\times B(x)\) involving \(F\) is any tree-like Hilbert-style derivation, (2) the maximal number of quantifiers occurring in these axioms (the main contribution in the height of the exponential tower) and (3) the number of occurrences of the axioms \(F(x)\to F(sx)\), \(F(x) \& F(y)\to F(x+y)\) and \(F(x) \& F(y)\to F(x*y)\). Also, \textit{A. G. Dragalin} [Lect. Notes Comput. Sci. 208, 58-79 (1985; Zbl 0604.03019)] used only the number of formulas in any tree-like derivation.