# A parameterized family of decidable theories involving differentiable functions

## Gabriele Buriola

**Authors:** Gabriele Buriola, Domenico Cantone, Gianluca Cincotti, Eugenio Omodeo and Gaetano Spartà

We build on the existing literature on decidability in elementary analysis [2,3] by introducing a new family of decidable theories (Here the word ‘theory’ refers to a fragment of a logical language subject to strong syntactic restraints.) called \(\text{RDF}^n\). These theories are parameterized by natural numbers and involve differentiable real functions of class \(C^n\). By extending the previously developed theory \(\text{RDF}^{*}\) [1], each \(\text{RDF}^n\) is a quantifier-free first-order theory that includes numerical variables, basic arithmetic operations, function variables, and operators and relators for function addition, multiplication by a scalar, differentiation, function comparisons, strict and non-strict monotonicity / convexity / concavity, and comparisons between functions (and their derivatives up to \(n\)-th order) and real-valued terms. The sentences constituting the \(\text{RDF}^n\) language are (universally closed) propositional combinations of atomic formulas of the forms shown in the table: therein, the prefix ‘\(\text{S}\_\)’ indicates strictness; \(\alpha\) stands for an integer ranging from 1 to \(n\) and \(D^\alpha\) denotes the \(\alpha\)-th order derivative; \(A\) stands for an interval specification; \(\bowtie\) can be any of the relators \(=,<,>,\leq,\geq\); \(s,t\) stand for real-valued terms, and \(f,g\) for terms designating functions in \(C^n\).

\(s = t\), | \(s > t\), | \(f(s) = t\), | \(D^{\alpha}[f](s) = t\), |

\((f=g)_A\), | \((f>g)_A\), | \((f \bowtie t)_A\), | \((D^{\alpha}[f] \bowtie t)_A\), |

\(\textit{Up}(f)_A\), | \(\textit{Down}(f)_A\) , | \(\textit{Convex}(f)_A\) , | \(\textit{Concave}(f)_A\), |

\(\textit{S}\_\textit{Up}(f)_A\), | \(\textit{S}\_\textit{Down}(f)_A\) , | \(\textit{S}\_\textit{Convex}(f)_A\), | \(\textit{S}\_\textit{Concave}(f)_A\) , |

The decidability of these theories relies on the one hand on Tarski’s celebrated theorem [6] concerning the decision problem for the algebra of real numbers and, on the other hand, on interpolation techniques. Our ultimate goal is to institute a uniform theory \(\textit{RDF}^{\infty}\) encompassing \(C^{\infty}\) functions.

Additionally, we explore the limits of decidability in the presence of a richer endowment of constructs relating derivatives and functions, e.g., equalities of the form \(\left( D^2[f]=g \right)_{\! A}\), building upon the findings of Richardson [4] and subsequent improvements by Laczkovich [5].

## Bibliography

- G. Buriola, D. Cantone, G. Cincotti, E. Omodeo, G. Spartà,
*A decidable theory involving addition of differentiable real functions*,,vol. 940 (2023), pp. 124–148.*Theoretical Computer Science* - H. Friedman, ‘A. Seress,
*Decidability in elementary analysis, I*,,vol. 76(1) (1989), pp. 94–115.*Advances in Mathematics* - \bysame_Decidability in elementary analysis, II_,
,vol. 79(1) (1990), pp. 1–17.*Advances in Mathematics* - D. Richardson,
*Some undecidable problems involving elementary functions of a real variable*,,vol. 33(4) (1968), pp. 514–520.*Journal of Symbolic Logic* - M. Laczkovich,
*The removal of \(pi\) from some undecidable problems involving elementary functions*,,vol. 131(7) (2002), pp. 2235–2240.*Proceedings of the American Mathematical Society* - A. Tarski,
*A decision method for elementary algebra and geometry*,Technical Report U.S. Air Force Project RAND R-109, Santa Monica, CA, 2nd revised edition, University of California Press, Berkeley and Los Angeles, iii+63 pp., 1951.