Authors: Gabriele Buriola and Andreas Weiermann

We extend previous results [2] regarding the phase transition thresholds for Goodstein Sequences and Hydra Games to a more general setting. In both cases, we substitute the original successor function with the iterations of a strictly increasing primitive recursive function \(g\) satisfying the condition \(g(x) \geq x+1\); more precisely, the steps of the Hydra Game, originally of type \(\alpha_{f\!,i+1}= \alpha_{f\!,i}[1+f(i)]\), are now of the form \(\alpha^{f\!,g}_{i+1}=\alpha^{f\!,g}_{i}[1+f(g^{i-1}(1))]\), while the steps of Goodstein sequences are changed from \(m_{f\!,i+1}=m_{f\!,i}\left(1+f(i) \mapsto 1+f(i+1)\right) -1\) to \(m^{f\!,g}_{i+1}=m^{f\!,g}_i\left(1+f(g^{i-1}(1)) \mapsto 1+f(g^{i}(1))\right) -1\). The new phase transition thresholds incorporate the starting function \(g\). These findings also allow a generalization of the phase transition threshold for Ackermannian functions [1] and fit within a rich literature regarding phase transitions in provability [3,4,5].

Bibliography

1. E. Omri, A. Weiermann,Classifying the phase transition threshold for Ackermannian functions,Journal of Pure and Applied Logic,Vol. 158, (2009), pp. 156–162.
2. F. Meskens, A. Weiermann,Classifying phase transition thresholds for Goodstein sequences and Hydra games,Gentzen’s Centenary,Springer International Publishing, Cham, (2015), pp. 455–478.
3. L. Carlucci, G. Lee, A. Weiermann,Sharp thresholds for hypergraph regressive Ramsey numbers,Journal of combinatorial theory. Series A,Vol. 118(2), (2011), pp. 558–585.
4. M. De Smet, A. Weiermann,Sharp Thresholds for a Phase Transition Related to Weakly Increasing Sequences,Journal of logic and computation,Vol. 22(2), (2012), pp. 207–211.
5. L. Gordeev, A. Weiermann,Phase transitions in Proof Theory,Discrete Mathematics and Theoretical Computer Science,(Proceedings), (2010), pp. 343–358.

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\).

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

1. 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.
2. H. Friedman, ‘A. Seress,Decidability in elementary analysis, I,Advances in Mathematics,vol. 76(1) (1989), pp. 94–115.
3. \bysame_Decidability in elementary analysis, II_,Advances in Mathematics,vol. 79(1) (1990), pp. 1–17.
4. D. Richardson,Some undecidable problems involving elementary functions of a real variable,Journal of Symbolic Logic,vol. 33(4) (1968), pp. 514–520.
5. 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.
6. 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.