The Journal of Symbolic Logic

Research Article

On the elementary theory of restricted elementary functions

Lou van den Dries

Department of Mathematics, University of Illinois, Urbana, Illinois 61801

As a contribution to definability theory in the spirit of Tarski's classical work on (R, <, 0, 1, +, ·) we extend here part of his results to the structure

Here exp ∣[0, 1] and sin ∣[0, π] are the restrictions of the exponential and sine function to the closed intervals indicated; formally we identify these restricted functions with their graphs and regard these as binary relations on R. The superscript “RE” stands for “restricted elementary” since, given any elementary function, one can in general only define certain restrictions of it in R RE.

Let (R RE, constants) be the expansion of R RE obtained by adding a name for each real number to the language. We can now formulate our main result as follows.

Theorem. (R RE, constants) is strongly model-complete.

This means that every formula ϕ(X 1, …, Xm ) in the natural language of (R RE, constants) is equivalent to an existential formula

with the extra property that for each xR m such that ϕ(x) is true in R RE there is exactly one yR n such that ψ(x, y) is true in R RE. (Here ψ is quantifier free.)

(Received March 10 1987)