The most nonelementary theory
The author affirmatively settles the following problem [\textit{K. J. Compton} and \textit{C. W. Henson}, Ann. Pure Appl. Logic 48, 1--79 (1990; Zbl 0705.03017)]: ``Is there a `natural' decidable theory with a lower bound of the form \(\exp_\infty(f(n))\), where \(f\) is not linearly bounded?'' The author proves that testing the validity of formulas in a decidable rudimentary theory of finite typed sets requires such a lower bound.
scientific article; zbMATH DE number 2083126
scientific article