×

Notations for exponentiation. (English) Zbl 1061.03062

Summary: We define a coding of natural numbers – which we will call exponential notations – and interpretations of the less-than-relation, the successor, addition and exponentiation function on exponential notations. We prove that all these interpretations are polynomial time computable. As a corollary we obtain that feasible arithmetic can prove the consistency of the canonical equational theory for the language containing the successor, addition and exponentiation function.

MSC:

03F25 Relative consistency and interpretations
03D15 Complexity of computation (including implicit computational complexity)
03F30 First-order arithmetic and fragments
68Q19 Descriptive complexity and finite models
Full Text: DOI

References:

[1] A. Beckmann, Separating fragments of bounded arithmetic, Ph.D. Thesis, WWU Münster, 1996.; A. Beckmann, Separating fragments of bounded arithmetic, Ph.D. Thesis, WWU Münster, 1996. · Zbl 0858.03053
[2] Buss, S., Bounded arithmetic. Bounded arithmetic, Studies in Proof Theory, Lecture Notes, Vol. 3 (1986), Bibliopolis: Bibliopolis Naples · Zbl 0649.03042
[3] P. Clote, J. Krajı́ček, Open problems, in: P. Clote, J. Krajı́ček (Eds.), Arithmetic, Proof Theory, and Computational Complexity, Papers from the Conference held in Prague, July 2-5, 1991, Oxford Logic Guides 23, New York, 1993, pp. 1-9.; P. Clote, J. Krajı́ček, Open problems, in: P. Clote, J. Krajı́ček (Eds.), Arithmetic, Proof Theory, and Computational Complexity, Papers from the Conference held in Prague, July 2-5, 1991, Oxford Logic Guides 23, New York, 1993, pp. 1-9.
[4] Cobham, A., The intrinsic computational difficulty of functions, (Bar-Hillel, Y., Logic, Methodology and Philosophy of Science (1965), North-Holland: North-Holland Amsterdam), 24-30 · Zbl 0192.08702
[5] Hajek, P.; Pudlák, P., Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic (1993), Springer: Springer Berlin · Zbl 0781.03047
[6] Krajı́ček, J., Bounded Arithmetic, Propositional Logic, and Complexity Theory (1995), Cambridge University Press: Cambridge University Press Heidelberg · Zbl 0835.03025
[7] Pohlers, W., Proof Theory: An Introduction. Proof Theory: An Introduction, Lecture Notes in Mathematics, Vol. 1407 (1989), Springer: Springer Berlin · Zbl 0695.03024
[8] Rose, H. E., Subrecursion: functions and hierarchies (1984), Oxford Logic Guides: Oxford Logic Guides Oxford · Zbl 0539.03018
[9] Takeuti, G., Sharply bounded arithmetic and the function \(a−1\), (Sieg, W., Logic and Computation. Logic and Computation, Contemporary Mathematics, Vol. 106 (1990), American Mathematical Society: American Mathematical Society Providence, RI), 281-288 · Zbl 0707.03046
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.