Some decidability issues concerning C^n real functions

This paper adapts preexisting decision algorithms to a family ℛ𝒟ℱ = {RDF𝑛 | 𝑛 ∈ N} of languages regarding one-argument real functions; each RDF𝑛 is a quantifier-free theory about the differentiability class 𝐶^𝑛, embodying a fragment of Tarskian elementary algebra. The limits of decidability are also highlighted, by pointing out that certain extensions of RDF𝑛 are undecidable. The possibility of extending RDF𝑛 into a language RDF∞ regarding the class 𝐶^∞, without disrupting decidability, is briefly discussed. Two sorts of individual variables, namely real variables and function variables, are available in each RDF𝑛. The former are used to construct terms and formulas that involve basic arithmetic operations and comparison relators between real terms, respectively. In contrast, terms designating functions involve function variables, constructs for addition of functions and scalar multiplication, and—outermost—𝑖-th order differentiation 𝐷^𝑖[ ] with 𝑖 ⩽ 𝑛. An array of predicate symbols designate various relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: function comparisons, strict and non-strict monotonicity / convexity / concavity, comparisons between a function (or one of its derivatives) and a real term. The decidability of RDF𝑛 relies, on the one hand, on Tarski’s celebrated decision algorithm for the algebra of real numbers, and, on the other hand, on reduction and interpolation techniques. An interpolation method, specifically designed for the case 𝑛 = 1, has been previously presented; another method, due to Carla Manni, can be used when 𝑛 = 2. For larger values of 𝑛, further research on interpolation is envisaged.