On the elementary theory of restricted elementary functions

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 , …, X m ) in the natural language of ( R RE , constants) is equivalent to an existential formula with the extra property that for each x ∈ R m such that ϕ ( x ) is true in R RE there is exactly one y ∈ R n such that ψ ( x, y ) is true in R RE . (Here ψ is quantifier free.)