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,Theoretical Computer Science,vol. 940 (2023), pp. 124–148.
- H. Friedman, ‘A. Seress,Decidability in elementary analysis, I,Advances in Mathematics,vol. 76(1) (1989), pp. 94–115.
- \bysame_Decidability in elementary analysis, II_,Advances in Mathematics,vol. 79(1) (1990), pp. 1–17.
- D. Richardson,Some undecidable problems involving elementary functions of a real variable,Journal of Symbolic Logic,vol. 33(4) (1968), pp. 514–520.
- M. Laczkovich,The removal of \(pi\) from some undecidable problems involving elementary functions,Proceedings of the American Mathematical Society,vol. 131(7) (2002), pp. 2235–2240.
- 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.