Equational theory of positive numbers with exponentiation

Gurevič, R.

doi:10.1090/S0002-9939-1985-0781071-1

Equational theory of positive numbers with exponentiation
HTML articles powered by AMS MathViewer

by R. Gurevič PDF

Proc. Amer. Math. Soc. 94 (1985), 135-141 Request permission

Abstract:

A. Tarski asked if all true identities involving 1, addition, multiplication, and exponentiation can be derived from certain so-called "high-school" identities (and a number of related questions). I prove that equational theory of $({\mathbf {N}},1, + , \cdot , \uparrow )$ is decidable ($a \uparrow b$ means ${a^b}$ for positive $a,b$) and that entailment relation in this theory is decidable (and present a similar result for inequalities). A. J. Wilkie found an identity not derivable from Tarski’s axioms with a difficult proof-theoretic argument of nonderivability. I present a model of Tarski’s axioms consisting of 59 elements in which Wilkie’s identity fails.

References

Leon Henkin, The logic of equality, Amer. Math. Monthly 84 (1977), no. 8, 597–612. MR 472649, DOI 10.2307/2321009
A. G. Hovanskiĭ, A class of systems of transcendental equations, Dokl. Akad. Nauk SSSR 255 (1980), no. 4, 804–807 (Russian). MR 600749
Angus Macintyre, The laws of exponentiation, Model theory and arithmetic (Paris, 1979–1980) Lecture Notes in Math., vol. 890, Springer, Berlin-New York, 1981, pp. 185–197. MR 645003
D. Richardson, Solution of the identity problem for integral exponential functions, Z. Math. Logik Grundlagen Math. 15 (1969), 333–340. MR 262068, DOI 10.1002/malq.19690152003
Alex J. Wilkie, On exponentiation—a solution to Tarski’s high school algebra problem, Connections between model theory and algebraic and analytic geometry, Quad. Mat., vol. 6, Dept. Math., Seconda Univ. Napoli, Caserta, 2000, pp. 107–129. MR 1930684