Speaker
Gabriele Buriola
University of Verona
Talks at this conference:
Wednesday, 14:50, J431 
Phase Transition Thresholds for Generalized Goodstein Sequences, Hydra Games and Ackermannian Functions. 

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^{i1}(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^{i1}(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


Wednesday, 15:40, J330 
A parameterized family of decidable theories involving differentiable functions 

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 quantifierfree firstorder 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 nonstrict monotonicity / convexity / concavity, and comparisons between functions (and their derivatives up to \(n\)th order) and realvalued 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 realvalued 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
